degen: do not mark initial trivial SCCs as accepting

Doing so is not wrong, but it's superfluous, and the extra accepting
state will cause additional work in emptiness checks based on NDFS.
Report from Jan Strejček.

* src/tgbaalgos/degen.cc: Here.
* src/tgbatest/degenid.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2015-04-01 15:26:05 +02:00
parent 54a8ce502d
commit 6e8170e386
2 changed files with 36 additions and 0 deletions

View file

@ -72,6 +72,7 @@ namespace spot
acc_cond::mark_t common = a_->acc().all_sets();
acc_cond::mark_t union_ = 0U;
bool has_acc_self_loop = false;
bool seen = false;
for (auto& t: a_->out(s))
{
// Ignore transitions that leave the SCC of s.
@ -85,7 +86,10 @@ namespace spot
// an accepting self-loop?
has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc);
seen = true;
}
if (!seen)
common = 0U;
cache_[s] = std::make_tuple(common, union_, has_acc_self_loop);
}

View file

@ -222,3 +222,35 @@ EOF
run 0 ../../bin/dstar2tgba in.dra -BD --stats=%s > out.stat
test 6 = "`cat out.stat`"
# Only one state should be accepting. In spot 1.2.x an initial state
# in a trivial SCC was marked as accepting: this is superfluous.
../../bin/ltl2tgba -BH 'a & GFb & GFc' > out
cat out
cat >expected<<EOF
HOA: v1
name: "a & G(Fb & Fc)"
States: 4
Start: 0
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant
--BODY--
State: 0
[0] 1
State: 1 {0}
[1&2] 1
[!1&2] 2
[!2] 3
State: 2
[1] 1
[!1] 2
State: 3
[1&2] 1
[!1&2] 2
[!2] 3
--END--
EOF
diff out expected