From f7d14ab5264e7f5da05a3c2af7b09d957837e116 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Wed, 31 May 2017 11:11:31 +0200 Subject: [PATCH] Degeneralization keeps track of levels. * NEWS: Document this. * spot/twa/twagraph.cc: `copy_state_names_from` handles this new info. * spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it. * tests/python/origstate.py, tests/python/simstate.py: Update tests to reflect the change. --- NEWS | 4 ++++ spot/twa/twagraph.cc | 21 +++++++++++++++++++++ spot/twaalgos/degen.cc | 4 ++++ spot/twaalgos/degen.hh | 3 +++ tests/python/origstate.py | 8 ++++---- tests/python/simstate.py | 24 ++++++++++++------------ 6 files changed, 48 insertions(+), 16 deletions(-) diff --git a/NEWS b/NEWS index 728f38fe0..26de8a415 100644 --- a/NEWS +++ b/NEWS @@ -54,6 +54,10 @@ 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 "degen-levels" keeps track + of the level of a state in a degeneralization. This information + complements the one carried in "original-states". + - 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 diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 422a8ee87..f69baa57c 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -607,6 +607,19 @@ namespace spot } os->resize(used_states); } + if (auto dl = get_named_prop>("degen-levels")) + { + unsigned size = dl->size(); + for (unsigned s = 0; s < size; ++s) + { + unsigned dst = newst[s]; + if (dst == s || dst == -1U) + continue; + assert(dst < s); + (*dl)[dst] = (*dl)[s]; + } + dl->resize(used_states); + } init_number_ = newst[init_number_]; g_.defrag_states(std::move(newst), used_states); } @@ -637,8 +650,11 @@ namespace spot return; auto orig = get_named_prop>("original-states"); + auto lvl = get_named_prop>("degen-levels"); auto sims = get_named_prop>("simulated-states"); + assert(!lvl || orig); + if (orig && sims) throw std::runtime_error("copy_state_names_from(): original-states and " "simulated-states are both set"); @@ -646,6 +662,9 @@ namespace spot if (orig && orig->size() != num_states()) throw std::runtime_error("copy_state_names_from(): unexpected size " "for original-states"); + if (lvl && lvl->size() != num_states()) + throw std::runtime_error("copy_state_names_from(): unexpected size " + "for degen-levels"); if (sims && sims->size() != other->num_states()) throw std::runtime_error("copy_state_names_from(): unexpected size " @@ -677,6 +696,8 @@ namespace spot throw std::runtime_error("copy_state_names_from(): state does not" " exist in source automaton"); newname = other->format_state(other_s); + if (lvl) + newname += '#' + std::to_string((*lvl)[s]); } names->emplace_back(newname); } diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index fd5760de4..235c635a9 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -240,8 +240,11 @@ namespace spot res->prop_copy(a, { false, true, true, true, true, true }); auto orig_states = new std::vector(); + auto levels = new std::vector(); orig_states->reserve(a->num_states()); // likely more are needed. + levels->reserve(a->num_states()); res->set_named_prop("original-states", orig_states); + res->set_named_prop("degen-levels", levels); // Create an order of acceptance conditions. Each entry in this // vector correspond to an acceptance set. Each index can @@ -328,6 +331,7 @@ namespace spot assert(ns == orig_states->size()); orig_states->emplace_back(ds.first); + levels->emplace_back(ds.second); // Level cache stores one encountered level for each state // (the value of use_lvl_cache determinates which level diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index 48579d839..ac0ce0510 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -56,6 +56,9 @@ namespace spot /// to retrieve it. Note that these functions may return the original /// automaton as-is if it is already degeneralized; in this case /// the "original-states" property is not defined. + /// Similarly, the property "degen-levels" keeps track of the degeneralization + /// levels. To retrieve it, call + /// `aut->get_named_prop>("degen-levels")`. /// \@{ SPOT_API twa_graph_ptr degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl = true, diff --git a/tests/python/origstate.py b/tests/python/origstate.py index 7c50c1d7e..0ca013889 100644 --- a/tests/python/origstate.py +++ b/tests/python/origstate.py @@ -67,15 +67,15 @@ acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc --BODY-- -State: 0 "0" {0} +State: 0 "0#1" {0} [0] 0 [!0] 1 [1] 2 -State: 1 "0" +State: 1 "0#0" [0] 0 [!0] 1 [1] 2 -State: 2 "1" {0} +State: 2 "1#1" {0} [1] 2 --END--""" @@ -90,7 +90,7 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc colored properties: deterministic --BODY-- -State: 0 "1" {0} +State: 0 "1#1" {0} [1] 0 --END--""" assert aut2.to_str() == ref diff --git a/tests/python/simstate.py b/tests/python/simstate.py index 677f70cf5..9c4943ac7 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -117,51 +117,51 @@ 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]₀}" +State: 0 "{₀[0#0,0#1]₀}" [0&!1] 0 [0&1] 1 [!0&1] 2 -State: 1 "{₀[0,0] [1]₀}" +State: 1 "{₀[0#0,0#1] [1#1]₀}" [0&!1] 3 [0&1] 4 [!0&1] 1 -State: 2 "{₀[1]₀}" +State: 2 "{₀[1#1]₀}" [0&!1] 5 {1} [0&1] 3 [!0&1] 0 -State: 3 "{₀[0,0]{₁[1]₁}₀}" +State: 3 "{₀[0#0,0#1]{₁[1#0]₁}₀}" [0&!1] 3 [0&1] 6 [!0&1] 7 -State: 4 "{₀[0,0] [1]{₁[1]₁}₀}" +State: 4 "{₀[0#0,0#1] [1#1]{₁[1#0]₁}₀}" [0&!1] 3 [0&1] 6 [!0&1] 7 -State: 5 "{₀[1]₀}" +State: 5 "{₀[1#0]₀}" [0&!1] 5 [0&1] 8 [!0&1] 0 -State: 6 "{₀[1]{₁[0,0] [1]₁}₀}" +State: 6 "{₀[1#1]{₁[0#0,0#1] [1#0]₁}₀}" [0&!1] 8 {1} [0&1] 9 {1} [!0&1] 1 {1} -State: 7 "{₀[1]{₁[0,0]₁}₀}" +State: 7 "{₀[1#1]{₁[0#0,0#1]₁}₀}" [0&!1] 8 {1} [0&1] 9 {1} [!0&1] 10 -State: 8 "{₀[0,0] [1]₀}" +State: 8 "{₀[0#0,0#1] [1#0]₀}" [0&!1] 8 [0&1] 9 [!0&1] 1 -State: 9 "{₀[0,0] [1] [1]₀}" +State: 9 "{₀[0#0,0#1] [1#1] [1#0]₀}" [0&!1] 3 [0&1] 4 [!0&1] 1 -State: 10 "{₀[0,0]{₁[1]₁}₀}" +State: 10 "{₀[0#0,0#1]{₁[1#1]₁}₀}" [0&!1] 3 {3} [0&1] 11 [!0&1] 7 -State: 11 "{₀[1]{₁[0,0]{₂[1]₂}₁}₀}" +State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}" [0&!1] 8 {1} [0&1] 9 {1} [!0&1] 1 {1}