alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sat: add missing prop_state_based_acc() call

Browse source 
Fixes #62.

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Add call to
prop_state_based_acc() when building an automaton with state-based
acceptance.
* src/tgbatest/satmin2.test: New test.
* doc/org/satmin.org: Update.
This commit is contained in:
Alexandre Duret-Lutz 2015-03-17 18:29:28 +01:00
parent 6712fa3c65
commit 72eed9b2e2
4 changed files with 17 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tgbatest/satmin2.test
View file

@ -57,3 +57,9 @@ EOF
../ltl2tgba -RS1 -kt -XH input.hoa > output
diff output expected
# At some point, this formula was correctly minimized, but
# the output was not marked as state-based.
../../bin/ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out
grep 'properties:.*state-acc' out
grep 'properties:.*deterministic' out