diff --git a/NEWS b/NEWS index 2b8697d29..7caad3743 100644 --- a/NEWS +++ b/NEWS @@ -209,6 +209,9 @@ New in spot 2.4.2.dev (not yet released) controllers in the format required by the synthesis tools competition SYNTCOMP. + - The new function spot::check_determinism() sets both + prop_semi_deterministic() and prop_universal() appropriately. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index a00267958..50cdcde2b 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -162,46 +162,90 @@ namespace spot return res; } + namespace + { + static bool + check_semi_determism(const const_twa_graph_ptr& aut, bool and_determinism) + { + trival sd = aut->prop_semi_deterministic(); + if (sd.is_known() && + (!and_determinism || aut->prop_universal().is_known())) + return sd.is_true(); + scc_info si(aut); + si.determine_unknown_acceptance(); + unsigned nscc = si.scc_count(); + assert(nscc); + std::vector reachable_from_acc(nscc); + bool semi_det = true; + do // iterator of SCCs in reverse topological order + { + --nscc; + if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc]) + { + for (unsigned succ: si.succ(nscc)) + reachable_from_acc[succ] = true; + for (unsigned src: si.states_of(nscc)) + { + bdd available = bddtrue; + for (auto& t: aut->out(src)) + if (!bdd_implies(t.cond, available)) + { + semi_det = false; + goto done; + } + else + { + available -= t.cond; + } + } + } + } + while (nscc); + done: + std::const_pointer_cast(aut) + ->prop_semi_deterministic(semi_det); + if (semi_det && and_determinism) + { + bool det = true; + nscc = si.scc_count(); + do // iterator of SCCs in reverse topological order + { + --nscc; + if (!si.is_accepting_scc(nscc) && !reachable_from_acc[nscc]) + { + for (unsigned src: si.states_of(nscc)) + { + bdd available = bddtrue; + for (auto& t: aut->out(src)) + if (!bdd_implies(t.cond, available)) + { + det = false; + goto done2; + } + else + { + available -= t.cond; + } + } + } + } + while (nscc); + done2: + std::const_pointer_cast(aut)->prop_universal(det); + } + return semi_det; + } + } + bool is_semi_deterministic(const const_twa_graph_ptr& aut) { - trival sd = aut->prop_semi_deterministic(); - if (sd.is_known()) - return sd.is_true(); - scc_info si(aut); - si.determine_unknown_acceptance(); - unsigned nscc = si.scc_count(); - assert(nscc); - std::vector reachable_from_acc(nscc); - bool semi_det = true; - do // iterator of SCCs in reverse topological order - { - --nscc; - if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc]) - { - for (unsigned succ: si.succ(nscc)) - reachable_from_acc[succ] = true; - for (unsigned src: si.states_of(nscc)) - { - bdd available = bddtrue; - for (auto& t: aut->out(src)) - if (!bdd_implies(t.cond, available)) - { - semi_det = false; - goto done; - } - else - { - available -= t.cond; - } - } - } - } - while (nscc); - done: - std::const_pointer_cast(aut) - ->prop_semi_deterministic(semi_det); - return semi_det; + return check_semi_determism(aut, false); + } + + void check_determinism(twa_graph_ptr aut) + { + check_semi_determism(aut, true); } } diff --git a/spot/twaalgos/isdet.hh b/spot/twaalgos/isdet.hh index d8aa23b16..1f750bdfb 100644 --- a/spot/twaalgos/isdet.hh +++ b/spot/twaalgos/isdet.hh @@ -91,5 +91,7 @@ namespace spot SPOT_API bool is_semi_deterministic(const const_twa_graph_ptr& aut); - + /// \brief Set the deterministic and semi-deterministic properties + /// appropriately. + SPOT_API void check_determinism(twa_graph_ptr aut); } diff --git a/tests/Makefile.am b/tests/Makefile.am index fd076c0df..1d3521eb2 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -379,6 +379,7 @@ TESTS_python = \ python/sbacc.py \ python/sccfilter.py \ python/sccinfo.py \ + python/semidet.py \ python/setacc.py \ python/setxor.py \ python/simstate.py \ diff --git a/tests/python/semidet.py b/tests/python/semidet.py new file mode 100644 index 000000000..022713f3e --- /dev/null +++ b/tests/python/semidet.py @@ -0,0 +1,39 @@ +# -*- mode: python; 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 . + +import spot + +formulas = [('(Gp0 | Fp1) M 1', False, True), + ('(!p1 U p1) U X(!p0 -> Fp1)', False, True), + ('(p1 | (Fp0 R (p1 W p0))) M 1', True, True), + ('!G(F(p1 & Fp0) W p1)', False, True), + ('X(!p0 W Xp1)', False, False), + ('FG(p0)', False, True) ] + +for f, isd, issd in formulas: + print(f) + aut = spot.translate(f) + # The formula with isd=True, issd=True is the only one + # for which both properties are already set. + assert (aut.prop_deterministic().is_maybe() or + aut.prop_semi_deterministic().is_maybe() or + isd == issd) + spot.check_determinism(aut) + assert aut.prop_deterministic() == isd + assert aut.prop_semi_deterministic() == issd