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

simulation: incorrect setting of non-deterministic property

Fixes #286.

* spot/twaalgos/simulation.cc: Only set the deterministic
property, not the non-deterministic one.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the issue.
parent a13a4e7d
......@@ -126,6 +126,9 @@ New in spot 2.4.0.dev (not yet released)
still correct outputs) depending on the BDD operations performed
before.
- spot::simulation() would occasionally incorrectly flag an
automaton as non-deterministic.
New in spot 2.4 (2017-09-06)
Build:
......
......@@ -582,7 +582,9 @@ namespace spot
res->set_init_state(gb->get_state(previous_class_
[a_->get_init_state_number()].id()));
res->merge_edges(); // FIXME: is this really needed?
res->merge_edges(); // This helps merging some edges with
// identical conditions, but different
// mark sets.
// Mark all accepting state in a second pass, when
// dealing with SBA in cosimulation.
......@@ -616,8 +618,10 @@ namespace spot
true, // stutter inv.
});
// !unambiguous and !semi-deterministic are not preserved
if (!Cosimulation)
res->prop_universal(nb_minato == nb_satoneset);
if (!Cosimulation && nb_minato == nb_satoneset)
// Note that nb_minato != nb_satoneset does not imply
// non-deterministic, because of the merge_edges() above.
res->prop_universal(true);
if (Sba)
res->prop_state_acc(true);
return res;
......
......@@ -265,3 +265,8 @@ ltl2tgba -xsimul=1 --low "$f1" "$f2" > res2
diff res1 res2
test 3 = `ltl2tgba -f 'G(Fa & Fb) U a' --stats=%s`
# issue #286, the following automaton caused the print_hoa() function to
# report inconsistent "universal" property.
ltl2tgba --low 'X(((1) U (p1)) | (((p1) | (F(p0))) U ((0) R ((p2) M (p1)))))'>o
grep deterministic o
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