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

Make --keep-states more useful by actually removing states.

Browse source 
Fixes #70.

We don't modify the behavior of mask_keep_states(), because it is
actually useful in some algorithm to remove states without renumbering
all the other states.

* src/bin/autfilt.cc: Call purge_dead_states().
* src/tgbatest/maskkeep.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-03-25 21:29:42 +01:00
parent 23bcbb5b37
commit 483212d275
2 changed files with 12 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/bin/autfilt.cc
View file

@ -506,7 +506,10 @@ namespace
// Postprocessing.
if (!opt_keep_states.empty())
aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
{
aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
aut->purge_dead_states();
}
if (opt_mask_acc)
aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());

40
src/tgbatest/maskkeep.test
View file

@ -48,7 +48,7 @@ EOF
cat >expect1 <<EOF
HOA: v1
States: 4
States: 1
Start: 0
AP: 0
acc-name: generalized-Buchi 2
@ -56,25 +56,6 @@ Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
State: 1
State: 2
State: 3
--END--
EOF
cat >expect2 <<EOF
HOA: v1
States: 4
Start: 1
AP: 0
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
State: 1
State: 2
State: 3
--END--
EOF
@ -82,11 +63,11 @@ run 0 ../../bin/autfilt --keep-states=0 input1 -H >output
diff output expect1
run 0 ../../bin/autfilt --keep-states=1 input1 -H >output
diff output expect2
diff output expect1
cat >expect3 <<EOF
HOA: v1
States: 4
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
@ -100,27 +81,22 @@ State: 1
[0] 2
State: 2
[1] 1
State: 3
--END--
EOF
cat >expect4 <<EOF
HOA: v1
States: 4
Start: 1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0] 1 {0}
[1] 2 {1}
[0] 1
State: 1
[0] 2
State: 2
[1] 1
State: 3
[1] 0
--END--
EOF