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

stutter: improve closure

Browse source 
if a transition with the same label already exist, reuse it

* src/tgbaalgos/stutter.cc: Here.
* src/tgbatest/stutter.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2015-03-31 19:18:41 +02:00
parent 2f42c1c9bf
commit a18327d488
2 changed files with 44 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/tgbaalgos/stutter.cc
View file

@ -487,13 +487,27 @@ namespace spot
{ {
if (!bdd_implies(cond, ts.cond)) if (!bdd_implies(cond, ts.cond))
{ {
ts.cond = ts.cond | cond; ts.cond |= cond;
if (std::find(todo.begin(), todo.end(), t) if (std::find(todo.begin(), todo.end(), t)
== todo.end()) == todo.end())
todo.push_back(t); todo.push_back(t);
} }
need_new_trans = false; need_new_trans = false;
break;
} }
else if (cond == ts.cond)
{
acc |= ts.acc;
if (ts.acc != acc)
{
ts.acc = acc;
if (std::find(todo.begin(), todo.end(), t)
== todo.end())
todo.push_back(t);
}
need_new_trans = false;
break;
}
} }
if (need_new_trans) if (need_new_trans)
{ {

33
src/tgbatest/stutter.test
View file

@ -42,7 +42,32 @@ $autfilt --states=12 prod.hoa -q
# #
# We just run those without checking the output, it is enough to # We just run those without checking the output, it is enough to
# trigger assertions in the HOA output routines. # trigger assertions in the HOA output routines.
run 0 ../../bin/ltl2tgba -H 'X(a U b)' > det.hoa run 0 $ltl2tgba -H 'X(a U b)' > det.hoa
run 0 ../../bin/autfilt --destut det.hoa -H run 0 $autfilt --destut det.hoa -H
run 0 ../../bin/autfilt --instut=1 det.hoa -H run 0 $autfilt --instut=1 det.hoa -H
run 0 ../../bin/autfilt --instut=2 det.hoa -H run 0 $autfilt --instut=2 det.hoa -H
$ltl2tgba -H 'a & Fb' | $autfilt --destut -H > output
cat >expected <<EOF
HOA: v1
name: "a & Fb"
States: 3
Start: 2
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[t] 0 {0}
State: 1
[1] 0 {0}
[!1] 1
State: 2
[0&1] 0 {0}
[0&!1] 1
--END--
EOF
diff output expected