Commit 4f8a8f73 authored by Maximilien Colange's avatar Maximilien Colange

Properly handle "simulated-states" property in twagraph::defrag_states.

* spot/twa/twagraph.cc: Implement the change.
* spot/twaalgos/simulation.hh: Improve documentation.
* tests/python/simstate.py: Improve the test.
* doc/org/concepts.org: Typo.
parent acbb5106
......@@ -1128,7 +1128,7 @@ Here is a list of named properties currently used inside Spot:
| ~highlight-edges~ | ~std::map<unsigned, unsigned>~ | map of (edge number, color number) for highlighting the output |
| ~highlight-states~ | ~std::map<unsigned, unsigned>~ | map of (state number, color number) for highlighting the output |
| ~incomplete-states~ | ~std::set<unsigned>~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) |
| ~degen-levels~ | ~std::vector<unsigned>~ | level associated to each state by the degenaralization algorithm |
| ~degen-levels~ | ~std::vector<unsigned>~ | level associated to each state by the degeneralization algorithm |
| ~simulated-states~ | ~std::vector<unsigned>~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions |
Objects referenced via named properties are automatically destroyed
......
......@@ -620,6 +620,16 @@ namespace spot
}
dl->resize(used_states);
}
if (auto ss = get_named_prop<std::vector<unsigned>>("simulated-states"))
{
for (auto& s : *ss)
{
if (s >= newst.size())
s = -1U;
else
s = newst[s];
}
}
init_number_ = newst[init_number_];
g_.defrag_states(std::move(newst), used_states);
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2015, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -64,6 +64,12 @@ namespace spot
/// acceptance conditions than necessary, and running scc_filter()
/// again afterwards will remove these superfluous conditions.
///
/// The resulting automaton has a named property "simulated-states", that is a
/// vector mapping each state of the input to a state of the output. Note that
/// some input states may be mapped to -1, as a by-product of improved
/// determinism. Typically, if the language of q1 is included in the language
/// of q2, only a transition to q2 will be built.
///
/// \param automaton the automaton to simulate.
/// \return a new automaton which is at worst a copy of the received
/// one
......
......@@ -166,3 +166,23 @@ State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}"
[0&1] 9 {1}
[!0&1] 1 {1}
--END--"""
a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)')
a = spot.degeneralize_tba(a)
b = spot.simulation(a)
b.set_init_state(1)
b.purge_unreachable_states()
b.copy_state_names_from(a)
assert b.to_str() == """HOA: v1
States: 1
Start: 0
AP: 2 "p0" "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0 "[1,8,9]"
[1] 0
[!1] 0 {0}
--END--"""
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment