Commit b4088271 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

add binding for language_containment_checker and document them

* spot/tl/contain.cc, spot/tl/contain.hh: Simplify the
use of language_containment_checker by adding default argument.
* python/spot/__init__.py, python/spot/impl.i: Bind it in Python.
* doc/org/tut04.org: New file to illustrate it.
* doc/org/tut.org, doc/Makefile.am: Add it.
* NEWS: Mention those changes.
parent 69cea65b
...@@ -38,7 +38,7 @@ New in spot 2.0.1a (not yet released) ...@@ -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 --eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options
these do not output scalable patterns, but simply a list of formulas these do not output scalable patterns, but simply a list of formulas
appearing in these three papers: Dwyer et al (FMSP'98), Etessami & 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: Library:
...@@ -53,6 +53,9 @@ New in spot 2.0.1a (not yet released) ...@@ -53,6 +53,9 @@ New in spot 2.0.1a (not yet released)
is_inherently_weak() will update the corresponding properties of is_inherently_weak() will update the corresponding properties of
the automaton as a side-effect of their check. the automaton as a side-effect of their check.
* language_containment_checker now has default values for all
parameters of its constructor.
Python: Python:
* The __format__() method for formula support the same * The __format__() method for formula support the same
...@@ -60,6 +63,13 @@ New in spot 2.0.1a (not yet released) ...@@ -60,6 +63,13 @@ New in spot 2.0.1a (not yet released)
So "{:[i]s}".format(f) is the same as So "{:[i]s}".format(f) is the same as
"{:s}".format(f.unabbreviate("i")). "{: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: Bug fixes:
* Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1 * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1
......
...@@ -96,6 +96,7 @@ ORG_FILES = \ ...@@ -96,6 +96,7 @@ ORG_FILES = \
org/tut01.org \ org/tut01.org \
org/tut02.org \ org/tut02.org \
org/tut03.org \ org/tut03.org \
org/tut04.org \
org/tut10.org \ org/tut10.org \
org/tut20.org \ org/tut20.org \
org/tut21.org \ org/tut21.org \
......
...@@ -22,6 +22,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. ...@@ -22,6 +22,7 @@ three interfaces supported by Spot: shell commands, Python, or C++.
- [[file:tut01.org][Parsing and Printing LTL Formulas]] - [[file:tut01.org][Parsing and Printing LTL Formulas]]
- [[file:tut02.org][Relabeling 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:tut10.org][Translating an LTL formula into a never claim]]
- [[file:tut20.org][Converting a never claim into HOA]] - [[file:tut20.org][Converting a never claim into HOA]]
- [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]] - [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]]
......
# -*- 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 <iostream>
#include <spot/tl/parse.hh>
#include <spot/tl/contain.hh>
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
...@@ -874,3 +874,7 @@ def sat_minimize(aut, acc=None, colored=False, ...@@ -874,3 +874,7 @@ def sat_minimize(aut, acc=None, colored=False,
def parse_word(word, dic=_bdd_dict): def parse_word(word, dic=_bdd_dict):
from spot.impl import parse_word as pw from spot.impl import parse_word as pw
return pw(word, dic) return pw(word, dic)
def language_containment_checker(dic=_bdd_dict):
from spot.impl import language_containment_checker as c
return c(dic)
...@@ -94,6 +94,7 @@ ...@@ -94,6 +94,7 @@
#include <spot/twa/bdddict.hh> #include <spot/twa/bdddict.hh>
#include <spot/tl/apcollect.hh> #include <spot/tl/apcollect.hh>
#include <spot/tl/contain.hh>
#include <spot/tl/dot.hh> #include <spot/tl/dot.hh>
#include <spot/tl/nenoform.hh> #include <spot/tl/nenoform.hh>
#include <spot/tl/print.hh> #include <spot/tl/print.hh>
...@@ -374,6 +375,7 @@ namespace std { ...@@ -374,6 +375,7 @@ namespace std {
%include <spot/twa/twa.hh> %include <spot/twa/twa.hh>
%include <spot/tl/apcollect.hh> %include <spot/tl/apcollect.hh>
%include <spot/tl/contain.hh>
%include <spot/tl/dot.hh> %include <spot/tl/dot.hh>
%include <spot/tl/nenoform.hh> %include <spot/tl/nenoform.hh>
%include <spot/tl/print.hh> %include <spot/tl/print.hh>
......
// -*- coding: utf-8 -*- // -*- 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). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
namespace spot namespace spot
{ {
language_containment_checker::language_containment_checker 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) bool branching_postponement, bool fair_loop_approx)
: dict_(dict), exprop_(exprop), symb_merge_(symb_merge), : dict_(dict), exprop_(exprop), symb_merge_(symb_merge),
branching_postponement_(branching_postponement), branching_postponement_(branching_postponement),
......
// -*- coding: utf-8 -*- // -*- 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). // et Développement de l'Epita (LRDE).
// Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
...@@ -42,10 +42,11 @@ namespace spot ...@@ -42,10 +42,11 @@ namespace spot
public: public:
/// This class uses spot::ltl_to_tgba_fm to translate LTL /// This class uses spot::ltl_to_tgba_fm to translate LTL
/// formulae. See that function for the meaning of these options. /// formulae. See that function for the meaning of these options.
language_containment_checker(const bdd_dict_ptr& dict, bool exprop, language_containment_checker(bdd_dict_ptr dict = make_bdd_dict(),
bool symb_merge, bool exprop = false,
bool branching_postponement, bool symb_merge = true,
bool fair_loop_approx); bool branching_postponement = false,
bool fair_loop_approx = false);
~language_containment_checker(); ~language_containment_checker();
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment