From 7b5ab54530d7c45ede9db84c892e16b17b594472 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Fri, 19 May 2017 17:44:02 +0200 Subject: [PATCH] Simulation keeps track of simulated states in the input automaton. * NEWS: Document the change. * spot/twaalgos/simulation.cc: Implement the change. * spot/twa/twagraph.cc: `copy_state_names_from` uses simulated states info if present. * spot/twaalgos/determinize.cc: Pretty-print in determinization follows simulated states, avoiding possible confusion. * tests/Makefile.am, tests/python/simstate.py: Add a test. --- NEWS | 5 ++ spot/twa/twagraph.cc | 37 ++++++-- spot/twaalgos/determinize.cc | 21 +++-- spot/twaalgos/simulation.cc | 7 ++ tests/Makefile.am | 1 + tests/python/simstate.py | 169 +++++++++++++++++++++++++++++++++++ 6 files changed, 228 insertions(+), 12 deletions(-) create mode 100644 tests/python/simstate.py diff --git a/NEWS b/NEWS index 8ab1a2bc8..728f38fe0 100644 --- a/NEWS +++ b/NEWS @@ -54,6 +54,11 @@ New in spot 2.3.4.dev (not yet released) the second command outputs an automaton with states that show references to the first one. + - A new named property for automata called "simulated-states" can be + used to record the origin of a state through simulation. The + behavior is similar to "original-states" above. Determinization + takes advantage of this in its pretty print. + - The new function spot::acc_cond::is_streett_like() checks whether an acceptance condition is conjunction of disjunctive clauses containing at most one Inf and at most one Fin. It builds a diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 8ce477a2d..422a8ee87 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -635,11 +635,22 @@ namespace spot { if (other == shared_from_this()) return; + auto orig = get_named_prop>("original-states"); + auto sims = get_named_prop>("simulated-states"); + + if (orig && sims) + throw std::runtime_error("copy_state_names_from(): original-states and " + "simulated-states are both set"); + if (orig && orig->size() != num_states()) throw std::runtime_error("copy_state_names_from(): unexpected size " "for original-states"); + if (sims && sims->size() != other->num_states()) + throw std::runtime_error("copy_state_names_from(): unexpected size " + "for simulated-states"); + auto names = std::unique_ptr> (new std::vector); unsigned ns = num_states(); @@ -647,11 +658,27 @@ namespace spot for (unsigned s = 0; s < ns; ++s) { - unsigned other_s = orig ? (*orig)[s] : s; - if (other_s >= ons) - throw std::runtime_error("copy_state_names_from(): state does not" - " exist in source automaton"); - names->emplace_back(other->format_state(other_s)); + std::string newname = ""; + if (sims) + { + for (unsigned t = 0; t < ons; ++t) + { + if (s == (*sims)[t]) + newname += other->format_state(t) + ','; + } + assert(!newname.empty()); + newname.pop_back(); // remove trailing comma + newname = '[' + newname + ']'; + } + else + { + unsigned other_s = orig ? (*orig)[s] : s; + if (other_s >= ons) + throw std::runtime_error("copy_state_names_from(): state does not" + " exist in source automaton"); + newname = other->format_state(other_s); + } + names->emplace_back(newname); } set_named_prop("state-names", names.release()); diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index db63ba604..e5a7335c3 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -185,7 +185,8 @@ namespace spot } std::string - nodes_to_string(const safra_state::nodes_t& states) + nodes_to_string(const const_twa_graph_ptr& aut, + const safra_state::nodes_t& states) { auto copy = sorted_nodes(states); std::ostringstream os; @@ -223,7 +224,7 @@ namespace spot } if (!first) os << ' '; - os << n.first; + os << aut->format_state(n.first); first = false; } // Finish unwinding stack to print last braces @@ -236,11 +237,12 @@ namespace spot } std::vector* - print_debug(std::map& states) + print_debug(const const_twa_graph_ptr& aut, + const std::map& states) { auto res = new std::vector(states.size()); - for (auto& p: states) - (*res)[p.second] = nodes_to_string(p.first.nodes_); + for (const auto& p: states) + (*res)[p.second] = nodes_to_string(aut, p.first.nodes_); return res; } @@ -576,11 +578,16 @@ namespace spot // Degeneralize twa_graph_ptr aut = spot::degeneralize_tba(a); + if (pretty_print) + aut->copy_state_names_from(a); std::vector implications; if (use_simulation) { aut = spot::scc_filter(aut); - aut = simulation(aut, &implications); + auto aut2 = simulation(aut, &implications); + if (pretty_print) + aut2->copy_state_names_from(aut); + aut = aut2; } scc_info scc = scc_info(aut); std::vector is_connected = find_scc_paths(scc); @@ -694,7 +701,7 @@ namespace spot res->prop_state_acc(false); if (pretty_print) - res->set_named_prop("state-names", print_debug(seen)); + res->set_named_prop("state-names", print_debug(aut, seen)); return res; } } diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 6328a08ba..9fd965a7c 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -439,6 +439,10 @@ namespace spot res->copy_ap_of(a_); res->copy_acceptance_of(a_); + auto state_mapping = new std::vector(); + state_mapping->resize(a_->num_states()); + res->set_named_prop("simulated-states", state_mapping); + // Non atomic propositions variables (= acc and class) bdd nonapvars = all_proms_ & bdd_support(all_class_var_); @@ -454,6 +458,9 @@ namespace spot // its class, or by all the implied classes. auto s = gb->new_state(cl.id()); gb->alias_state(s, relation_[cl].id()); + // update state_mapping + for (auto& st : p.second) + (*state_mapping)[st] = s; if (implications) (*implications)[s] = relation_[cl]; } diff --git a/tests/Makefile.am b/tests/Makefile.am index 234a8a3e3..82e7b0f0e 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -362,6 +362,7 @@ TESTS_python = \ python/sccinfo.py \ python/setacc.py \ python/setxor.py \ + python/simstate.py \ python/rs_like.py \ python/sum.py \ python/trival.py \ diff --git a/tests/python/simstate.py b/tests/python/simstate.py new file mode 100644 index 000000000..677f70cf5 --- /dev/null +++ b/tests/python/simstate.py @@ -0,0 +1,169 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2015, 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 +from sys import exit + +aut = spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +--BODY-- +State: 0 +[t] 1 {0} +State: 1 +[t] 1 {0} +--END-- +""") + +aut2 = spot.simulation(aut) +assert aut2.to_str() == """HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc colored complete +properties: deterministic +--BODY-- +State: 0 {0} +[t] 0 +--END--""" + +aut2.copy_state_names_from(aut) +assert aut2.to_str() == """HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc colored complete +properties: deterministic +--BODY-- +State: 0 "[0,1]" {0} +[t] 0 +--END--""" + +aut = spot.translate('GF((p0 -> Gp0) R p1)') + +daut = spot.tgba_determinize(aut, True) +assert daut.to_str() == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "p1" "p0" +acc-name: parity min odd 4 +Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic stutter-invariant +--BODY-- +State: 0 "{₀[1]₀}" +[0&1] 1 {3} +[!0&1] 0 +[0&!1] 0 {1} +[!0&!1] 0 +State: 1 "{₀[1]{₂[0]₂}₀}{₁[2]₁}" +[0&1] 1 {3} +[!0&1] 2 +[0&!1] 0 {1} +[!0&!1] 0 {2} +State: 2 "{₀[1]₀}{₁[2]₁}" +[0&1] 1 {3} +[!0&1] 2 +[0&!1] 0 {1} +[!0&!1] 0 {2} +--END--""" + +aut = spot.automaton(""" +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Inf(0)&Inf(1) +--BODY-- +State: 0 +[0] 0 +[1] 1 {1} +State: 1 +[0] 1 {0} +[1] 0 +--END-- +""") + +daut = spot.tgba_determinize(aut, True) +assert daut.to_str() == """HOA: v1 +States: 12 +Start: 0 +AP: 2 "a" "b" +acc-name: parity min odd 4 +Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3))) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 "{₀[0,0]₀}" +[0&!1] 0 +[0&1] 1 +[!0&1] 2 +State: 1 "{₀[0,0] [1]₀}" +[0&!1] 3 +[0&1] 4 +[!0&1] 1 +State: 2 "{₀[1]₀}" +[0&!1] 5 {1} +[0&1] 3 +[!0&1] 0 +State: 3 "{₀[0,0]{₁[1]₁}₀}" +[0&!1] 3 +[0&1] 6 +[!0&1] 7 +State: 4 "{₀[0,0] [1]{₁[1]₁}₀}" +[0&!1] 3 +[0&1] 6 +[!0&1] 7 +State: 5 "{₀[1]₀}" +[0&!1] 5 +[0&1] 8 +[!0&1] 0 +State: 6 "{₀[1]{₁[0,0] [1]₁}₀}" +[0&!1] 8 {1} +[0&1] 9 {1} +[!0&1] 1 {1} +State: 7 "{₀[1]{₁[0,0]₁}₀}" +[0&!1] 8 {1} +[0&1] 9 {1} +[!0&1] 10 +State: 8 "{₀[0,0] [1]₀}" +[0&!1] 8 +[0&1] 9 +[!0&1] 1 +State: 9 "{₀[0,0] [1] [1]₀}" +[0&!1] 3 +[0&1] 4 +[!0&1] 1 +State: 10 "{₀[0,0]{₁[1]₁}₀}" +[0&!1] 3 {3} +[0&1] 11 +[!0&1] 7 +State: 11 "{₀[1]{₁[0,0]{₂[1]₂}₁}₀}" +[0&!1] 8 {1} +[0&1] 9 {1} +[!0&1] 1 {1} +--END--""" +