diff --git a/NEWS b/NEWS index 9e3123790..538b84f7b 100644 --- a/NEWS +++ b/NEWS @@ -21,6 +21,8 @@ New in spot 2.3.2.dev (not yet released) - twa objects have a new property: prop_complete(). This obviously acts as a cache for the is_complete() function. + - spot::dualize() implements the dual of any alternating automaton. + Bug fixes: - In "lenient" mode the parser would fail to recover from diff --git a/python/spot/impl.i b/python/spot/impl.i index 696cb462c..4273e61db 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -120,6 +120,7 @@ #include #include #include +#include #include #include #include @@ -541,6 +542,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 8b8a89d6e..e7e435e50 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -43,6 +43,7 @@ twaalgos_HEADERS = \ dot.hh \ dtbasat.hh \ dtwasat.hh \ + dualize.hh \ emptiness.hh \ emptiness_stats.hh \ gv04.hh \ @@ -102,6 +103,7 @@ libtwaalgos_la_SOURCES = \ dot.cc \ dtbasat.cc \ dtwasat.cc \ + dualize.cc \ emptiness.cc \ gv04.cc \ hoa.cc \ diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc new file mode 100644 index 000000000..26fe1a32a --- /dev/null +++ b/spot/twaalgos/dualize.cc @@ -0,0 +1,383 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). +// +// 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 . + +#include +#include +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + class dualizer final + { + private: + // Input automaton + const const_twa_graph_ptr aut_; + // State id to bdd variable association + // [id] == bddtrue means the state will be accepting everything + // (true state) in the dual automaton. + // [id] == bddfalse means the state will be rejecting everything + // (sink) in the dual automaton, which can lead to the removal of + // the transitions going into that state and therefore to the removal + // of the state when applying purge_unreachable_states(). + // When [id] != bddtrue/bddfalse, the value correspond to the state + // bdd variable. + std::vector state_to_var_; + // bdd variable to state id association + std::map var_to_state_; + // Acceptance mark to bdd variable association + std::vector mark_to_var_; + // bdd variable to acceptance mark association + std::map var_to_mark_; + // bdd representing all the state variables + bdd all_states_; + // bdd representing all the marks variables + bdd all_marks_; + // bdd representing states & marks variables + bdd all_vars_; + // Id of the true state sink. -1U if none. + unsigned true_state_; + // In case the acceptance condition is never unsatisfied, but the + // automaton is not complete, we do transform the acceptance condition + // to Büchi, and need to mark all the existing transitions with the + // proper mark, that will be stored in acc_. 0U if not used. + acc_cond::mark_t acc_; + // Whether aut_ has a state accepting all. + bool has_sink; + + // Any sink state in the input automaton will become a true state in the + // output. Knowing those allows us to simplify some universal transitions. + // There could be more than one sink state in the input automaton, and in + // this case they will be squashed into a single true state in the output + // automaton. + void find_sink_states(acc_cond::mark_t& second) + { + // Loop over the states and search a state that has no outgoing + // transitions, or only self-loops labeled by the same non-accepting + // mark. A similar test is done in complete_here(). + unsigned n = aut_->num_states(); + for (unsigned i = 0; i < n; ++i) + { + bool sinkable = true; + bool first = true; + acc_cond::mark_t commonacc = second; + for (auto& t: aut_->out(i)) + { + if (t.dst != i) + { + sinkable = false; + break; + } + if (first) + { + commonacc = t.acc; + first = false; + } + else if (t.acc != commonacc) + { + sinkable = false; + break; + } + } + if (sinkable && !aut_->acc().accepting(commonacc)) + { + second = commonacc; + state_to_var_[i] = bddtrue; + true_state_ = i; + has_sink = true; + } + } + } + // Any true state in the input automaton will become a sink state in the + // output. Knowing those allow us to simplify some universal transitions. + // There could be more than one true state in the input automaton. All + // true states from the input automaton will be removed in the output + // and the transitions leading to those states will be removed as well. + void find_true_states() + { + // Loop over the states and search a state that has a self-loop on + // any letter (bddtrue), with an accepting mark. + unsigned n = aut_->num_states(); + for (unsigned i = 0; i < n; ++i) + { + bool acc_all = false; + for (auto& t: aut_->out(i)) + { + if (t.dst == i && t.cond == bddtrue + && aut_->acc().accepting(t.acc)) + { + acc_all = true; + break; + } + } + if (acc_all) + { + state_to_var_[i] = bddfalse; + has_sink = true; + } + } + } + + void copy_edges(const twa_graph_ptr &res) + { + std::vector st; + unsigned n = aut_->num_states(); + for (unsigned i = 0; i < n; ++i) + { + bdd delta = dualized_transition_function(i); + bdd ap = bdd_exist(bdd_support(delta), all_vars_); + bdd letters = bdd_exist(delta, all_vars_); + + while (letters != bddfalse) + { + bdd oneletter = bdd_satoneset(letters, ap, bddtrue); + letters -= oneletter; + + minato_isop isop(delta & oneletter); + bdd cube; + + while ((cube = isop.next()) != bddfalse) + { + bdd cond = bdd_exist(cube, all_vars_); + bdd dest = bdd_existcomp(cube, all_vars_); + + st.clear(); + acc_cond::mark_t m = bdd_to_state(dest, st); + if (st.empty()) + { + st.push_back(true_state_); + if (aut_->prop_state_acc()) + m = aut_->state_acc_sets(i); + } + res->new_univ_edge(i, st.begin(), st.end(), cond, m); + } + } + } + } + + // Handles the dualization of a universal initial transition. + // In theory the transition would be split into several existential + // initial transitions, but since spot does not allow multiple initial + // states, we rather use a trick: We add a new initial state, and then + // copy all exiting transitions from each of the state of the universal + // initial transition. + void univ_init(const twa_graph_ptr& res) + { + bdd comb = bddfalse; + outedge_combiner oe(res); + for (unsigned c : aut_->univ_dests(aut_->get_init_state_number())) + comb |= oe(c); + + auto s = res->new_state(); + res->set_init_state(s); + oe.new_dests(s, comb); + } + + // Allocates the states and marks as variables into the bdd dictionary. + // Also adds the corresponding mapping, and sets all_states_, all_marks_, + // and all_vars_ to hold those variables as bdds. + void allocate_dict_vars(const twa_graph_ptr& res) + { + auto dict = aut_->get_dict(); + + unsigned numstates = aut_->num_states(); + all_states_ = bddtrue; + for (unsigned i = 0; i < numstates; ++i) + { + int v = dict->register_anonymous_variables(1, this); + if (state_to_var_[i] != bddtrue) + state_to_var_[i] = bdd_ithvar(v); + var_to_state_[v] = i; + all_states_ &= bdd_ithvar(v); + } + + unsigned numsets = res->num_sets(); + all_marks_ = bddtrue; + for (unsigned i = 0; i < numsets; ++i) + { + int v = dict->register_anonymous_variables(1, this); + mark_to_var_.push_back(v); + var_to_mark_.emplace(v, i); + all_marks_ &= bdd_ithvar(v); + } + all_vars_ = all_states_ & all_marks_; + } + + // Returns the dualized transition function of any input state as a bdd. + bdd dualized_transition_function(unsigned state_id) + { + if (state_to_var_[state_id] == bddtrue) + return bddfalse; + + bdd res = bddtrue; + for (auto& e : aut_->out(state_id)) + { + bdd dest = bddfalse; + for (unsigned d : aut_->univ_dests(e)) + dest |= state_to_var_[d]; + + bdd mark_bdd = bddtrue; + acc_cond::mark_t m = acc_ ? acc_ : e.acc; + for (unsigned s: m.sets()) + mark_bdd &= bdd_ithvar(mark_to_var_[s]); + + res &= bdd_imp(e.cond, mark_bdd & dest); + } + return res; + } + + // Given the bdd representation b of a transition, adds destination states + // to s, and returns the marks on the transition. s being empty means the + // transition goes toward a "forever true" state. s with size one + // represents an existential transition, while size over one represents + // a universal transition. + acc_cond::mark_t bdd_to_state(bdd b, std::vector& s) + { + acc_cond::mark_t m = 0U; + while (b != bddtrue) + { + assert(bdd_low(b) == bddfalse); + int v = bdd_var(b); + auto it = var_to_state_.find(v); + if (it != var_to_state_.end()) + s.push_back(it->second); + else + m.set(var_to_mark_[v]); + + b = bdd_high(b); + } + return m; + } + + public: + dualizer(const const_twa_graph_ptr& aut) + : aut_(aut), + state_to_var_(aut_->num_states(), bddfalse), + true_state_(-1U), + acc_(0U), + has_sink(false) + { + } + + ~dualizer() + { + aut_->get_dict()->unregister_all_my_variables(this); + } + + twa_graph_ptr run() + { + bool cmpl = is_complete(aut_); + auto um = aut_->acc().unsat_mark(); + + auto res = make_twa_graph(aut_->get_dict()); + res->copy_ap_of(aut_); + + if (!um.first && cmpl) + { + //Shortcut if dual is false + res->new_states(1); + res->new_edge(0, 0, bddtrue, 0U); + res->set_init_state(0); + res->set_acceptance(0, acc_cond::acc_code::f()); + + res->prop_terminal(true); + res->prop_complete(true); + res->prop_universal(true); + return res; + } + if (is_deterministic(aut_)) + { + res = cleanup_acceptance_here(spot::complete(aut_)); + res->set_acceptance(res->num_sets(), + res->get_acceptance().complement()); + // Complementing the acceptance is likely to break the terminal + // property, but not weakness. We make a useless call to + // prop_keep() just so we remember to update it in the future if a + // new argument is added. + res->prop_keep({true, true, true, true, true, true}); + res->prop_terminal(trival::maybe()); + return res; + } + + const_twa_graph_ptr autptr; + res->new_states(aut_->num_states()); + if (!cmpl) + { + if (!um.first) + { + acc_ = res->set_buchi(); + autptr = res; + } + else + { + find_sink_states(um.second); + autptr = aut_; + } + if (true_state_ == -1U) + true_state_ = res->new_state(); + } + // This case does not cover cmpl && !um.first + // Due to previous test shortcutting automatons that accept all words. + else + { + assert(um.first); + find_sink_states(um.second); + autptr = aut_; + } + if (true_state_ != -1U) + res->new_edge(true_state_, true_state_, bddtrue, um.second); + + res->set_acceptance(autptr->num_sets(), + autptr->get_acceptance().complement()); + allocate_dict_vars(res); + find_true_states(); + + copy_edges(res); + + unsigned init_state = aut_->get_init_state_number(); + if (aut_->is_univ_dest(init_state)) + univ_init(res); + else + res->set_init_state(init_state); + + res->merge_edges(); + res->purge_unreachable_states(); + + res->prop_copy(aut_, {true, true, false, false, false, true}); + res->prop_terminal(trival::maybe()); + if (!has_sink) + res->prop_complete(true); + + cleanup_acceptance_here(res); + return res; + } + }; + } + + twa_graph_ptr dualize(const const_twa_graph_ptr& aut) + { + dualizer du(aut); + return du.run(); + } +} diff --git a/spot/twaalgos/dualize.hh b/spot/twaalgos/dualize.hh new file mode 100644 index 000000000..42b5bef6a --- /dev/null +++ b/spot/twaalgos/dualize.hh @@ -0,0 +1,58 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 . + +#pragma once + +#include +#include + +namespace spot +{ + /// \brief Complement an automaton by dualizing it. + /// + /// Given an automaton \a aut of any type, produces the dual as output. The + /// automaton will be completed if it isn't already. If it is deterministic + /// and complete, complementing the automaton can be done by just + /// complementing the acceptance condition. + /// + /// In particular, this implies that an input that use generalized Büchi will + /// be output as generalized co-Büchi. + /// + /// Functions like to_generalized_buchi() or remove_fin() are frequently + /// called on existential automatons after dualize() to obtain an easier + /// acceptance condition, but maybe at the cost of losing determinism. + /// + /// If the input automaton is deterministic, the output will be deterministic. + /// If the input automaton is existential, the output will be universal. + /// If the input automaton is universal, the output will be existential. + /// Finally, if the input automaton is alternating, the result is alternating. + /// More can be found on page 22 (Definition 1.6) of: + /** \verbatim + @mastersthesis{loding.98.methodsfor + author = {Christof Löding} + title = {Methods for the Transformation of ω-Automata: Complexity + and Connection to Second Order Logic} + school = {Institute of Computer Science and Applied Mathematics + Christian-Albrechts-University of Kiel} + year = {1998} + } + \endverbatim */ + SPOT_API twa_graph_ptr + dualize(const const_twa_graph_ptr& aut); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index f59f871c0..da132b2f2 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -332,6 +332,7 @@ TESTS_python = \ python/bugdet.py \ python/declenv.py \ python/decompose_scc.py \ + python/dualize.py \ python/implies.py \ python/interdep.py \ python/ltl2tgba.test \ diff --git a/tests/python/dualize.py b/tests/python/dualize.py new file mode 100755 index 000000000..d06e9f6ad --- /dev/null +++ b/tests/python/dualize.py @@ -0,0 +1,540 @@ +#!/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 +import buddy + +match_strings = [('is_buchi', 'is_co_buchi'),\ + ('is_generalized_buchi', 'is_generalized_co_buchi'),\ + ('is_all', 'is_none'),\ + ('is_all', 'is_all'), + ('is_buchi', 'is_all')] + +def dualtype(aut, dual): + if dual.acc().is_none(): return True + return (not spot.is_deterministic(aut) or spot.is_deterministic(dual))\ + and (spot.is_universal(dual) or not aut.is_existential())\ + and (dual.is_existential() or not spot.is_universal(aut)) + +def produce_phi(rg, n): + phi = [] + while len(phi) < n: + phi.append(rg.next()) + return phi + +def produce_automaton(phi): + aut = [] + for f in phi: + aut.append(spot.translate(f)) + return aut + +def test_aut(aut, d = None): + if d is None: + d = spot.dualize(aut) + aa = aut.acc() + da = d.acc() + + complete = spot.is_complete(aut) + univ = aut.is_univ_dest(aut.get_init_state_number()) + an = aut.num_states() + dn = d.num_states() + + if not dualtype(aut, d): + return (False, 'Incorrect transition mode resulting of dual') + for p in match_strings: + if ((getattr(aa, p[0])() and getattr(da, p[1])())\ + or (getattr(aa, p[1])() and getattr(da, p[0])())): + return (True, '') + return (False, 'Incorrect acceptance type dual') + +def test_assert(a, d=None): + t = test_aut(a, d) + if not t[0]: + print (t[1]) + print (a.to_str('hoa')) + print (spot.dualize(a).to_str('hoa')) + assert False + +aut = spot.translate('a') + +test_assert(aut) + +dual = spot.dualize(aut) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 3 +Start: 1 +AP: 1 "a" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic stutter-invariant weak +--BODY-- +State: 0 {0} +[t] 0 +State: 1 +[0] 0 +[!0] 2 +State: 2 +[t] 2 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +[0] 2 +State: 1 {0} +[0] 1 +State: 2 {0} +[1] 2 +--END--""") + +test_assert(aut) +dual = spot.dualize(aut) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: univ-branch trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0] 3 +[0] 1&2 +State: 1 {0} +[0] 1 +[!0] 3 +State: 2 {0} +[1] 2 +[!1] 3 +State: 3 +[t] 3 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 4 +Start: 0&2 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc univ-branch +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[t] 1 +State: 2 +[1] 3 +State: 3 {0} +[t] 3 +--END--""") + +test_assert(aut) +dual = spot.dualize(aut) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 2 +Start: 1 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[t] 0 +State: 1 +[!0 | !1] 0 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 4 +Start: 0&2 +AP: 2 "a" "b" +Acceptance: 2 Inf(0) | Inf(1) +properties: trans-labels explicit-labels state-acc univ-branch +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[t] 1 +State: 2 +[1] 3 +State: 3 {1} +[t] 3 +--END--""") + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 2 +Start: 1 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[t] 0 +State: 1 +[!0 | !1] 0 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) | Fin(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[0] 3 +State: 2 +[0] 3 +State: 3 {0} +[t] 3 +--END--""") + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 5 +Start: 0 +AP: 2 "a" "b" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {0} +[0] 1 +[!0] 4 +State: 1 {0} +[0] 3 +[!0] 4 +State: 2 {0} +[0] 3 +[!0] 4 +State: 3 {0} +[t] 3 +State: 4 +[t] 4 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Inf(0) & Fin(1) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 {0} +[0&!1] 1 +[0&1] 2 +State: 1 {1} +[1] 1 +[0&!1] 2 +State: 2 +[!0&!1] 0 +[t] 2 +--END--""") + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: univ-branch trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {0} +[0&!1] 1 +[0&1] 2 +[!0] 3 +State: 1 {1} +[1] 1 +[0&!1] 2 +[!0&!1] 3 +State: 2 +[0 | 1] 2 +[!0&!1] 0&2 +State: 3 +[t] 3 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +Acceptance: 1 Inf(0) | Fin(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0] 1 +[!0] 2 +State: 1 {0} +[t] 1 +State: 2 +[t] 2 +[0] 0 +--END--""") + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 1 +Start: 0 +AP: 1 "a" +acc-name: none +Acceptance: 0 f +properties: trans-labels explicit-labels state-acc complete +properties: deterministic terminal +--BODY-- +State: 0 +[t] 0 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +Acceptance: 1 Inf(0) | Fin(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0] 1 +[!0] 2 +State: 1 {0} +[t] 1 +State: 2 +[t] 2 +--END--""") + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 1 +Start: 0 +AP: 1 "a" +acc-name: none +Acceptance: 0 f +properties: trans-labels explicit-labels state-acc complete +properties: deterministic terminal +--BODY-- +State: 0 +[t] 0 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0&1] 1 +[0&!1] 2 +State: 1 +[t] 1 {0} +[0] 0 +State: 2 +[0] 2 +--END--""") + + +dual = spot.dualize(aut) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0 | !1] 1 +State: 1 +[t] 1 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +[0] 2 +State: 1 {0} +[0] 1 +State: 2 +[t] 2 +--END--""") + + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0] 1 +State: 1 {0} +[t] 1 +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 4 +Start: 0 +AP: 1 "a" +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +[!0] 2 +[0] 0 +State: 1 {0} +[t] 1 +State: 2 +[0] 3 +[!0] 0 +State: 3 {0} +[t] 3 +--END--""") + +dual = spot.dualize(aut) +assert dualtype(aut, dual) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 0 +[!0] 1 +State: 1 +[!0] 0 +[0] 2 +State: 2 {0} +[t] 2 +--END--""" + + +aut = spot.translate('G!a R XFb') +test_assert(aut) +dual = spot.dualize(aut) +h = dual.to_str('hoa') + +assert h == """HOA: v1 +States: 5 +Start: 0 +AP: 2 "a" "b" +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: univ-branch trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 1 +[!0] 1&2 +State: 1 +[0&!1] 1 +[0&1] 1 {0} +[!0&!1] 1&2 +[!0&1] 1&2 {0} +State: 2 +[!0&1] 3 +[0 | !1] 4 +State: 3 +[!0] 3 {0} +[0] 4 +State: 4 +[t] 4 +--END--""" + + +opts = spot.option_map() +opts.set('output', spot.OUTPUTLTL) +opts.set('tree_size_min', 15) +opts.set('tree_size_max', 15) +opts.set('seed', 0) +opts.set('simplification_level', 0) +spot.srand(0) +rg = spot.randltlgenerator(2, opts) + +for a in produce_automaton(produce_phi(rg, 1000)): + test_assert(a) + test_assert(spot.dualize(a), spot.dualize(spot.dualize(a)))