diff --git a/NEWS b/NEWS index 0436d7cf8..4a79a551c 100644 --- a/NEWS +++ b/NEWS @@ -56,6 +56,12 @@ New in spot 2.12.0.dev (not yet released) were missing the rule "[*0]|f ≡ f" when f already accepts the empty word. (Issue #545.) + - spot::match_states(A, B) is a new function that returns a vector + V such that V[x] contains all states y such that state (x, y) can + reach an accepting cycle in product(A, B). In particular, if A + and B accept the same language, any word accepted by A from state + x can be accepted in B from some state in V[x]. + Bug fixes: - Generating random formulas without any unary opertor would very diff --git a/python/spot/impl.i b/python/spot/impl.i index 6d91144d8..1f9c11fde 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -132,6 +132,7 @@ #include #include #include +#include #include #include #include @@ -522,6 +523,7 @@ namespace std { %template(pairintacccond) pair; %template(vectorformula) vector; %template(vectorunsigned) vector; + %template(vectorvectorunsigned) vector>; %template(vectorpairunsigned) vector>; %template(vectoracccond) vector; %template(vectoracccode) vector; @@ -739,6 +741,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 ede79f81a..b5993aaef 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -64,6 +64,7 @@ twaalgos_HEADERS = \ ltl2tgba_fm.hh \ magic.hh \ mask.hh \ + matchstates.hh \ minimize.hh \ mealy_machine.hh \ couvreurnew.hh \ @@ -139,6 +140,7 @@ libtwaalgos_la_SOURCES = \ ltl2tgba_fm.cc \ magic.cc \ mask.cc \ + matchstates.cc \ minimize.cc \ mealy_machine.cc \ couvreurnew.cc \ diff --git a/spot/twaalgos/matchstates.cc b/spot/twaalgos/matchstates.cc new file mode 100644 index 000000000..14edfe18b --- /dev/null +++ b/spot/twaalgos/matchstates.cc @@ -0,0 +1,50 @@ +// -*- 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 . + +#include "config.h" +#include +#include +#include + +namespace spot +{ + std::vector> + match_states(const const_twa_graph_ptr& aut1, + const const_twa_graph_ptr& aut2) + { + twa_graph_ptr prod = product(aut1, aut2); + product_states* ps = prod->get_named_prop("product-states"); + if (!ps) + return {}; + scc_info si(prod, scc_info_options::TRACK_SUCCS); + + std::vector> v(aut1->num_states()); + unsigned sz = ps->size(); + assert(sz == prod->num_states()); + for (unsigned sp = 0; sp < sz; ++sp) + if (si.is_useful_state(sp)) + { + auto [sl, sr] = (*ps)[sp]; + v[sl].push_back(sr); + } + return v; + } + + + +} diff --git a/spot/twaalgos/matchstates.hh b/spot/twaalgos/matchstates.hh new file mode 100644 index 000000000..7bd972402 --- /dev/null +++ b/spot/twaalgos/matchstates.hh @@ -0,0 +1,40 @@ +// -*- 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 . + +#pragma once + +#include +#include +#include + +namespace spot +{ + /// \ingroup twa_algorithms + /// \brief match the state of \a aut1 with the states of \a aut2. + /// + /// Return a vector `V` such that for each state `x` of + /// \a aut1, `V[x]` contains the set of states `y` such that + /// `(x,y)` is a useful state of `product(aut1,aut2)`. + /// + /// In particular, if the language of \a aut2 includes the language + /// of \a aut1, then any word accepted from state `x` in \a aut1 + /// is also accepted from one of the states in `V[x]`. + SPOT_API std::vector> + match_states(const const_twa_graph_ptr& aut1, + const const_twa_graph_ptr& aut2); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 54abc1a73..16b283077 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -435,6 +435,7 @@ TESTS_python = \ python/ltlf.py \ python/ltlparse.py \ python/ltlsimple.py \ + python/matchstates.py \ python/mealy.py \ python/_mealy.ipynb \ python/merge.py \ diff --git a/tests/python/matchstates.py b/tests/python/matchstates.py new file mode 100644 index 000000000..050a84b84 --- /dev/null +++ b/tests/python/matchstates.py @@ -0,0 +1,62 @@ +#!/usr/bin/python3 +# -*- 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() + +a = spot.automaton("""HOA: v1 +States: 4 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc stutter-invariant +properties: very-weak +--BODY-- +State: 0 "Ga | Gb | Gc" +[0] 1 +[1] 2 +[2] 3 +State: 1 "Ga" +[0] 1 +State: 2 "Gb" +[1] 2 +State: 3 "Gc" +[2] 3 +--END--""") + +b = spot.automaton("""HOA: v1 States: 7 Start: 6 AP: 3 "a" "b" "c" +acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels +state-acc deterministic properties: stutter-invariant very-weak +--BODY-- State: 0 [2] 0 State: 1 [!1&2] 0 [1&2] 1 [1&!2] 2 State: 2 +[1] 2 State: 3 [0] 3 State: 4 [!0&2] 0 [0&!2] 3 [0&2] 4 State: 5 +[!0&1] 2 [0&!1] 3 [0&1] 5 State: 6 [!0&!1&2] 0 [!0&1&2] 1 [!0&1&!2] 2 +[0&!1&!2] 3 [0&!1&2] 4 [0&1&!2] 5 [0&1&2] 6 --END--""") + +m1 = spot.match_states(a, b) +tc.assertEqual(m1, ((6,), (3, 4, 5, 6), (1, 2, 5, 6), (0, 1, 4, 6))) +m2 = spot.match_states(b, a) +tc.assertEqual(m2, ((3,), (2, 3), (2,), (1,), (1, 3), (1, 2), (0, 1, 2, 3))) + +c = spot.translate('false') +m3 = spot.match_states(a, c) +tc.assertEqual(m3, ((), (), (), ())) +m4 = spot.match_states(c, a) +tc.assertEqual(m4, ((), ))