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

org: fix some typos

Browse source 
* doc/org/tut12.org: Here.
This commit is contained in:
Alexandre Duret-Lutz 2020-03-04 23:22:21 +01:00
parent 3820f369b0
commit fa90a97d54
1 changed files with 11 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

15
doc/org/tut12.org
View file

@ -20,7 +20,7 @@ However there is a trick we can use in case we want to use Spot to
build a finite automaton that recognize some LTLf (i.e. LTL with build a finite automaton that recognize some LTLf (i.e. LTL with
finite semantics) property. The plan is as follows: finite semantics) property. The plan is as follows:
1. Have Spot read the input formula as if it were LTL. 1. Have Spot read the input LTLf formula as if it was LTL.
2. Rewrite this formula in a way that embeds the semantics of LTLf in 2. Rewrite this formula in a way that embeds the semantics of LTLf in
LTL. First, introduce a new atomic proposition =alive= that will LTL. First, introduce a new atomic proposition =alive= that will
be true initially, but that will eventually become false forever. be true initially, but that will eventually become false forever.
@ -62,7 +62,7 @@ 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 above sequence of operations can be
executed as follows. Transforming LTLf to LTL can be done using executed as follows. Transforming LTLf to LTL can be done using
[[file:ltlfilt.org][=ltlfilt=]]'s =--from-ltlf= option, translating the resulting formula [[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 into a Büchi automaton is obviously done with [[file:ltl2tgba.org][=ltl2tgba=]], and removing
@ -159,6 +159,10 @@ State: 3 {0}
--END-- --END--
#+end_example #+end_example
If you need to print the automaton in a custom format (some finite
automaton format probably), you should check our example of [[file:tut21.org][custom
print of an automaton]].
* C++ version * C++ version
The C++ version is straightforward adaptation of the Python version. The C++ version is straightforward adaptation of the Python version.
@ -226,9 +230,12 @@ State: 3 {0}
--END-- --END--
#+end_example #+end_example
* Final note Again, please check our example of [[file:tut21.org][custom print of an automaton]] if you
need to print in some format for NFA/DFA.
Spots only deal with infinite behaviors, so if you plan to use Spot to * Final notes
Spot only deals with infinite behaviors, so if you plan to use Spot to
perform some LTLf model checking, you should stop at step 3. Keep the perform some LTLf model checking, you should stop at step 3. Keep the
=alive= proposition in your property automaton, and also add it to the =alive= proposition in your property automaton, and also add it to the
Kripke structure representing your system. Kripke structure representing your system.