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

org: more hyperlinks

Browse source 
* doc/org/ltlfilt.org, doc/org/tut12.org: Add links.
This commit is contained in:
Alexandre Duret-Lutz 2019-03-15 14:05:36 +01:00
parent 262668bbad
commit 936990a427
2 changed files with 23 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
doc/org/ltlfilt.org
View file

@ -285,6 +285,9 @@ ltldo ltl3ba -f '"proc@loc1" U "proc@loc2"' --spin
This case also relabels the formula before calling =ltl3ba=, and it This case also relabels the formula before calling =ltl3ba=, and it
then rename all the atomic propositions in the output. then rename all the atomic propositions in the output.
An example showing how to use the =--from-ltlf= option is on [[file:tut12.org][a
separate page]].
* Filtering * Filtering
=ltlfilt= supports many ways to filter formulas: =ltlfilt= supports many ways to filter formulas:

25
doc/org/tut12.org
View file

@ -60,8 +60,13 @@ initially, as required in the first paper...
* Shell version * Shell version
The first four steps of the the above sequence of operations can be The first four steps of the the above sequence of operations can be
executed as follows. Interpreting the resulting Büchi automaton as a executed as follows. Transforming LTLf to LTL can be done using
finite automaton is out of scope for Spot. [[file:ltlfilt.org][=ltlfilt=]]'s =--from-ltlf= option, translating the resulting formula
into a Büchi automaton is obviously done with [[file:ltl2tgba.org][=ltl2tgba=]], and removing
an atomic proposition from an automaton can be done using [[file:autfilt.org][=autfilt=]]'s
=--remove-ap= option (adding =--small= will also simplify the
automaton). Interpreting the resulting Büchi automaton as a finite
automaton is out of scope for Spot.
#+begin_src sh :exports both :results verbatim #+begin_src sh :exports both :results verbatim
ltlfilt --from-ltlf -f "(a U b) & Fc" | ltlfilt --from-ltlf -f "(a U b) & Fc" |
@ -101,9 +106,14 @@ automaton is output.
* Python version * Python version
In Python, we need to the =remove_ap()= object, which we must first In Python, we use the =from_ltlf()= function to convert from LTLf to
setup with some atomic propositions to remove. LTL and translate the result into a Büchi automaton using
=translate()= [[file:tut10.org][as usual]]. Then we need to use the =remove_ap()= object,
which we must first setup with some atomic propositions to remove.
Finally we call the =postprocess()= function for automata
simplifications. (Note that =postprocess()= is already called by
=translate()=, but in this case removing the atomic proposition allows
more simplification opportunities.)
#+begin_src python :results output :exports both #+begin_src python :results output :exports both
import spot import spot
@ -148,6 +158,11 @@ State: 3 {0}
* C++ version * C++ version
The C++ version is straightforward adaptation of the Python version.
The Python functions =translate()= and =postprocess()= are convenient
wrappers around the =spot::translator= and =spot::postprocessor=
objects that we need to use here.
#+begin_src cpp :results verbatim :exports both #+begin_src cpp :results verbatim :exports both
#include <iostream> #include <iostream>
#include <spot/tl/parse.hh> #include <spot/tl/parse.hh>