Hi Fanda, On Tue, Oct 17, 2017 at 4:27 PM, František Blahoudek <fandikb@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