From 0df785bcde02459b617af1fb5081b0aa555ef6e9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Mar 2017 17:36:31 +0100 Subject: [PATCH] doc: add an example about how to build monitor in shell/python/C++ Part of #239. * doc/org/tut11.org: New file. * doc/org/ltl2tgba.org, doc/org/hierarchy.org: Add some anchors we can link to in tut11.org. * doc/org/tut.org, doc/Makefile.am: Add tut11.org. * NEWS: Mention the new page. --- NEWS | 5 + doc/Makefile.am | 1 + doc/org/hierarchy.org | 3 + doc/org/ltl2tgba.org | 5 + doc/org/tut.org | 1 + doc/org/tut11.org | 289 ++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 304 insertions(+) create mode 100644 doc/org/tut11.org diff --git a/NEWS b/NEWS index 977f5afd5..79559b92f 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,11 @@ New in spot 2.3.1.dev (not yet released) atomic propositions instead of conting them. Tools that output formulas also support --format=%x for this purpose. + Documentation: + + - https://spot.lrde.epita.fr/tut11.html is a new page describing + how to build monitors in Shell, Python, or C++. + Bugs fixed: - The tests using LTSmin's patched version of divine would fail diff --git a/doc/Makefile.am b/doc/Makefile.am index c98f07661..917a50afe 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -105,6 +105,7 @@ ORG_FILES = \ org/tut03.org \ org/tut04.org \ org/tut10.org \ + org/tut11.org \ org/tut20.org \ org/tut21.org \ org/tut22.org \ diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index d8e656c11..4bbde1e82 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -427,6 +427,9 @@ $txt ** Safety + :PROPERTIES: + :CUSTOM_ID: safety + :END: /Safety/ properties also form a subclass of /obligation/ properties, and again there is no code specific to them in the translation. diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 118809f3d..f2f04185e 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -870,6 +870,9 @@ more restricted labels. files are on a separate page]]. * Building Monitors + :PROPERTIES: + :CUSTOM_ID: monitors + :END: In addition to TGBA and BA, =ltl2tgba= can output /monitor/ using the =-M= option. These are finite automata that accept all prefixes of a @@ -933,6 +936,8 @@ match the formula, monitor cannot be used to check for eventualities such as =F(a)=: indeed, any finite execution can be extended to match =F(a)=. +For more discussion and examples about monitor, see also our [[file:tut11.org][separate +page showing how to build them in Python and C++]]. Because Monitors accept every recognized run (in other words, they only reject words that are not recognized), it makes little sense to diff --git a/doc/org/tut.org b/doc/org/tut.org index d799d0cdc..1afad5011 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -24,6 +24,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[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:tut11.org][Translating an LTL formula into a monitor]] - [[file:tut20.org][Converting a never claim into HOA]] - [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]] - [[file:tut31.org][Removing alternation]] diff --git a/doc/org/tut11.org b/doc/org/tut11.org new file mode 100644 index 000000000..beb9433ec --- /dev/null +++ b/doc/org/tut11.org @@ -0,0 +1,289 @@ +# -*- coding: utf-8 -*- +#+TITLE: Translating an LTL formula into a monitors +#+DESCRIPTION: Code example for using Spot to translating formulas in monitors +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +A monitor is a special type of automaton that is supposed to /monitor/ +a running system and move accordingly. A monitor detects an error +when it cannot move: i.e., the system as performed some action, or +reached some state that is not supposed to happen. + +For instance here is a monitor that checks that *yellow* never occurs +immediately after *red*. + +#+NAME: tut11a +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -D -M '!F(red & Xyellow)' -d +#+END_SRC + +#+BEGIN_SRC dot :file tut11a.png :cmdline -Tpng :var txt=tut11a :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:tut11a.png]] + +This monitor stays in the initial state until *red* becomes true, it +can then wait in the second state while *red* holds and *yellow* does +not,, and will only move back to the initial state when both *red* and +*yellow* are false. The only way this monitor would not be able to +progress is if *yellow* becomes true while in the second state; in +that case a violation should be reported. + + +* Building a deterministic monitor + +** Shell + +To build the above deterministic monitor using [[file:ltl2tgba.org][=ltl2tgba=]], we simply +pass option =-M= (for monitor) and =-D= (for deterministic). + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -D -M '!F(red & X(yellow))' +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +name: "G(!red | X!yellow)" +States: 2 +Start: 0 +AP: 2 "red" "yellow" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[!0&!1] 0 +[0&!1] 1 +--END-- +#+end_example + +** Python + +The code is very similar to [[file:tut10.org][our previous example of building a never +claim]] except that we explicitly require a deterministic monitor and +output in the [[file:hoa.org][HOA format]]. + +#+BEGIN_SRC python :results output :exports both +import spot +print(spot.translate('!F(red & X(yellow))', 'monitor', 'det').to_str('HOA')) +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 2 +Start: 0 +AP: 2 "red" "yellow" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[!0&!1] 0 +[0&!1] 1 +--END-- +#+end_example + +** C++ + +The code very similar to [[file:tut10.org][the never claim example]]. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include + #include + + int main() + { + spot::parsed_formula pf = spot::parse_infix_psl("!F(red & X(yellow))"); + if (pf.format_errors(std::cerr)) + return 1; + spot::translator trans; + trans.set_type(spot::postprocessor::Monitor); + trans.set_pref(spot::postprocessor::Deterministic); + spot::twa_graph_ptr aut = trans.run(pf.f); + print_hoa(std::cout, aut) << '\n'; + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 2 +Start: 0 +AP: 2 "red" "yellow" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[!0&!1] 0 +[0&!1] 1 +--END-- +#+end_example + + +* Non-deterministic monitors + +If you drop the =-D= option from =ltl2tgba=, or the =det= argument +from =spot.translate()=, or the +=set_pref(spot::postprocessor::Deterministic)= in C++, then a +non-deterministic monitor can be output. By default Spot will build +both a deterministic and a non-deterministic monitor, it will output +the smallest one. + +* Details + +** Expressiveness + +In the [[file:hierarchy.org][hierarchy of temporal properties]], the properties that are +monitorable correspond to the class of [[file:hierarchy.org::#safety][safety properties]]. You can +check that an LTL formula is a safety by using: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt --count --safety -f '!F(red & X(yellow))' +#+END_SRC + +#+RESULTS: +: 1 + +(This asks [[file:ltlfilt.org][=ltlfilt=]] to count the number of safety formulas among +those---only one here---that were passed.) + +For properties that are not safety properties, the monitors built +recognize the smallest safety property that contain the original +languages. + +For instance if we want to ensure that whenever we press a button, the +red light will be on until the green light is on, we would use the +following formula: =G(press -> red U green)=. Unfortunately it is not +a safety property: + +#+BEGIN_SRC sh :results verbatim :exports code +ltlfilt --count --safety -f 'G(press -> red U green)' +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +ltlfilt --count --safety -f 'G(press -> red U green)' +true +#+END_SRC + +#+RESULTS: +: 0 + +Nonetheless, we can still build a monitor for it: + +#+NAME: tut11b +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -D -M 'G(press -> red U green)' -d +#+END_SRC +#+BEGIN_SRC dot :file tut11b.png :cmdline -Tpng :var txt=tut11b :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:tut11b.png]] + + +This monitor will report violations if both *red* and *green* are off +when the button is pressed, and also if *red* goes off without *green* +going on. However note that in the original formula, =red U green= +implies that *green* will eventually become true, and the monitor +cannot ensure that: a system where *red* is continuously on, and +*green* is continuously off would not trigger any violation. The +monitor that has been built here actually represents the safety +property =G(press -> red W green)=, and accepts a bit more than +our original property =G(press -> red U green)=. + +** Construction & References + +The construction of deterministic monitors in Spot follows the +construction of M. d'Amorim and G. Roşu ([[https://www.ideals.illinois.edu/bitstream/handle/2142/10975/Efficient%20Monitoring%20of%20%CF%89-languages.pdf][Efficient monitoring of +ω-languages]]. CAV’05) as described by D. Tabakov and M. Y. Vardi +([[https://www.cs.rice.edu/~vardi/papers/rv10rj.pdf][Optimized Temporal Monitors for SystemC]]. RV’10) with a minor +optimization: instead of starting from a Büchi automaton we start from +a Transition-based Generalized Büchi automaton. + +The construction steps are: +1. translate the LTL formula into a TGBA +2. remove SCCs that cannot reach an accepting cycle +3. strip the acceptance condition +4. determinize the automaton (using a classical powerset) +5. minimize the automaton (using standard DFA minimization) + +When non-deterministic monitors are required, the last two steps +are replaced by a pass of simulation-based reductions. + + +The following code shows how to implement the above five steps in C++ +without using =spot::translator=. Unless you plan to customize some +of these steps, we recommend you use =spot::translator= instead. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include + #include + #include + #include + #include + + int main() + { + spot::parsed_formula pf = spot::parse_infix_psl("G(press -> red U green)"); + if (pf.format_errors(std::cerr)) + return 1; + // 1. translate LTL formula into TGBA + spot::twa_graph_ptr aut = spot::ltl_to_tgba_fm(pf.f, spot::make_bdd_dict()); + // 2. remove "dead" SCCs + aut = spot::scc_filter(aut); + // 3. strip the acceptance condition (in place) + spot::strip_acceptance_here(aut); + // 4. & 5. determinize and minimize the automaton + aut = spot::minimize_monitor(aut); + // output the result. + print_hoa(std::cout, aut) << '\n'; + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 2 +Start: 1 +AP: 3 "press" "red" "green" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak +--BODY-- +State: 0 +[1&!2] 0 +[2] 1 +State: 1 +[0&1&!2] 0 +[!0 | 2] 1 +--END-- +#+end_example + +* Further reading + +If your application requires monitors and you plan to build them with +Spot, it is very likely that you will want to convert the resulting +automata to your own data structure. See [[file:tut21.org][how to print an automaton in +a custom format]] to learn all you need to iterate over Spot's automata.