diff --git a/NEWS b/NEWS index 3fe9fecfe9cbe76eba70ace3733bf54669eaac3c..2e051b4159b0cc4787675977c916060487e2145f 100644 --- a/NEWS +++ b/NEWS @@ -38,7 +38,7 @@ New in spot 2.0.1a (not yet released) --eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options these do not output scalable patterns, but simply a list of formulas appearing in these three papers: Dwyer et al (FMSP'98), Etessami & - Holzmann (Concur'00) Somenzi & Bloem (CAV'00). + Holzmann (Concur'00), Somenzi & Bloem (CAV'00). Library: @@ -53,6 +53,9 @@ New in spot 2.0.1a (not yet released) is_inherently_weak() will update the corresponding properties of the automaton as a side-effect of their check. + * language_containment_checker now has default values for all + parameters of its constructor. + Python: * The __format__() method for formula support the same @@ -60,6 +63,13 @@ New in spot 2.0.1a (not yet released) So "{:[i]s}".format(f) is the same as "{:s}".format(f.unabbreviate("i")). + * Bindings for language_containment_checker were added. + + Documentation: + + * A new example page shows how to test the equivalence of + two LTL/PSL formulas. https://spot.lrde.epita.fr/tut04.html + Bug fixes: * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1 diff --git a/doc/Makefile.am b/doc/Makefile.am index 9f9f465122af95590ae6d44c7ba6398ca9fe989a..292b37da2fdf084b55537fdaa561f5551ed6af20 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -96,6 +96,7 @@ ORG_FILES = \ org/tut01.org \ org/tut02.org \ org/tut03.org \ + org/tut04.org \ org/tut10.org \ org/tut20.org \ org/tut21.org \ diff --git a/doc/org/tut.org b/doc/org/tut.org index b34ab01ce60e51323f6e14f87061ba08f10924d6..1eb19401a8404a4f36cbe3b198d457eb6984d3c1 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -22,6 +22,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut01.org][Parsing and Printing LTL Formulas]] - [[file:tut02.org][Relabeling Formulas]] +- [[file:tut04.org][Testing the equivalence of two LTL formulas]] - [[file:tut10.org][Translating an LTL formula into a never claim]] - [[file:tut20.org][Converting a never claim into HOA]] - [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]] diff --git a/doc/org/tut04.org b/doc/org/tut04.org new file mode 100644 index 0000000000000000000000000000000000000000..1d9344570a2e7781e6ee8f1fdc716b04e38af52f --- /dev/null +++ b/doc/org/tut04.org @@ -0,0 +1,95 @@ +# -*- coding: utf-8 -*- +#+TITLE: Testing the equivalence of two formulas +#+DESCRIPTION: Code example for testing the equivalence of two LTL or PSL formulas +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +This page show how to test whether two LTL/PSL formulas are equal. + +* Shell + +Using a =ltlfilt= you can use =--equivalent-to=f= to filter a list of +LTL formula and retain only those equivalent to =f=. So this gives an easy +way to test the equivalence of two formulas: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -f '(a U b) U a' --equivalent-to 'b U a' +#+END_SRC +#+RESULTS: +: (a U b) U a + +Since input formula was output, it means it is equivalent. Adding +=-c= to count the number for formula output provide a yes/no answer. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -c -f '(a U b) U a' --equivalent-to 'b U a' +#+END_SRC +#+RESULTS: +: 1 + +* Python + +In Python, we can test this via a =language_containment_checker= +object: + +#+BEGIN_SRC python :results output :exports both +import spot +f = spot.formula("(a U b) U a") +g = spot.formula("b U a") +c = spot.language_containment_checker() +print(c.equal(f, g)) +#+END_SRC +#+RESULTS: +: True + +The equivalence check is done by converting the formulas $f$ and $g$ +and their negation into four automata $A_f$, $A_{\lnot f}$, $A_g$, and +$A_{\lnot g}$, and then making sure that $A_f\otimes A_{\lnot g}$ and +$A_g\otimes A_{\lnot f}$ are empty. + +We could also write this check by doing [[file:tut10.org][the translation]] and emptiness +check ourselves. For instance: + +#+BEGIN_SRC python :results output :exports both +import spot + +def implies(f, g): + a_f = f.translate() + a_ng = spot.formula_Not(g).translate() + return spot.product(a_f, a_ng).is_empty() + +def equiv(f, g): + return implies(f, g) and implies(g, f) + +f = spot.formula("(a U b) U a") +g = spot.formula("b U a") +print(equiv(f, g)) +#+END_SRC +#+RESULTS: +: True + +The =language_containment_checker= object essentially performs the +same work, but it also implements a cache to avoid translating the +same formulas multiple times when it is used to test multiple +equivalence. + +* C++ + +Here is a C++ translation of the first Python example. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include + + int main() + { + spot::formula f = spot::parse_formula("(a U b) U a"); + spot::formula g = spot::parse_formula("b U a"); + spot::language_containment_checker c; + std::cout << (c.equal(f, g) ? "Equivalent\n" : "Not equivalent\n"); + } +#+END_SRC + +#+RESULTS: +: Equivalent diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 0042b3347f31a4f01804fd26a993933244abbe74..e1b82016166a589a7842f7e992b662287f9007c6 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -874,3 +874,7 @@ def sat_minimize(aut, acc=None, colored=False, def parse_word(word, dic=_bdd_dict): from spot.impl import parse_word as pw return pw(word, dic) + +def language_containment_checker(dic=_bdd_dict): + from spot.impl import language_containment_checker as c + return c(dic) diff --git a/python/spot/impl.i b/python/spot/impl.i index cd895afbd7773605254a108d912a632741bfdc67..a544b4ff0e581c36f184b14684dbcef145a089d0 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -94,6 +94,7 @@ #include #include +#include #include #include #include @@ -374,6 +375,7 @@ namespace std { %include %include +%include %include %include %include diff --git a/spot/tl/contain.cc b/spot/tl/contain.cc index 2ca722ffefddfd2d5dc5d980c2808d025dacbe57..a60a7ac3b948e9defd223fbc960961bdee7a3ed1 100644 --- a/spot/tl/contain.cc +++ b/spot/tl/contain.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de +// Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -29,7 +29,7 @@ namespace spot { language_containment_checker::language_containment_checker - (const bdd_dict_ptr& dict, bool exprop, bool symb_merge, + (bdd_dict_ptr dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx) : dict_(dict), exprop_(exprop), symb_merge_(symb_merge), branching_postponement_(branching_postponement), diff --git a/spot/tl/contain.hh b/spot/tl/contain.hh index ba43980b5fe962fdfa977523b559da91152802a5..f26ca5a9af3a460c9b17198679ffbcd25d705f5f 100644 --- a/spot/tl/contain.hh +++ b/spot/tl/contain.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche +// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -42,10 +42,11 @@ namespace spot public: /// This class uses spot::ltl_to_tgba_fm to translate LTL /// formulae. See that function for the meaning of these options. - language_containment_checker(const bdd_dict_ptr& dict, bool exprop, - bool symb_merge, - bool branching_postponement, - bool fair_loop_approx); + language_containment_checker(bdd_dict_ptr dict = make_bdd_dict(), + bool exprop = false, + bool symb_merge = true, + bool branching_postponement = false, + bool fair_loop_approx = false); ~language_containment_checker();