Commit 0df785bc authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 9defdad2
......@@ -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
......
......@@ -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 \
......
......@@ -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.
......
......@@ -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
......
......@@ -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]]
......
# -*- 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 <iostream>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/hoa.hh>
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 <iostream>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/stripacc.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/hoa.hh>
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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment