From e7f5af6c6a3b02a6e112c189a848e7fbaac0c554 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 7 Jun 2015 15:13:41 +0200 Subject: [PATCH] org: add example of LTL->BA translation This addresses one item in #14. * doc/org/tut10.org: New file. * doc/Makefile.am: Add it. * src/twaalgos/translate.hh: Fix inclusion of types from postprocessor. * wrap/python/spot.py (translate): Fix typo in doc string. --- doc/Makefile.am | 1 + doc/org/tut10.org | 213 ++++++++++++++++++++++++++++++++++++++ src/twaalgos/translate.hh | 6 +- wrap/python/spot.py | 2 +- 4 files changed, 219 insertions(+), 3 deletions(-) create mode 100644 doc/org/tut10.org diff --git a/doc/Makefile.am b/doc/Makefile.am index 59adeb6f2..a7cd88c82 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -80,6 +80,7 @@ ORG_FILES = \ org/tools.org \ org/tut01.org \ org/tut02.org \ + org/tut10.org \ org/satmin.org \ org/satmin.tex \ org/setup.org \ diff --git a/doc/org/tut10.org b/doc/org/tut10.org new file mode 100644 index 000000000..c709705f7 --- /dev/null +++ b/doc/org/tut10.org @@ -0,0 +1,213 @@ +#+TITLE: Translating an LTL formula into a never claim +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +Here is how to translate an LTL (or PSL) formula into a never claim. + +* Shell + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba --spin 'GFa -> GFb' +#+END_SRC + +#+RESULTS: +#+begin_example +never { /* F(GFb | G!a) */ +T0_init: + if + :: ((!(a))) -> goto accept_S0 + :: ((true)) -> goto T0_init + :: ((b)) -> goto accept_S2 + fi; +accept_S0: + if + :: ((!(a))) -> goto accept_S0 + fi; +accept_S2: + if + :: ((b)) -> goto accept_S2 + :: ((!(b))) -> goto T0_S3 + fi; +T0_S3: + if + :: ((b)) -> goto accept_S2 + :: ((!(b))) -> goto T0_S3 + fi; +} +#+end_example + +* Python + +The =formula= function returns a formula object (or raises a +parse-error exception). Formula objects have a =translate()= method +that returns an automaton, and the automata objects have a =to_str= +method that can output in one of the supported syntaxes. + +So the translation is actually a one-liner in Python: + +#+BEGIN_SRC python :results output :exports both +import spot +print(spot.formula('GFa -> GFb').translate('BA').to_str('spin')) +#+END_SRC + +#+RESULTS: +#+begin_example +never { +T0_init: + if + :: ((!(a))) -> goto accept_S0 + :: ((true)) -> goto T0_init + :: ((b)) -> goto accept_S2 + fi; +accept_S0: + if + :: ((!(a))) -> goto accept_S0 + fi; +accept_S2: + if + :: ((b)) -> goto accept_S2 + :: ((!(b))) -> goto T0_S3 + fi; +T0_S3: + if + :: ((b)) -> goto accept_S2 + :: ((!(b))) -> goto T0_S3 + fi; +} + +#+end_example + +The above line can actually be made a bit shorter, because +=translate()= can also be used as a function (as opposed to a method) +that take a formula (possibly as a string) as first argument: + +#+BEGIN_SRC python :results output :exports both +import spot +print(spot.translate('GFa -> GFb', 'BA').to_str('spin')) +#+END_SRC + +#+RESULTS: +#+begin_example +never { +T0_init: + if + :: ((!(a))) -> goto accept_S0 + :: ((true)) -> goto T0_init + :: ((b)) -> goto accept_S2 + fi; +accept_S0: + if + :: ((!(a))) -> goto accept_S0 + fi; +accept_S2: + if + :: ((b)) -> goto accept_S2 + :: ((!(b))) -> goto T0_S3 + fi; +T0_S3: + if + :: ((b)) -> goto accept_S2 + :: ((!(b))) -> goto T0_S3 + fi; +} + +#+end_example + +* C++ + +All the translation pipeline (this include simplifying the formula, +translating the simplified formula into an automaton, and simplifying +the resulting automaton) is handled by the =spot::translator= object. +This object can configured by calling =set_type()= to chose the type +of automaton to output, =set_level()= to set the level of optimization +(it's high by default), and =set_pref()= to set various preferences +(like small or deterministic) or characteristic (complete, +unambiguous) for the resulting automaton. Finally, the output as a +never claim is done via the =print_never_claim= function. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include "ltlparse/public.hh" + #include "ltlvisit/print.hh" + #include "twaalgos/translate.hh" + #include "twaalgos/neverclaim.hh" + + int main() + { + std::string input = "[]<>p0 || <>[]p1"; + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel); + if (spot::ltl::format_parse_errors(std::cerr, input, pel)) + { + if (f) + f->destroy(); + return 1; + } + spot::translator trans; + trans.set_type(spot::postprocessor::BA); + spot::twa_graph_ptr aut = trans.run(f); + print_never_claim(std::cout, aut) << '\n'; + f->destroy(); + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +never { +T0_init: + if + :: ((p1)) -> goto accept_S0 + :: ((true)) -> goto T0_init + :: ((p0)) -> goto accept_S2 + fi; +accept_S0: + if + :: ((p1)) -> goto accept_S0 + fi; +accept_S2: + if + :: ((p0)) -> goto accept_S2 + :: ((!(p0))) -> goto T0_S3 + fi; +T0_S3: + if + :: ((p0)) -> goto accept_S2 + :: ((!(p0))) -> goto T0_S3 + fi; +} +#+end_example + +* Additional comments + +The Python version of =translate()= is documented as follows: + +#+BEGIN_SRC python :results output :exports both +import spot +help(spot.translate) +#+END_SRC + +#+RESULTS: +#+begin_example +Help on function translate in module spot: + +translate(formula, *args) + Translate a formula into an automaton. + + Keep in mind that pref expresses just a preference that may not be + satisfied. + + The optional arguments should be strings among the following: + - at most one in 'TGBA', 'BA', or 'Monitor' + (type of automaton to build) + - at most one in 'Small', 'Deterministic', 'Any' + (preferred characteristics of the produced automaton) + - at most one in 'Low', 'Medium', 'High' + (optimization level) + - any combination of 'Complete', 'Unambiguous', and + 'StateBasedAcceptance' (or 'SBAcc' for short) + + The default correspond to 'tgba', 'small' and 'high'. + +#+end_example diff --git a/src/twaalgos/translate.hh b/src/twaalgos/translate.hh index dc00aa2f7..e7673728d 100644 --- a/src/twaalgos/translate.hh +++ b/src/twaalgos/translate.hh @@ -74,7 +74,7 @@ namespace spot delete simpl_owned_; } - typedef postprocessor::output_type output_type; + using postprocessor::output_type; void set_type(output_type type) @@ -82,13 +82,15 @@ namespace spot this->postprocessor::set_type(type); } + using postprocessor::output_pref; + void set_pref(output_pref pref) { this->postprocessor::set_pref(pref); } - typedef postprocessor::optimization_level optimization_level; + using postprocessor::optimization_level; void set_level(optimization_level level) diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 075177170..275e8306c 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -229,7 +229,7 @@ def translate(formula, *args): - at most one in 'TGBA', 'BA', or 'Monitor' (type of automaton to build) - at most one in 'Small', 'Deterministic', 'Any' - (perefered characteristics of the produced automaton) + (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' (optimization level) - any combination of 'Complete', 'Unambiguous', and