From a12d676bdc8cad5b66f50589fa0782a42bd9c097 Mon Sep 17 00:00:00 2001 From: Thomas Medioni Date: Thu, 27 Apr 2017 15:10:53 +0200 Subject: [PATCH] introduce spot::simplify_acceptance() MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Simplify some automata where some marks are identical, or complementary to another. Fixes #216. * NEWS: mention the new function. * spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh: Implement the function. * tests/Makefile.am, tests/python/merge.py: Test this implementation. --- NEWS | 4 + spot/twaalgos/cleanacc.cc | 219 +++++++++++++ spot/twaalgos/cleanacc.hh | 13 + tests/Makefile.am | 1 + tests/python/merge.py | 647 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 884 insertions(+) create mode 100644 tests/python/merge.py diff --git a/NEWS b/NEWS index 4419d4ecd..634d00eb8 100644 --- a/NEWS +++ b/NEWS @@ -104,6 +104,10 @@ New in spot 2.3.4.dev (not yet released) automaton. This parameter is defaulted to true, in order to keep this modification backward-compatible. + - The new function spot::simplify_acceptance() is able to perform + some simplifications on an acceptance condition, and might lead + to the removal of some acceptance sets. + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index 7f2c1d577..44018de30 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -73,5 +73,224 @@ namespace spot twa::prop_set::all())); } + namespace + { + twa_graph_ptr merge_identical_marks_here(twa_graph_ptr aut) + { + // always cleanup before proceeding, otherwise if some mark appears in the + // acceptance condition, but not in the automaton the result is undefined. + cleanup_acceptance_here(aut, false); + auto& acc = aut->acc(); + auto& c = acc.get_acceptance(); + acc_cond::mark_t used_in_cond = c.used_sets(); + + if (!used_in_cond) + return aut; + + unsigned num_sets = acc.num_sets(); + std::vector always_together(num_sets); + + for (unsigned i = 0; i < num_sets; ++i) + if (used_in_cond.has(i)) + always_together[i] = used_in_cond; + else + always_together[i] = acc_cond::mark_t({i}); + + acc_cond::mark_t previous_a = 0U; + for (auto& t: aut->edges()) + { + acc_cond::mark_t a = t.acc & used_in_cond; + if (a == previous_a) + continue; + previous_a = a; + for (unsigned m: a.sets()) + { + acc_cond::mark_t at = always_together[m]; + acc_cond::mark_t newm = at & a; + + for (unsigned rem: (at - newm).sets()) + always_together[rem] -= newm; + + always_together[m] = newm; + } + } + + acc_cond::mark_t to_remove = 0U; + for (unsigned i = 0; i < num_sets; ++i) + { + auto oldm = always_together[i]; + if (oldm == acc_cond::mark_t({i})) + continue; + + acc_cond::mark_t newm = oldm.lowest(); + to_remove |= oldm - newm; + always_together[i] = newm; + } + for (auto& t: aut->edges()) + t.acc -= to_remove; + + // Replace the marks in the acceptance condition + auto pos = &c.back(); + auto end = &c.front(); + while (pos > end) + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + acc_cond::mark_t replace = pos[-1].mark & to_remove; + pos[-1].mark -= replace; + for (unsigned m: replace.sets()) + pos[-1].mark |= always_together[m]; + pos -= 2; + break; + } + } + return aut; + } + + // Eventually remove complementary marks from the acceptance condition. + acc_cond::acc_code remove_compl_rec(const acc_cond::acc_word* pos, + const std::vector& + complement) + { + auto start = pos - pos->sub.size; + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + { + --pos; + auto res = acc_cond::acc_code::t(); + acc_cond::mark_t seen_fin = 0U; + auto inf = acc_cond::acc_code::inf(0U); + do + { + auto tmp = remove_compl_rec(pos, complement); + + if (tmp.back().sub.op == acc_cond::acc_op::Fin + && tmp.front().mark.count() == 1) + seen_fin |= tmp.front().mark; + + if (tmp.back().sub.op == acc_cond::acc_op::Inf) + { + inf &= std::move(tmp); + pos -= pos->sub.size + 1; + continue; + } + tmp &= std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + + for (auto m: seen_fin.sets()) + inf.front().mark -= complement[m]; + + res &= inf; + return res; + } + case acc_cond::acc_op::Or: + { + --pos; + auto res = acc_cond::acc_code::f(); + acc_cond::mark_t seen_inf = 0U; + auto fin = acc_cond::acc_code::f(); + do + { + auto tmp = remove_compl_rec(pos, complement); + + if (tmp.back().sub.op == acc_cond::acc_op::Inf + && tmp.front().mark.count() == 1) + seen_inf |= tmp.front().mark; + + if (tmp.back().sub.op == acc_cond::acc_op::Fin) + { + fin |= std::move(tmp); + pos -= pos->sub.size + 1; + continue; + } + tmp |= std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + + for (auto m: seen_inf.sets()) + fin.front().mark -= complement[m]; + + res |= fin; + return res; + } + case acc_cond::acc_op::Fin: + return acc_cond::acc_code::fin(pos[-1].mark); + case acc_cond::acc_op::Inf: + return acc_cond::acc_code::inf(pos[-1].mark); + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + }; + SPOT_UNREACHABLE(); + return {}; + } + + // Always cleanup_acceptance_here with stripping after calling this function + // As complementary marks might be simplified in the acceptance condition. + twa_graph_ptr simplify_complementary_marks_here(twa_graph_ptr aut) + { + auto& acc = aut->acc(); + auto c = acc.get_acceptance(); + acc_cond::mark_t used_in_cond = c.used_sets(); + if (!used_in_cond) + return aut; + + unsigned num_sets = acc.num_sets(); + std::vector complement(num_sets); + + + for (unsigned i = 0; i < num_sets; ++i) + if (used_in_cond.has(i)) + complement[i] = used_in_cond - acc_cond::mark_t({i}); + + acc_cond::mark_t previous_a = 0U; + for (auto& t: aut->edges()) + { + if (t.acc == previous_a) + continue; + previous_a = t.acc; + for (unsigned m: used_in_cond.sets()) + { + if (t.acc.has(m)) + complement[m] -= t.acc; + else + complement[m] &= t.acc; + } + } + aut->set_acceptance(num_sets, + remove_compl_rec(&acc.get_acceptance().back(), + complement)); + return aut; + } + } + + twa_graph_ptr simplify_acceptance_here(twa_graph_ptr aut) + { + cleanup_acceptance_here(aut, false); + merge_identical_marks_here(aut); + simplify_complementary_marks_here(aut); + cleanup_acceptance_here(aut, true); + + return aut; + } + + twa_graph_ptr simplify_acceptance(const_twa_graph_ptr aut) + { + return simplify_acceptance_here(make_twa_graph(aut, twa::prop_set::all())); + } } diff --git a/spot/twaalgos/cleanacc.hh b/spot/twaalgos/cleanacc.hh index 8af0e8248..d58e01fd0 100644 --- a/spot/twaalgos/cleanacc.hh +++ b/spot/twaalgos/cleanacc.hh @@ -34,4 +34,17 @@ namespace spot /// \brief Remove useless acceptance sets SPOT_API twa_graph_ptr cleanup_acceptance(const_twa_graph_ptr aut); + + /// \brief Simplify an acceptance condition + /// + /// Remove useless acceptance sets. + /// Merge identical sets. + /// If some sets are complement to each other, might result in the + /// simplification of some clause in the acceptance condition. + SPOT_API twa_graph_ptr + simplify_acceptance_here(twa_graph_ptr aut); + + /// \brief Simplify an acceptance condition + SPOT_API twa_graph_ptr + simplify_acceptance(const_twa_graph_ptr aut); } diff --git a/tests/Makefile.am b/tests/Makefile.am index e9493fd0c..3da8475f2 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -348,6 +348,7 @@ TESTS_python = \ python/ltlf.py \ python/ltlparse.py \ python/ltlsimple.py \ + python/merge.py \ python/minato.py \ python/misc-ec.py \ python/optionmap.py \ diff --git a/tests/python/merge.py b/tests/python/merge.py new file mode 100644 index 000000000..c0601e7bb --- /dev/null +++ b/tests/python/merge.py @@ -0,0 +1,647 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# l'EPITA. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import spot + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Inf(0) & Inf(1) | Fin(3) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0 1} +State: 1 +[0] 1 {2 3} +[1] 2 {0 1 2 3} +State: 2 +[1] 0 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Fin(1) | Inf(0) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0} +State: 1 +[0] 1 {1} +[1] 2 {0 1} +State: 2 +[1] 0 {1} +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 Inf(0) & Inf(1) & Inf(2) | Fin(3) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0 1} +State: 1 +[0] 1 {2 3} +[1] 2 {0 1 2 3} +State: 2 +[1] 0 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Fin(1) | (Inf(0)&Inf(1)) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0} +State: 1 +[0] 1 {1} +[1] 2 {0 1} +State: 2 +[1] 0 {1} +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 (Inf(0) & Fin(1)) | (Inf(2) & Fin(3)) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0 1} +State: 1 +[0] 1 {2 3} +[1] 2 {0 1 2 3} +State: 2 +[1] 0 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 (Fin(0) & Inf(0)) | (Fin(1) & Inf(1)) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0} +State: 1 +[0] 1 {1} +[1] 2 {0 1} +State: 2 +[1] 0 {1} +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 (Inf(0) & Fin(2)) | (Inf(1) & Fin(3)) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0 1} +State: 1 +[0] 1 {2 3} +[1] 2 {2 3} +State: 2 +[1] 0 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[0] 1 +[1] 2 +State: 2 {0} +[1] 0 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 (Inf(0) & Fin(2)) | (Inf(1) & (Fin(3) | Fin(2))) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0 1} +State: 1 +[0] 1 {2 3} +[1] 2 {2 3} +State: 2 +[1] 0 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[0] 1 +[1] 2 +State: 2 {0} +[1] 0 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 4 (Inf(0) & Fin(2)) | (Inf(1) & (Fin(3) | Fin(2))) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 {0 1} +State: 1 +[0] 1 {2 3} +[1] 2 {2 3} +State: 2 +[1] 0 +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 (Fin(1) & Inf(0)) | (Fin(1) & Inf(0)) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 {0} +[0] 1 +State: 1 {1} +[0] 1 +[1] 2 +State: 2 +[1] 0 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: Rabin 2 +Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) +--BODY-- +State: 0 {0} +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +State: 1 {1} +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +State: 2 {0 3} +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +State: 3 {1 3} +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +--END--""") + +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {0} +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +State: 1 +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +State: 2 {0 1} +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +State: 3 {1} +[!0&!1] 1 +[0&!1] 0 +[!0&1] 3 +[0&1] 2 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 1 +[!0] 0 {2} +State: 1 +[0] 1 {1 2} +[!0] 2 +State: 2 +[0] 2 {0 1 2} +[!0] 1 {0} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 3 (Fin(0) | Inf(1)) & Fin(2) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 1 +[!0] 0 {2} +State: 1 +[0] 1 {1 2} +[!0] 2 +State: 2 +[0] 2 {0 1 2} +[!0] 1 {0} +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 4 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&1] 2 +[!0&!1] 0 {0} +[0] 3 +State: 1 +[0] 0 {1 2 3} +[!0] 3 {0 2} +State: 2 +[t] 1 {1 2} +State: 3 +[0&1] 0 {1} +[0&!1] 3 {1 2} +[!0] 1 {2 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 4 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&1] 2 +[!0&!1] 0 {0} +[0] 3 +State: 1 +[0] 0 {1 2 3} +[!0] 3 {0 2} +State: 2 +[t] 1 {1 2} +State: 3 +[0&1] 0 {1} +[0&!1] 3 {1 2} +[!0] 1 {2 3} +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 1 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {1 2} +[t] 0 +--END-- +""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 1 +Start: 0 +AP: 2 "p0" "p1" +acc-name: none +Acceptance: 0 f +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 0 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 0 {0 2} +[!0] 1 {3} +State: 1 +[t] 1 {1 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 3 (Fin(0) | Inf(1)) & Inf(2) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 0 {0} +[!0] 1 {2} +State: 1 +[t] 1 {1 2} +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 1 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {0 1 3} +[t] 0 +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 1 +Start: 0 +AP: 2 "p0" "p1" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 0 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 0 {0} +[!0] 1 +State: 1 +[0] 1 {3} +[!0] 0 {1 3} +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 0 {0} +[!0] 1 +State: 1 +[0] 1 +[!0] 0 {1} +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: trans-labels explicit-labels state-acc colored complete +properties: deterministic +--BODY-- +State: 0 {1} +[t] 1 +State: 1 {1} +[t] 0 +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 1 +State: 1 +[t] 0 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {1} +[t] 2 +State: 1 {0 3} +[t] 1 +State: 2 {2} +[t] 1 +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 3 (Fin(0) | Inf(1)) & (Fin(2) | Inf(0)) +properties: trans-labels explicit-labels state-acc colored complete +properties: deterministic +--BODY-- +State: 0 {1} +[t] 2 +State: 1 {0} +[t] 1 +State: 2 {2} +[t] 1 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {0 1 2} +[t] 2 +State: 1 {0 3} +[t] 2 +State: 2 {1 2 3} +[t] 1 +--END-- +""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p1" +Acceptance: 3 (Fin(0) | Inf(1)) & (Fin(1) | Inf(2)) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {0 1} +[t] 2 +State: 1 {0 2} +[t] 2 +State: 2 {1 2} +[t] 1 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 1 {1} +State: 1 +[0] 1 {1} +[!0] 0 +--END--""") +spot.simplify_acceptance_here(aut) +hoa = aut.to_str('hoa') + +assert hoa == """HOA: v1 +States: 2 +Start: 0 +AP: 2 "p0" "p1" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 1 +State: 1 +[0] 1 +[!0] 0 +--END--"""