Commit 37fc948b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

sbacc: fix a typo and remove some useless code

* spot/twaalgos/sbacc.cc: Do not assign to one_in twice, and
fix the value of init_acc.
* tests/core/sbacc.test: Add a test case.
* NEWS: Mention the bug.
parent 1eb5be54
......@@ -19,6 +19,10 @@ New in spot 2.3.1.dev (not yet released)
- genltl was never meant to have (randomly attributed) short
options for --postive and --negative.
- a typo in the code for transformating transition-based acceptance
to state-based acceptance could cause a superfluous initial state
to be output in some cases (the result was still correct).
Deprecation notices:
- Using --format=%a to print the number of atomic propositions in
......
......@@ -37,21 +37,22 @@ namespace spot
unsigned ns = old->num_states();
acc_cond::mark_t all = old->acc().all_sets();
// Marks that are common to all ingoing or outgoing transitions.
std::vector<acc_cond::mark_t> common_in(ns, all);
std::vector<acc_cond::mark_t> common_out(ns, all);
// Marks that label one incoming transition from the same SCC.
std::vector<acc_cond::mark_t> one_in(ns, 0U);
for (auto& e: old->edges())
if (si.scc_of(e.src) == si.scc_of(e.dst))
{
common_in[e.dst] &= e.acc;
common_out[e.src] &= e.acc;
one_in[e.dst] = e.acc;
}
for (unsigned s = 0; s < ns; ++s)
common_out[s] |= common_in[s];
for (auto& e: old->edges())
if (si.scc_of(e.src) == si.scc_of(e.dst))
one_in[e.dst] = (e.acc - common_out[e.src]);
one_in[e.dst] = e.acc - common_out[e.src];
auto res = make_twa_graph(old->get_dict());
res->copy_ap_of(old);
......@@ -83,7 +84,7 @@ namespace spot
if (!si.is_rejecting_scc(si.scc_of(old_init)))
// Use any edge going into the initial state to set the first
// acceptance mark.
init_acc = one_in[old_init] | common_out[init_acc];
init_acc = one_in[old_init] | common_out[old_init];
res->set_init_state(new_state(old_init, init_acc));
while (!todo.empty())
......
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -76,6 +76,22 @@ State: 1 {0}
State: 2
[0] 0 {1}
--END--
/* The following example used to be converted into a
3-state automaton instead of just 2 states, due to
a typo in the code. */
HOA: v1
States: 2
Start: 1
AP: 2 "a" "b"
Acceptance: 2 Fin(0) & Inf(1)
--BODY--
State: 0
[t] 0 {0}
State: 1
[1] 0
[0&!1] 1 {1}
--END--
EOF
run 0 $autfilt --state-based-acceptance in.hoa -H > out.hoa
......@@ -96,6 +112,20 @@ State: 1 {0}
State: 2 {0 1}
[0] 0
--END--
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Rabin 1
Acceptance: 2 Fin(0) & Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {1}
[0&!1] 0
[1] 1
State: 1
[t] 1
--END--
EOF
diff out.hoa expected
......@@ -103,7 +133,7 @@ diff out.hoa expected
$autfilt --sba -H expected > out.hoa
diff out.hoa expected
$autfilt --strip-acc -H expected > out.hoa
$autfilt --strip-acc -H expected -n1 > out.hoa
cat >expected <<EOF
HOA: v1
States: 3
......
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