Commit 0621e0e9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

monitor: fix -MD/-M difference in property output

Fixes #241.

* spot/twaalgos/postproc.cc: Use the deterministic monitor if it
has as many states as the non-deterministic one.
* spot/twaalgos/minimize.cc (minimize_monitor): Quickly check
for terminal automata.
* spot/twaalgos/stripacc.cc: Set the weak property.
* spot/twaalgos/stripacc.hh: Improve documentation.
* tests/core/monitor.test, tests/core/sbacc.test: Update.
* NEWS: Mention the issue.
parent 28f4e4b9
...@@ -30,6 +30,11 @@ New in spot 2.3.1.dev (not yet released) ...@@ -30,6 +30,11 @@ New in spot 2.3.1.dev (not yet released)
- 'ltl2tgba --any -C -M ...' would not complete automata. - 'ltl2tgba --any -C -M ...' would not complete automata.
- while not incorrect, the HOA properties output by 'ltl2tgba -M'
could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D'
would always report 'weak' automata. Both variants now report the
most precise between 'weak' or 'terminal'.
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
......
...@@ -490,6 +490,13 @@ namespace spot ...@@ -490,6 +490,13 @@ namespace spot
res->prop_deterministic(true); res->prop_deterministic(true);
res->prop_weak(true); res->prop_weak(true);
res->prop_state_acc(true); res->prop_state_acc(true);
// Quickly check if this is a terminal automaton
for (auto& e: res->edges())
if (e.src == e.dst && e.cond == bddtrue)
{
res->prop_terminal(true);
break;
}
return res; return res;
} }
......
...@@ -234,10 +234,11 @@ namespace spot ...@@ -234,10 +234,11 @@ namespace spot
// For Small,High we return the smallest between the output of // For Small,High we return the smallest between the output of
// the simulation, and that of the deterministic minimization. // the simulation, and that of the deterministic minimization.
// Prefer the deterministic automaton in case of equality.
if (PREF_ == Small && level_ == High && simul_) if (PREF_ == Small && level_ == High && simul_)
{ {
auto m = minimize_monitor(a); auto m = minimize_monitor(a);
if (m->num_states() < a->num_states()) if (m->num_states() <= a->num_states())
a = m; a = m;
} }
a->remove_unused_ap(); a->remove_unused_ap();
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et // Copyright (C) 2012, 2014, 2015, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -30,5 +30,6 @@ namespace spot ...@@ -30,5 +30,6 @@ namespace spot
t.acc = 0U; t.acc = 0U;
a->set_generalized_buchi(0); a->set_generalized_buchi(0);
a->release_named_properties(); a->release_named_properties();
a->prop_weak(true);
} }
} }
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et // Copyright (C) 2012-2014, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -26,7 +26,9 @@ namespace spot ...@@ -26,7 +26,9 @@ namespace spot
/// \ingroup twa_misc /// \ingroup twa_misc
/// \brief Remove all acceptance sets from a twa_graph. /// \brief Remove all acceptance sets from a twa_graph.
/// ///
/// This is equivalent to marking all states/transitions as accepting. /// This will also set the acceptance condition to true, and mark
/// the automaton as weak. Doing so obviously makes all recognized
/// infinite runs accepting.
SPOT_API void SPOT_API void
strip_acceptance_here(twa_graph_ptr a); strip_acceptance_here(twa_graph_ptr a);
} }
...@@ -44,7 +44,7 @@ digraph G { ...@@ -44,7 +44,7 @@ digraph G {
} }
EOF EOF
expect ltl2tgba --monitor a GFa --hoa<<EOF expect ltl2tgba --monitor a GFa Ga --hoa<<EOF
HOA: v1 HOA: v1
name: "a" name: "a"
States: 2 States: 2
...@@ -68,11 +68,24 @@ AP: 0 ...@@ -68,11 +68,24 @@ AP: 0
acc-name: all acc-name: all
Acceptance: 0 t Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant properties: deterministic stutter-invariant terminal
--BODY-- --BODY--
State: 0 State: 0
[t] 0 [t] 0
--END-- --END--
HOA: v1
name: "Ga"
States: 1
Start: 0
AP: 1 "a"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant weak
--BODY--
State: 0
[0] 0
--END--
EOF EOF
# Completing a monitor can produce a Büchi automaton. # Completing a monitor can produce a Büchi automaton.
...@@ -85,7 +98,7 @@ AP: 1 "a" ...@@ -85,7 +98,7 @@ AP: 1 "a"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant inherently-weak properties: deterministic stutter-invariant weak
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[0] 0 [0] 0
......
...@@ -141,7 +141,7 @@ Start: 0 ...@@ -141,7 +141,7 @@ Start: 0
AP: 1 "a" AP: 1 "a"
acc-name: all acc-name: all
Acceptance: 0 t Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic properties: trans-labels explicit-labels state-acc deterministic weak
--BODY-- --BODY--
State: 0 State: 0
[0] 1 [0] 1
......
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