Commit 9377db2e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

sbacc: fix a serious bug

Reported by Thibaud Michaud

* spot/twaalgos/sbacc.cc: Do not label rejecting SCCs with the empty
mark, as it might be accepting.
* tests/core/sbacc.test: Add test cases.
* NEWS: Mention the bug.
parent cb920242
......@@ -20,6 +20,11 @@ New in spot 2.3.3.dev (not yet released)
- spot::dtwa_complement now simply returns the result of dualize()
Bugs fixed:
- the transformation to state-based acceptance (spot::sbacc()) was
incorrect on automata where the empty acceptance mark is accepting.
Backward-incompatible changes:
- spot::acc_cond::mark_t::operator bool() has been marked as
......
......@@ -22,6 +22,7 @@
#include <utility>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/stripacc.hh>
namespace spot
{
......@@ -33,6 +34,18 @@ namespace spot
throw std::runtime_error
("sbacc() does not support alternation");
// We will need a mark that is rejecting to mark rejecting states.
// If no such mark exist, our work is actually quite simple: we
// just have to copy the automaton and give it "t" as acceptance
// condition.
auto unsat_mark = old->acc().unsat_mark();
if (!unsat_mark.first)
{
auto res = make_twa_graph(old, twa::prop_set::all());
strip_acceptance_here(res);
return res;
}
scc_info si(old);
unsigned ns = old->num_states();
......@@ -97,7 +110,7 @@ namespace spot
{
unsigned scc_dst = si.scc_of(t.dst);
acc_cond::mark_t acc = 0U;
bool dst_acc = si.is_accepting_scc(scc_dst);
bool dst_acc = !si.is_rejecting_scc(scc_dst);
if (maybe_accepting && scc_src == scc_dst)
acc = t.acc - common_out[t.src];
else if (dst_acc)
......@@ -106,6 +119,8 @@ namespace spot
acc = one_in[t.dst];
if (dst_acc)
acc |= common_out[t.dst];
else
acc = unsat_mark.second;
res->new_edge(one.second, new_state(t.dst, acc),
t.cond, one.first.second);
}
......
......@@ -159,3 +159,68 @@ randltl --weak-fairness -n 20 2 |
"$ltl2tgba -H %f | $autfilt -H >%O"
test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s`
# Test case from Thibaud Michaud. This used to fail, because sbacc()
# would remove acceptance marks from all rejecting SCCS...
cat >tm.hoa <<EOF
HOA: v1
States: 5
Start: 1
AP: 4 "req" "go" "ack" "cancel"
acc-name: parity max odd 3
Acceptance: 3 Fin(2) & (Inf(1) | Fin(0))
properties: trans-labels explicit-labels trans-acc colored complete
properties: deterministic
--BODY--
State: 0
[t] 1 {0}
State: 1
[!0] 0 {0}
[0] 2 {0}
State: 2
[2] 1 {0}
[!2] 3 {0}
State: 3
[t] 4 {0}
State: 4
[2] 1 {2}
[!2] 3 {1}
--END--
EOF
autfilt --sbacc tm.hoa > out.hoa
autfilt -q --equivalent-to out.hoa tm.hoa
# Tautological acceptances are converted to "t"
cat >taut.hoa <<EOF
HOA: v1
States: 2
Start: 1
AP: 0
Acceptance: 2 Fin(0) | Inf(0) | Fin(1)
--BODY--
State: 0
[t] 1 {0}
State: 1
[t] 0
[t] 1 {1}
--END--
EOF
cat >expect.hoa <<EOF
HOA: v1
States: 2
Start: 1
AP: 0
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete weak
--BODY--
State: 0
[t] 1
State: 1
[t] 0
[t] 1
--END--
EOF
autfilt --sbacc taut.hoa > out.hoa
diff out.hoa expect.hoa
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment