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

@@ -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

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 \

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.

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

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]]

doc/org/tut11.org

+# -*- 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.