From 634dd283791b36ac1e761b59ddd1ad8f9159f59c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 17 May 2021 18:30:16 +0200 Subject: [PATCH] merge_states: include sorting and detection of identical self-loops * spot/twa/twagraph.cc: Implement it. * spot/twa/twagraph.hh, NEWS: Document it. * tests/python/mergedge.py: Test it. * tests/core/ltlsynt.test, tests/python/games.ipynb: Adjust expectations. --- NEWS | 5 +++++ spot/twa/twagraph.cc | 25 ++++++++++++++++++++++++- spot/twa/twagraph.hh | 12 ++++++++---- tests/core/ltlsynt.test | 36 ++++++++++++++++++------------------ tests/python/games.ipynb | 6 +++--- tests/python/mergedge.py | 32 +++++++++++++++++++++++++++++++- 6 files changed, 89 insertions(+), 27 deletions(-) diff --git a/NEWS b/NEWS index 2db96f234..db1db6ac1 100644 --- a/NEWS +++ b/NEWS @@ -224,6 +224,11 @@ New in spot 2.9.7.dev (not yet released) that error messages should be emitted as if the next automaton was read from "filename" starting on line 10. (Issue #232) + - spot::twa_graph::merge_states() will now sort the vector of edges + before attempting to detect mergeable states. When merging states + with identical outgoing transitions, it will now also consider + self-looping transitions has having identical destinations. + Python: - Bindings for functions related to games. diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 6d98b5f07..93d042521 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -295,6 +295,27 @@ namespace spot throw std::runtime_error( "twa_graph::merge_states() does not work on alternating automata"); + typedef graph_t::edge_storage_t tr_t; + g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs) + { + if (lhs.src < rhs.src) + return true; + if (lhs.src > rhs.src) + return false; + if (lhs.acc < rhs.acc) + return true; + if (lhs.acc > rhs.acc) + return false; + if (bdd_less_than_stable lt; lt(lhs.cond, rhs.cond)) + return true; + if (rhs.cond != lhs.cond) + return false; + // The destination must be sorted last + // for our self-loop optimization to work. + return lhs.dst < rhs.dst; + }); + g_.chain_edges_(); + const unsigned nb_states = num_states(); std::vector remap(nb_states, -1U); for (unsigned i = 0; i != nb_states; ++i) @@ -306,7 +327,9 @@ namespace spot if (std::equal(out1.begin(), out1.end(), out2.begin(), out2.end(), [](const edge_storage_t& a, const edge_storage_t& b) - { return a.dst == b.dst && a.data() == b.data(); })) + { return ((a.dst == b.dst + || (a.dst == a.src && b.dst == b.src)) + && a.data() == b.data()); })) { remap[i] = j; break; diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 77ca9284a..c5bd22d4e 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -572,10 +572,14 @@ namespace spot /// \brief Merge states that can be merged. /// - /// This merges states that have the exact same outgoing edges. This method - /// compares the successors of states in the order in which they are stored. - /// Therefore, it is better to call it when you know that the edges are - /// stored, e.g. after a call to merge_edges(). + /// Two states can be merged if the set of outgoing transitions + /// is identical, i.e., same condition, same colors, same destination. + /// Two self-loops with the same condition and colors are considered + /// identical even if they do not actually have the same destination. + /// + /// The implementation will sort the edges of the automaton to + /// ease the comparison between two states. This may miss some + /// self-loop based in non-deterministic automata. void merge_states(); /// \brief Remove all dead states diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index c924a9a1e..97a431872 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -45,18 +45,18 @@ parity 17; parity 13; 0 1 0 1,2 "INIT"; 2 1 1 3; -3 3 0 4,5; +3 3 0 5,4; +4 2 1 12,3; +12 2 0 5,4; 5 1 1 6,7; -7 1 0 8,9; -9 1 1 10,11; -11 1 0 8,9; -8 3 1 3,12; -12 2 0 4,5; -4 2 1 3,12; -10 2 0 8,9; +7 1 0 9,8; +8 3 1 12,3; +9 1 1 11,10; +10 2 0 9,8; +11 1 0 9,8; 6 1 0 13,4; 13 1 1 6,10; -1 1 1 3,6; +1 1 1 6,3; parity 5; 1 1 0 4,5 "INIT"; 5 5 1 0,1; @@ -86,11 +86,11 @@ aag 16 1 2 1 13 16 14 3 18 14 2 20 5 6 -22 20 2 -24 20 3 -26 17 25 +22 20 3 +24 20 2 +26 17 23 28 11 26 -30 19 23 +30 19 25 32 13 30 i0 a o0 b @@ -133,11 +133,11 @@ aag 16 1 2 2 13 16 14 3 18 14 2 20 5 6 -22 20 2 -24 20 3 -26 17 25 +22 20 3 +24 20 2 +26 17 23 28 11 26 -30 19 23 +30 19 25 32 13 30 i0 a o0 b @@ -378,6 +378,6 @@ f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))' ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 13 states' err ltlsynt -x dpa-simul=0 --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err -grep 'DPA has 30 states' err +grep 'DPA has 29 states' err ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 12 states' err diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index 2da7d8a03..1030da908 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -960,23 +960,23 @@ "[!0] 3 {1}\n", "[0] 4 {1}\n", "State: 2\n", - "[0] 4 {1}\n", "[!0] 5 {1}\n", + "[0] 4 {1}\n", "State: 3\n", "[!1] 6 {1}\n", "[1] 7 {2}\n", "State: 4\n", "[t] 8 {2}\n", "State: 5\n", - "[1] 7 {2}\n", "[!1] 6 {1}\n", + "[1] 7 {2}\n", "State: 6\n", "[t] 3 {1}\n", "State: 7\n", "[t] 5 {2}\n", "State: 8\n", - "[0] 4 {2}\n", "[!0] 9 {1}\n", + "[0] 4 {2}\n", "State: 9\n", "[t] 10 {1}\n", "State: 10\n", diff --git a/tests/python/mergedge.py b/tests/python/mergedge.py index e1dffc80a..b0325603e 100644 --- a/tests/python/mergedge.py +++ b/tests/python/mergedge.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2020, 2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -53,3 +53,33 @@ assert aut.num_edges() == 9 aut.merge_edges() assert aut.num_edges() == 5 assert spot.is_deterministic(aut) + +aut = spot.automaton(""" +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +--BODY-- +State: 0 +[!0] 1 {0} +[0] 2 {0} +State: 1 +[!0] 1 {0} +[0] 1 +State: 2 +[!0] 2 {0} +[0] 1 +--END--""") +aut.merge_states() +assert aut.num_edges() == 4 +assert aut.num_states() == 2 +assert spot.is_deterministic(aut) +assert aut.prop_complete() +aut.merge_states() +assert aut.num_edges() == 4 +assert aut.num_states() == 2 +assert spot.is_deterministic(aut) +assert aut.prop_complete()