From 936990a42719aa96f1f49b22bf7dd3779273cd2d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 15 Mar 2019 14:05:36 +0100 Subject: [PATCH] org: more hyperlinks * doc/org/ltlfilt.org, doc/org/tut12.org: Add links. --- doc/org/ltlfilt.org | 3 +++ doc/org/tut12.org | 25 ++++++++++++++++++++----- 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 84335a641..d1b92a41c 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -285,6 +285,9 @@ ltldo ltl3ba -f '"proc@loc1" U "proc@loc2"' --spin This case also relabels the formula before calling =ltl3ba=, and it 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 =ltlfilt= supports many ways to filter formulas: diff --git a/doc/org/tut12.org b/doc/org/tut12.org index e2f3ac4b5..10641558b 100644 --- a/doc/org/tut12.org +++ b/doc/org/tut12.org @@ -60,8 +60,13 @@ initially, as required in the first paper... * Shell version The first four steps of the the above sequence of operations can be -executed as follows. Interpreting the resulting Büchi automaton as a -finite automaton is out of scope for Spot. +executed as follows. Transforming LTLf to LTL can be done using +[[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 ltlfilt --from-ltlf -f "(a U b) & Fc" | @@ -101,9 +106,14 @@ automaton is output. * Python version -In Python, we need to the =remove_ap()= object, which we must first -setup with some atomic propositions to remove. - +In Python, we use the =from_ltlf()= function to convert from LTLf to +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 import spot @@ -148,6 +158,11 @@ State: 3 {0} * 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 #include #include