alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

introduce original-states

Browse source 
* spot/twaalgos/degen.cc, spot/twaalgos/degen.hh,
spot/twaalgos/mask.hh: Store original states in "original-states"
properties.
* spot/twaalgos/dot.cc: Add support for option 'd'.
* bin/common_aoutput.cc: Document it.
* doc/org/concepts.org, NEWS: Document "original-states".
* tests/core/readsave.test: Add some tests.
This commit is contained in:
Alexandre Duret-Lutz 2017-04-20 18:11:29 +02:00
parent e7797b727d
commit 07c2dd3b64
8 changed files with 141 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

17
NEWS
View file

@ -20,6 +20,23 @@ New in spot 2.3.3.dev (not yet released)
- spot::dtwa_complement now simply returns the result of dualize()
- There is a new named property for automata called
"original-states" that can be used to record the origin of a state
when an automaton is transformed. It is currently defined by the
degeneralization algorithms, and by transform_accessible() and
algorithms based on it (like remove_ap::strip(),
decompose_strength(), decompose_scc()). This is realy meant as an
aid for writing algorithms that need this mapping, but it can also
be used to debug these algorithms: the "original-states"
information is displayed by the dot printer when the 'd' option is
passed. For instance in
% ltl2tgba 'GF(a <-> Fb)' --dot=s
% ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=ds
the second command outputs an automaton with states that show
references to the first one.
Bugs fixed:
- the transformation to state-based acceptance (spot::sbacc()) was

13
bin/common_aoutput.cc
View file

@ -92,17 +92,22 @@ static const argp_option options[] =
OPTION_ARG_OPTIONAL,
"GraphViz's format. Add letters for "
"(1) force numbered states, "
"(a) acceptance display, (b) acceptance sets as bullets, "
"(a) display acceptance, "
"(b) acceptance sets as bullets, "
"(B) bullets except for Büchi/co-Büchi automata, "
"(c) force circular nodes, "
"(C) color nodes with COLOR, "
"(d) show origins when known, "
"(e) force elliptic nodes, "
"(f(FONT)) use FONT, (h) horizontal layout, "
"(f(FONT)) use FONT, "
"(h) horizontal layout, "
"(k) use state labels when possible, "
"(n) with name, (N) without name, "
"(n) with name, "
"(N) without name, "
"(o) ordered transitions, "
"(r) rainbow colors for acceptance sets, "
"(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
"(R) color acceptance sets by Inf/Fin, "
"(s) with SCCs, "
"(t) force transition-based acceptance, "
"(v) vertical layout, "
"(y) split universal edges by color, "

1
doc/org/concepts.org
View file

@ -1118,6 +1118,7 @@ Here is a list of named properties currently used inside Spot:
|---------------------+--------------------------------+---------------------------------------------------------------------------------------------------------------------------------|
| ~automaton-name~ | ~std::string~ | name for the automaton, for instance to display in the HOA format |
| ~product-states~ | ~const spot::product_states~ | vector of pairs of states giving the left and right operands of each state in a product automaton |
| ~original-states~ | ~std::vector<unsigned>~ | original state number before transformation (used by some algorithms like =degeneralize()=) |
| ~state-names~ | ~std::vector<std::string>~ | vector naming each state of the automaton, for display purpose |
| ~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 |

69
spot/twaalgos/degen.cc
View file

@ -214,6 +214,10 @@ namespace spot
// Preserve determinism, weakness, and stutter-invariance
res->prop_copy(a, { false, true, true, true, true, true });
auto orig_states = new std::vector<unsigned>();
orig_states->reserve(a->num_states()); // likely more are needed.
res->set_named_prop("original-states", orig_states);
// Create an order of acceptance conditions. Each entry in this
// vector correspond to an acceptance set. Each index can
// be used as a level in degen_state to indicate the next expected
@ -290,16 +294,37 @@ namespace spot
s.second = 0;
}
ds2num[s] = res->new_state();
todo.emplace_back(s);
auto new_state = [&](degen_state& ds)
{
unsigned ns = res->new_state();
ds2num[ds] = ns;
todo.emplace_back(ds);
// If use_lvl_cache is on insert initial state to level cache
// Level cache stores first encountered level for each state.
// When entering an SCC first the lvl_cache is checked.
// If such state exists level from chache is used.
// If not, a new level (starting with 0) is computed.
if (use_lvl_cache)
lvl_cache[s.first] = std::make_pair(s.second, true);
assert(ns == orig_states->size());
orig_states->emplace_back(ds.first);
// Level cache stores one encountered level for each state
// (the value of use_lvl_cache determinates which level
// should be remembered).
// When entering an SCC first the lvl_cache is checked.
// If such state exists level from chache is used.
if (use_lvl_cache)
{
unsigned lvl = ds.second;
if (lvl_cache[ds.first].second)
{
if (use_lvl_cache == 3)
lvl = std::max(lvl_cache[ds.first].first, lvl);
else if (use_lvl_cache == 2)
lvl = std::min(lvl_cache[ds.first].first, lvl);
else
lvl = lvl_cache[ds.first].first; // Do not change
}
lvl_cache[ds.first] = std::make_pair(lvl, true);
}
return ns;
};
new_state(s);
while (!todo.empty())
{
@ -502,31 +527,9 @@ namespace spot
int dest;
ds2num_map::const_iterator di = ds2num.find(d);
if (di != ds2num.end())
{
dest = di->second;
}
dest = di->second;
else
{
dest = res->new_state();
ds2num[d] = dest;
todo.emplace_back(d);
// Insert new state to cache
if (use_lvl_cache)
{
auto lvl = d.second;
if (lvl_cache[d.first].second)
{
if (use_lvl_cache == 3)
lvl = std::max(lvl_cache[d.first].first, lvl);
else if (use_lvl_cache == 2)
lvl = std::min(lvl_cache[d.first].first, lvl);
else
lvl = lvl_cache[d.first].first; // Do not change
}
lvl_cache[d.first] = std::make_pair(lvl, true);
}
}
dest = new_state(d);
unsigned& t = tr_cache[dest * 2 + is_acc];

10
spot/twaalgos/degen.hh
View file

@ -1,5 +1,5 @@
// -*- 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.
//
// This file is part of Spot, a model checking library.
@ -48,6 +48,14 @@ namespace spot
///
/// The degeneralize_tba() variant produce a degeneralized automaton
/// with transition-based acceptance.
///
/// The mapping between each state of the resulting automaton
/// and the original state of the input automaton is stored in the
/// "original-states" named property of the produced automaton. Call
/// `aut->get_named_prop<std::vector<unsigned>>("original-states")`
/// 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.
/// \@{
SPOT_API twa_graph_ptr
degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl = true,

18
spot/twaalgos/dot.cc
View file

@ -67,6 +67,7 @@ namespace spot
std::map<unsigned, unsigned>* highlight_edges_ = nullptr;
std::map<unsigned, unsigned>* highlight_states_ = nullptr;
std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
std::vector<unsigned>* orig_ = nullptr;
std::set<unsigned>* incomplete_ = nullptr;
std::string* name_ = nullptr;
acc_cond::mark_t inf_sets_ = 0U;
@ -87,6 +88,7 @@ namespace spot
bool opt_all_bullets = false;
bool opt_ordered_edges_ = false;
bool opt_numbered_edges_ = false;
bool opt_orig_show_ = false;
bool max_states_given_ = false; // related to max_states_
const_twa_graph_ptr aut_;
@ -199,6 +201,9 @@ namespace spot
options = end + 1;
}
break;
case 'd':
opt_orig_show_ = true;
break;
case 'e':
opt_shape_ = ShapeEllipse;
break;
@ -520,6 +525,8 @@ namespace spot
os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
else
os_ << s;
if (orig_ && s < orig_->size())
os_ << " (" << (*orig_)[s] << ')';
if (acc)
{
os_ << "\\n";
@ -538,6 +545,8 @@ namespace spot
os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
else
os_ << s;
if (orig_ && s < orig_->size())
os_ << " (" << (*orig_)[s] << ')';
if (acc)
{
os_ << "<br/>";
@ -557,6 +566,8 @@ namespace spot
os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
else
os_ << s;
if (orig_ && s < orig_->size())
os_ << " (" << (*orig_)[s] << ')';
if (opt_state_labels_)
escape_str(os_ << "\\n", state_label(s));
os_ << '"';
@ -687,6 +698,8 @@ namespace spot
sprod_ = nullptr;
}
}
if (opt_orig_show_)
orig_ = aut->get_named_prop<std::vector<unsigned>>("original-states");
if (opt_state_labels_)
{
// Verify that we can use state labels for this automaton.
@ -720,11 +733,12 @@ namespace spot
&& aut_->prop_state_acc().is_true());
if (opt_shape_ == ShapeAuto)
{
if (sn_ || sprod_ || aut->num_states() > 100 || opt_state_labels_)
if (sn_ || sprod_ || aut->num_states() > 100
|| opt_state_labels_ || orig_)
{
opt_shape_ = ShapeEllipse;
// If all state names are short, prefer circles.
if (!opt_state_labels_ &&
if (!opt_state_labels_ && !orig_ &&
sn_ && std::all_of(sn_->begin(), sn_->end(),
[](const std::string& s)
{ return s.size() <= 2; }))

40
spot/twaalgos/mask.hh
View file

@ -25,19 +25,26 @@ namespace spot
{
/// \brief Clone and mask an automaton.
///
/// Copy the edges of automaton \a old, into automaton
/// \a cpy, creating new states at the same time. The argument \a
/// trans should behave as a function with the following prototype:
/// Copy the edges of automaton \a old into the empty automaton \a
/// cpy, creating new states as needed. The argument \a trans
/// should behave as a function with the following prototype:
/// <code>
/// void (*trans) (unsigned src, bdd& cond, acc_cond::mark_t& acc,
/// unsigned dst)
/// </code>
/// It can modify either the condition or the acceptance sets of
/// the edges. Set the condition to bddfalse to remove the edge
/// (this will also remove the destination state and its descendants
/// if they are not reachable by another edge).
///
/// The \a trans function may modify either the condition or the
/// acceptance sets of the edges. Set the condition to bddfalse to
/// remove the edge (this will also remove the destination state and
/// its descendants if they are not reachable by another edge).
///
/// The mapping between each state of the resulting automaton
/// and the original state of the input automaton is stored in the
/// "original-states" named property of the produced automaton. Call
/// `aut->get_named_prop<std::vector<unsigned>>("original-states")`
/// to retrieve it.
///
/// \param init The optional new initial state.
template<typename Trans>
void transform_accessible(const const_twa_graph_ptr& old,
twa_graph_ptr& cpy,
@ -50,6 +57,10 @@ namespace spot
std::vector<unsigned> todo;
std::vector<unsigned> seen(old->num_states(), -1U);
auto orig_states = new std::vector<unsigned>();
orig_states->reserve(old->num_states()); // maybe less are needed.
cpy->set_named_prop("original-states", orig_states);
auto new_state =
[&](unsigned old_state) -> unsigned
{
@ -58,12 +69,17 @@ namespace spot
{
tmp = cpy->new_state();
seen[old_state] = tmp;
orig_states->emplace_back(old_state);
todo.emplace_back(old_state);
}
return tmp;
};
cpy->set_init_state(new_state(init));
if (seen[init] != 0)
throw std::runtime_error
("the destination automaton of transform_accessible() should be empty");
while (!todo.empty())
{
unsigned old_src = todo.back();
@ -79,11 +95,12 @@ namespace spot
trans(t.src, cond, acc, t.dst);
if (cond != bddfalse)
cpy->new_edge(new_src,
new_state(t.dst),
cond, acc);
cpy->new_edge(new_src, new_state(t.dst),
cond, acc);
}
}
orig_states->shrink_to_fit();
}
/// \brief Copy an automaton and update each edge.
@ -133,6 +150,7 @@ namespace spot
{
transform_accessible(old, cpy, trans, old->get_init_state_number());
}
template<typename Trans>
void transform_copy(const const_twa_graph_ptr& old,
twa_graph_ptr& cpy,

25
tests/core/readsave.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de
# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016, 2017 Laboratoire de
# Recherche et Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -1041,3 +1041,26 @@ test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count`
test 2 = `genltl --dac=1..3 | ltl2tgba --stats='%e,"%h",%s' |
dstar2tgba -F-/2 --stats='%<,%>,"%h"' |
autfilt --states=2..3 -F-/3 --stats='%<,"%h"' | wc -l`
# --dot=d
ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=d | grep ' (' >out
cat >expected <<EOF
0 [label="0 (0)", peripheries=2]
1 [label="1 (0)"]
2 [label="2 (1)"]
3 [label="3 (2)", peripheries=2]
4 [label="4 (2)"]
EOF
diff out expected
# --dot=d should also not use circles
ltl2tgba 'a U b' | autfilt --remove-ap=b=0 --dot=d >out
cat >expected <<EOF
digraph G {
rankdir=LR
I [label="", style=invis, width=0]
I -> 0
0 [label="0 (1)"]
0 -> 0 [label="a"]
}
EOF
diff out expected