diff --git a/NEWS b/NEWS index bf7dd0482df2d2aca6bda95c369607cbd36ed193..c5cff53103130dc0e93e5a1ceac46a8ecfca0350 100644 --- a/NEWS +++ b/NEWS @@ -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 diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index b4df91026e83878012a62f20b4cf1fdd5a66c0e5..93acc554c2612d86506f45a668cf756807cb8fa0 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -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 common_in(ns, all); std::vector common_out(ns, all); + // Marks that label one incoming transition from the same SCC. std::vector 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()) diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 156c2250acab3a5088f05e6ae2213e9eecab8270..fedc228bdd6911a5996acb737aedb2d6a2c374be 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -1,6 +1,6 @@ #! /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 <