17 Oct
2017
17 Oct
'17
4:27 p.m.
Hi,
I have found out that is_tt and is_ff does nt work as expected in Python.
See the attached notebook for details.
Best,
Fanda Blahoudek
18 Oct
18 Oct
2:31 p.m.
Hi Fanda,
On Tue, Oct 17, 2017 at 4:27 PM, František Blahoudek <fandikb(a)gmail.com> wrote:
Hi,
I have found out that is_tt and is_ff does nt work as expected in Python.
See the attached notebook for details.
formula::is_tt() and formula::is_ff() tests whether the formula (not
the language) is tt or ff, but that isn't the case in your notebook,
so it seems to be working as expected.
class SPOT_API formula final
{
[...]
/// Return the true constant.
static formula tt() {...}
/// Whether the formula is the true constant.
bool is_tt() const {...}
[...]
For equivalence checks, see
https://spot.lrde.epita.fr/tut04.html
--
Alexandre Duret-Lutz
2667
days inactive
2668
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
František Blahoudek