simulation: do not mark codeterministic automata as deterministic
* src/tgbaalgos/simulation.cc: Here. * src/tgbatest/det.test: Test it.
This commit is contained in:
parent
a89b9d3678
commit
46d967945b
2 changed files with 9 additions and 2 deletions
|
|
@ -632,11 +632,10 @@ namespace spot
|
|||
true, // weakness preserved,
|
||||
false, // determinism checked and set below
|
||||
});
|
||||
if (nb_minato == nb_satoneset)
|
||||
if (nb_minato == nb_satoneset && !Cosimulation)
|
||||
res->prop_deterministic();
|
||||
if (Sba)
|
||||
res->prop_state_based_acc();
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -144,3 +144,11 @@ digraph G {
|
|||
}
|
||||
EOF
|
||||
diff out.tgba ex.tgba
|
||||
|
||||
|
||||
# This formula produce a co-deterministic automaton that is not deterministic,
|
||||
# and a bug in the cosimulation caused the result to be marked as deterministic.
|
||||
run 0 ../../bin/ltl2tgba -H '(0 R Xa) R (a xor Fa)' > out.hoa
|
||||
grep deterministic out.hoa && exit 1
|
||||
|
||||
true
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue