diff --git a/NEWS b/NEWS index 42ad55dbc..113ec0fc4 100644 --- a/NEWS +++ b/NEWS @@ -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 be output in some cases (the result was still correct). + - 'ltl2tgba --any -C -M ...' would not complete automata. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 8381adc3f..118809f3d 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -921,32 +921,6 @@ $txt ltl2tgba -MD '(Xa & Fb) | Gc' -d #+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=] - 2 [label=<2>] - 2 -> 2 [label=] - 3 [label=<3>] - 3 -> 1 [label=] - 3 -> 4 [label=] - 4 [label=<4>] - 4 -> 0 [label=] - 4 -> 2 [label=] -} -#+end_example - #+BEGIN_SRC dot :file monitor2.png :cmdline -Tpng :var txt=monitor2 :exports results $txt #+END_SRC @@ -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 =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: ltlfilt filenames GraphViz vectorial pdf Tpdf dotex # LocalWords: sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 2191b8924..5b3f2ca29 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -227,20 +227,21 @@ namespace spot else strip_acceptance_here(a); - 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_) + if (PREF_ != Any) { - auto m = minimize_monitor(a); - if (m->num_states() < a->num_states()) - a = m; + if (PREF_ != Deterministic) + 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 (m->num_states() < a->num_states()) + a = m; + } + a->remove_unused_ap(); } - a->remove_unused_ap(); if (COMP_) a = complete(a); return a; diff --git a/tests/core/monitor.test b/tests/core/monitor.test index 504721c28..d21fb3c9d 100755 --- a/tests/core/monitor.test +++ b/tests/core/monitor.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -44,7 +44,7 @@ digraph G { } EOF -expect ltl2tgba --monitor a --hoa<