diff --git a/NEWS b/NEWS index e3b2a9329..958ea1645 100644 --- a/NEWS +++ b/NEWS @@ -120,6 +120,12 @@ New in spot 2.11.6.dev (not yet released) - ltsmin's interface will now point to README.ltsmin in case an error is found while running divine or spins. + - spot::is_safety_automaton() was generalized to detect any + automaton for which the acceptance could be changed to "t" without + changing the language. In previous versions this function assumed + weak automata as input, but the documentation did not reflect + this. + Python: - The spot.automata() and spot.automaton() functions now accept a diff --git a/THANKS b/THANKS index 46e747d4e..4eb4a598c 100644 --- a/THANKS +++ b/THANKS @@ -56,6 +56,7 @@ Raven Beutner Reuben Rowe Roei Nahum Rüdiger Ehlers +Samuel Judson Shachar Itzhaky Shengping Shaw Shufang Zhu diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 0ba9d0637..ff7a69266 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -23,6 +23,8 @@ #include #include #include +#include +#include using namespace std::string_literals; @@ -182,23 +184,55 @@ namespace spot { if (aut->acc().is_t()) return true; + if (!aut->is_existential()) + throw std::runtime_error + ("is_safety_automaton() does not support alternation"); - bool need_si = !si; - if (need_si) - si = new scc_info(aut); + std::unique_ptr localsi; + if (!si) + { + localsi = std::make_unique(aut); + si = localsi.get(); + } + si->determine_unknown_acceptance(); - bool res = true; - unsigned scount = si->scc_count(); - for (unsigned scc = 0; scc < scount; ++scc) - if (!si->is_trivial(scc) && si->is_rejecting_scc(scc)) + // a trim automaton without rejecting cycle is a safety automaton + bool has_rejecting_cycle = false; + + // first, look for rejecting SCCs. + unsigned scccount = si->scc_count(); + for (unsigned scc = 0; scc < scccount; ++scc) + if (si->is_useful_scc(scc) + && !si->is_trivial(scc) + && si->is_rejecting_scc(scc)) { - res = false; + has_rejecting_cycle = true; break; } + if (!has_rejecting_cycle && !aut->prop_inherently_weak().is_true()) + { + // maybe we have rejecting cycles inside accepting SCCs? + for (unsigned scc = 0; scc < scccount; ++scc) + if (si->is_useful_scc(scc) + && !si->is_trivial(scc) + && si->is_accepting_scc(scc) + && scc_has_rejecting_cycle(*si, scc)) + { + has_rejecting_cycle = true; + break; + } + } + if (!has_rejecting_cycle) + return true; - if (need_si) - delete si; - return res; + // If the automaton has a rejecting loop and is deterministic, it + // cannot be a safety automaton. + if (is_universal(aut)) + return false; + + twa_graph_ptr b = make_twa_graph(aut, twa::prop_set::all()); + strip_acceptance_here(b); + return spot::contains(aut, b); } diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index 15122518a..baaaefe99 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -104,12 +104,24 @@ namespace spot /// \brief Check whether an automaton is a safety automaton. /// - /// A safety automaton has only accepting SCCs (or trivial - /// SCCs). + /// An automaton is a safety automaton if its acceptance condition + /// can be changed to "true" without changing its language. /// - /// A minimized WDBA (as returned by a successful run of - /// minimize_obligation()) represents safety property if it is a - /// safety automaton. + /// The test performed by this function differs depending on + /// the nature of the input \a aut. + /// + /// If \a aut is an automaton with `t` acceptance, it is necessarily + /// a safety automaton. + /// + /// Else we check for the absence of rejecting cycle in the + /// useful part of the automaton. This absence is only a sufficient + /// condition in the non-deterministic case, because a rejecting + /// run might correspond to a word that is accepted by another run. + /// + /// If the previous test could not conclude, we build the automaton + /// B that is a copy of \a aut with acceptance set to true, and we + /// check that \a aut contains all words of B. This last test + /// requires complementing \a aut. /// /// \param aut the automaton to check /// diff --git a/tests/Makefile.am b/tests/Makefile.am index f6c303dd5..3609ec03b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -446,6 +446,7 @@ TESTS_python = \ python/relabel.py \ python/remfin.py \ python/removeap.py \ + python/safety.py \ python/satmin.py \ python/sbacc.py \ python/sccfilter.py \ diff --git a/tests/python/safety.py b/tests/python/safety.py new file mode 100644 index 000000000..e6376ef4f --- /dev/null +++ b/tests/python/safety.py @@ -0,0 +1,52 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) by the Spot authors, see the AUTHORS file for details. +# +# 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 +from unittest import TestCase +tc = TestCase() + + +for f in ['Fb', 'GFa & GFb', + '(p0 W Fp0) R ((Gp1 & Fp1) | (F!p1 & G!p1)) & GFp0', + 'GFp0 xor GFp1']: + aut = spot.translate(f, 'BA') + tc.assertFalse(spot.is_safety_automaton(aut)) + + aut = spot.translate(f, 'BA') + tc.assertFalse(spot.is_safety_automaton(aut)) + + aut = spot.translate(f, 'deterministic', 'complete') + tc.assertFalse(spot.is_safety_automaton(aut)) + + aut = spot.translate(f, 'generic', 'sbacc') + tc.assertFalse(spot.is_safety_automaton(aut)) + +for f in ['Gb', 'Ga|Gb|Gc', 'Fr->(!p U r)', 'p1 M F(p1 U (Gp0 U X(0)))', + '((p1 U !p0) M !FXp1) W p0', 'p0 & ((!p1 | (p1 W X!p1)) M p1)', + '(p0 W Fp0) R ((Gp1 & Fp1) | (F!p1 & G!p1))']: + aut = spot.translate(f, 'BA') + tc.assertTrue(spot.is_safety_automaton(aut)) + + ba = spot.translate(f, 'BA', 'complete') + tc.assertTrue(spot.is_safety_automaton(aut)) + + ba = spot.translate(f, 'deterministic', 'complete') + tc.assertTrue(spot.is_safety_automaton(aut)) + + ba = spot.translate(f, 'generic', 'sbacc') + tc.assertTrue(spot.is_safety_automaton(aut))