Commit 2b9accdf authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

postproc: fix monitor code

Fixes #240.

* spot/twaalgos/postproc.cc: Do not call do_simul on the output of
minimize_monitor(), and do not skip complete() when PREF_==Any.
* tests/core/monitor.test: Add a test case.
* NEWS: Mention the bug.
* doc/org/ltl2tgba.org: Document complete monitors.
parent cf5d2c2b
...@@ -23,6 +23,8 @@ New in spot 2.3.1.dev (not yet released) ...@@ -23,6 +23,8 @@ New in spot 2.3.1.dev (not yet released)
to state-based acceptance could cause a superfluous initial state to state-based acceptance could cause a superfluous initial state
to be output in some cases (the result was still correct). to be output in some cases (the result was still correct).
- 'ltl2tgba --any -C -M ...' would not complete automata.
Deprecation notices: Deprecation notices:
- Using --format=%a to print the number of atomic propositions in - Using --format=%a to print the number of atomic propositions in
......
...@@ -921,32 +921,6 @@ $txt ...@@ -921,32 +921,6 @@ $txt
ltl2tgba -MD '(Xa & Fb) | Gc' -d ltl2tgba -MD '(Xa & Fb) | Gc' -d
#+END_SRC #+END_SRC
#+RESULTS: monitor2
#+begin_example
digraph G {
rankdir=LR
node [shape="circle"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, width=0]
I -> 3
0 [label=<0>]
0 -> 0 [label=<1>]
1 [label=<1>]
1 -> 0 [label=<a>]
2 [label=<2>]
2 -> 2 [label=<c>]
3 [label=<3>]
3 -> 1 [label=<!c>]
3 -> 4 [label=<c>]
4 [label=<4>]
4 -> 0 [label=<a>]
4 -> 2 [label=<!a &amp; c>]
}
#+end_example
#+BEGIN_SRC dot :file monitor2.png :cmdline -Tpng :var txt=monitor2 :exports results #+BEGIN_SRC dot :file monitor2.png :cmdline -Tpng :var txt=monitor2 :exports results
$txt $txt
#+END_SRC #+END_SRC
...@@ -959,6 +933,29 @@ match the formula, monitor cannot be used to check for eventualities ...@@ -959,6 +933,29 @@ match the formula, monitor cannot be used to check for eventualities
such as =F(a)=: indeed, any finite execution can be extended to match such as =F(a)=: indeed, any finite execution can be extended to match
=F(a)=. =F(a)=.
Because Monitors accept every recognized run (in other words, they
only reject words that are not recognized), it makes little sense to
use option =-C= to request /complete/ monitors. If uou combine =-C=
with =-M=, the result will output as a Büchi automaton if (and only
if) a sink state had to be added. For instance, here is the
"complete" version of the previous monitor.
#+NAME: monitor3
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -C -M -D '(Xa & Fb) | Gc' -d
#+END_SRC
#+BEGIN_SRC dot :file monitor3.png :cmdline -Tpng :var txt=monitor3 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:monitor3.png]]
# LocalWords: ltl tgba num toc PSL Büchi automata SRC GFb invis Acc # LocalWords: ltl tgba num toc PSL Büchi automata SRC GFb invis Acc
# LocalWords: ltlfilt filenames GraphViz vectorial pdf Tpdf dotex # LocalWords: ltlfilt filenames GraphViz vectorial pdf Tpdf dotex
# LocalWords: sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb # LocalWords: sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb
......
...@@ -227,20 +227,21 @@ namespace spot ...@@ -227,20 +227,21 @@ namespace spot
else else
strip_acceptance_here(a); strip_acceptance_here(a);
if (PREF_ == Any) if (PREF_ != Any)
return a;
a = do_simul(a, simul_);
// For Small,High we return the smallest between the output of
// the simulation, and that of the deterministic minimization.
if (PREF_ == Small && level_ == High && simul_)
{ {
auto m = minimize_monitor(a); if (PREF_ != Deterministic)
if (m->num_states() < a->num_states()) a = do_simul(a, simul_);
a = m;
// For Small,High we return the smallest between the output of
// the simulation, and that of the deterministic minimization.
if (PREF_ == Small && level_ == High && simul_)
{
auto m = minimize_monitor(a);
if (m->num_states() < a->num_states())
a = m;
}
a->remove_unused_ap();
} }
a->remove_unused_ap();
if (COMP_) if (COMP_)
a = complete(a); a = complete(a);
return a; return a;
......
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et # Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de
# Développement de l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
...@@ -44,7 +44,7 @@ digraph G { ...@@ -44,7 +44,7 @@ digraph G {
} }
EOF EOF
expect ltl2tgba --monitor a --hoa<<EOF expect ltl2tgba --monitor a GFa --hoa<<EOF
HOA: v1 HOA: v1
name: "a" name: "a"
States: 2 States: 2
...@@ -60,9 +60,6 @@ State: 0 ...@@ -60,9 +60,6 @@ State: 0
State: 1 State: 1
[0] 0 [0] 0
--END-- --END--
EOF
expect ltl2tgba --monitor GFa --hoa<<EOF
HOA: v1 HOA: v1
name: "GFa" name: "GFa"
States: 1 States: 1
...@@ -77,3 +74,23 @@ State: 0 ...@@ -77,3 +74,23 @@ State: 0
[t] 0 [t] 0
--END-- --END--
EOF EOF
# Completing a monitor can produce a Büchi automaton.
expect ltl2tgba --any -C -M Ga <<EOF
HOA: v1
name: "Ga"
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant inherently-weak
--BODY--
State: 0 {0}
[0] 0
[!0] 1
State: 1
[t] 1
--END--
EOF
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