From 262668bbad3ba137a6984d000703e829e09d815d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 14 Mar 2019 22:55:45 +0100 Subject: [PATCH] org: add an example for dealing with LTLf formulas Related to issue #377. * doc/org/tut12.org: New file. * doc/org/tut.org, doc/Makefile.am, NEWS: Add the new file. --- NEWS | 3 + doc/Makefile.am | 1 + doc/org/tut.org | 1 + doc/org/tut12.org | 222 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 227 insertions(+) create mode 100644 doc/org/tut12.org diff --git a/NEWS b/NEWS index 983e88e24..c9e36f4e0 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,9 @@ New in spot 2.7.1.dev (not yet released) - A new page shows how to create explicit Kripke structures in C++ and Python. See https://spot.lrde.epita.fr/tut52.html + - Another new page shows how to deal with LTLf formulas (i.e., LTL + with finite semantics) and how to translate those. + See https://spot.lrde.epita.fr/tut12.html Python: diff --git a/doc/Makefile.am b/doc/Makefile.am index de8eac0ab..cfbd13c73 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -104,6 +104,7 @@ ORG_FILES = \ org/tut04.org \ org/tut10.org \ org/tut11.org \ + org/tut12.org \ org/tut20.org \ org/tut21.org \ org/tut22.org \ diff --git a/doc/org/tut.org b/doc/org/tut.org index 7e812b2f3..60b8f0344 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -25,6 +25,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[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:tut12.org][Working with LTL formula with finite semantics]] - [[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/tut12.org b/doc/org/tut12.org new file mode 100644 index 000000000..e2f3ac4b5 --- /dev/null +++ b/doc/org/tut12.org @@ -0,0 +1,222 @@ +# -*- coding: utf-8 -*- +#+TITLE: Working with LTL formula with finite semantics +#+DESCRIPTION: Code example for using Spot to translate LTLf formulas +#+INCLUDE: setup.org +#+HTML_LINK_UP: tut.html + +The LTL operators used by Spot are defined over infinite words, and +the various type of automata supported are all \omega-automata, i.e., +automata over infinite words. + +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 +finite semantics) property. The plan is as follows: + +#+name: from_ltlf +#+begin_src sh :results verbatim :exports none :var f="bug" +ltlfilt --from-ltlf -f "$f" +#+end_src + +1. Have Spot read the input formula as if it were LTL. +2. Rewrite this formula in a way that embeds the semantics of LTLf in + LTL. First, introduce a new atomic proposition =alive= that will + be true initially, but that will eventually become false forever. + Then adjust all original LTL operators so that they have to be + satisfied during the =alive= part of the word. For instance the + formula =(a U b) & Fc= would be transformed into + call_from_ltlf(f="(a U b) & Fc"). +3. Convert the resulting formula into a Büchi automaton: + #+name: tut12a + #+begin_src sh :results verbatim :exports none + ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B -d + #+end_src + #+BEGIN_SRC dot :file tut12a.svg :var txt=tut12a :exports results + $txt + #+END_SRC + #+RESULTS: + [[file:tut12a.svg]] +4. Remove the =alive= property, and, while we are at it, simplify the + Büchi automaton: + #+name: tut12b + #+begin_src sh :results verbatim :exports none + ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B | autfilt --remove-ap=alive -B --small -d + #+end_src + #+BEGIN_SRC dot :file tut12b.svg :var txt=tut12b :exports results + $txt + #+END_SRC + #+RESULTS: + [[file:tut12b.svg]] +5. Interpret the above automaton as finite automaton. (This part is + out of scope for Spot.) + +The above sequence of operations was described by De Giacomo & Vardi +in their [[https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf][IJCAI'13 paper]] and by Dutta & Vardi in their [[https://www.cs.rice.edu/~vardi/papers/memocode14a.pdf][Memocode'14 +paper]]. However, beware that the LTLf to LTL rewriting suggested in +theorem 1 of the [[https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf][IJCAI'13 paper]] has a typo (=t(φ₁ U φ₂)= should be +equal to =t(φ₁) U t(φ₂ & alive)=) that is fixed in the [[https://www.cs.rice.edu/~vardi/papers/memocode14a.pdf][Memocode'14 +paper]], but that second paper forgets to ensure that =alive= holds +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. + +#+begin_src sh :exports both :results verbatim +ltlfilt --from-ltlf -f "(a U b) & Fc" | + ltl2tgba -B | + autfilt --remove-ap=alive -B --small +#+end_src + +#+RESULTS: +#+begin_example +HOA: v1 +States: 4 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak +--BODY-- +State: 0 +[!2] 0 +[2] 3 +State: 1 +[0&!2] 0 +[!0&1&!2] 1 +[!0&1&2] 2 +[0&2] 3 +State: 2 +[!0&1] 2 +[0] 3 +State: 3 {0} +[t] 3 +--END-- +#+end_example + +Use =-B -D= instead of =-B= if you want to ensure that a deterministic +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. + + +#+begin_src python :results output :exports both +import spot +# Translate LTLf to Büchi. +aut = spot.from_ltlf('(a U b) & Fc').translate('ba') +# Remove "alive" atomic proposition +rem = spot.remove_ap() +rem.add_ap('alive') +aut = rem.strip(aut) +# Simplify result and print it. Use postprocess('ba', 'det') +# if you always want a deterministic automaton. +aut = spot.postprocess(aut, 'ba') +print(aut.to_str('hoa')) +#+end_src + +#+RESULTS: +#+begin_example +HOA: v1 +States: 4 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak +--BODY-- +State: 0 +[!2] 0 +[2] 3 +State: 1 +[0&!2] 0 +[!0&1&!2] 1 +[!0&1&2] 2 +[0&2] 3 +State: 2 +[!0&1] 2 +[0] 3 +State: 3 {0} +[t] 3 +--END-- +#+end_example + +* C++ version + +#+begin_src cpp :results verbatim :exports both + #include + #include + #include + #include + #include + #include + + int main() + { + spot::parsed_formula pf = spot::parse_infix_psl("(a U b) & Fc"); + if (pf.format_errors(std::cerr)) + return 1; + + spot::translator trans; + trans.set_type(spot::postprocessor::BA); + trans.set_pref(spot::postprocessor::Small); + spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f)); + + spot::remove_ap rem; + rem.add_ap("alive"); + aut = rem.strip(aut); + + spot::postprocessor post; + post.set_type(spot::postprocessor::BA); + post.set_pref(spot::postprocessor::Small); // or ::Deterministic + aut = post.run(aut); + + print_hoa(std::cout, aut) << '\n'; + return 0; + } +#+end_src + +#+RESULTS: +#+begin_example +HOA: v1 +States: 4 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak +--BODY-- +State: 0 +[!2] 0 +[2] 3 +State: 1 +[0&!2] 0 +[!0&1&!2] 1 +[!0&1&2] 2 +[0&2] 3 +State: 2 +[!0&1] 2 +[0] 3 +State: 3 {0} +[t] 3 +--END-- +#+end_example + +* Final note + +Spots only deal with infinite behaviors, so if you plan to use Spot to +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 +Kripke structure representing your system. + +Alternatively, if your Kripke structure is already equiped with some +=dead= property (as introduced by default in our [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin= interface]]), +you could replace =alive= by =!dead= by using ~ltlfilt +--from-ltl="!dead"~ (from the command-line), a running +=from_ltlf(f, "!dead")= in Python or C++.