alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* doc/org/tut04.org: Show are_equivalent().

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2018-05-15 16:17:00 +02:00
parent 6a808492c1
commit 965d0ed6b7
1 changed files with 41 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

53
doc/org/tut04.org
View file

@ -36,23 +36,21 @@ familiar to =grep= users.)
* Python * Python
In Python, we can test this via a =language_containment_checker= In Python, we can implement this in a number of ways. The
object: easiest is to use the =spot.are_equivalent()= function.
#+BEGIN_SRC python :results output :exports both #+BEGIN_SRC python :results output :exports both
import spot import spot
f = spot.formula("(a U b) U a") are_eq = spot.are_equivalent("(a U b) U a", "b U a")
g = spot.formula("b U a") print("Equivalent" if are_eq else "Not equivalent")
c = spot.language_containment_checker()
print("Equivalent" if c.equal(f, g) else "Not equivalent")
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: Equivalent : Equivalent
The equivalence check is done by converting the formulas $f$ and $g$ The equivalence check is done by converting the input formulas $f$ and
and their negation into four automata $A_f$, $A_{\lnot f}$, $A_g$, and $g$ and their negation into four automata $A_f$, $A_{\lnot f}$, $A_g$,
$A_{\lnot g}$, and then making sure that $A_f\otimes A_{\lnot g}$ and and $A_{\lnot g}$, and then making sure that $A_f\otimes A_{\lnot g}$
$A_g\otimes A_{\lnot f}$ are empty. and $A_g\otimes A_{\lnot f}$ are empty.
We could also write this check by doing [[file:tut10.org][the translation]] and emptiness We could also write this check by doing [[file:tut10.org][the translation]] and emptiness
check ourselves. For instance: check ourselves. For instance:
@ -62,7 +60,7 @@ import spot
def implies(f, g): def implies(f, g):
a_f = f.translate() a_f = f.translate()
a_ng = spot.formula_Not(g).translate() a_ng = spot.formula.Not(g).translate()
return spot.product(a_f, a_ng).is_empty() return spot.product(a_f, a_ng).is_empty()
def equiv(f, g): def equiv(f, g):
@ -75,6 +73,19 @@ print("Equivalent" if equiv(f, g) else "Not equivalent")
#+RESULTS: #+RESULTS:
: Equivalent : Equivalent
This can also be done 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("Equivalent" if c.equal(f, g) else "Not equivalent")
#+END_SRC
#+RESULTS:
: Equivalent
The =language_containment_checker= object essentially performs the The =language_containment_checker= object essentially performs the
same work, but it also implements a cache to avoid translating the same work, but it also implements a cache to avoid translating the
same formulas multiple times when it is used to test multiple same formulas multiple times when it is used to test multiple
@ -82,7 +93,25 @@ equivalences.
* C++ * C++
Here is a C++ translation of the first Python example. Here are possible C++ implementations using either =are_equivalent()=
or the =language_containment_checker=. Note that the
=are_equivalent()= function also work with automata.
#+BEGIN_SRC C++ :results verbatim :exports both
#include <iostream>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/contains.hh>
int main()
{
spot::formula f = spot::parse_formula("(a U b) U a");
spot::formula g = spot::parse_formula("b U a");
std::cout << (spot::are_equivalent(f, g) ?
"Equivalent\n" : "Not equivalent\n");
}
#+END_SRC
#+RESULTS:
: Equivalent
#+BEGIN_SRC C++ :results verbatim :exports both #+BEGIN_SRC C++ :results verbatim :exports both
#include <iostream> #include <iostream>