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

fix handling of Rabin-like input for dnf_to_dca()

Browse source 
The bug is mentioned by Maximilien Colange in a comment to issue #317,
but turned out to be unrelated to that original issue.

* spot/twaalgos/totgba.cc (dnf_to_streett): Save the correspondence
between the created states an the DNF clause in a named property.
* doc/org/concepts.org, spot/twaalgos/totgba.hh: Mention the new
property.
* spot/twaalgos/cobuchi.cc (save_inf_nca_st): Rewrite using the named
property.  Relying on seen marks and trying to deduce the matching
original clause could only work from plain Rabin.
* tests/core/dca.test: Add the test from Maximilien.
* NEWS: Mention the issue.
This commit is contained in:
Alexandre Duret-Lutz 2018-02-18 15:20:53 +01:00
parent 69f31c89c6
commit 81e5357e62
6 changed files with 63 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -25,6 +25,8 @@ New in spot 2.5.0.dev (not yet released)
condition (by merging identical set) prior to running the
conversion to Büchi.
- dnf_to_dca() was mishandling some Rabin-like input.
New in spot 2.5 (2018-01-20)
Build:

25
doc/org/concepts.org
View file

@ -1119,18 +1119,19 @@ method.
Here is a list of named properties currently used inside Spot:
| key name | (pointed) value type | description |
|---------------------+--------------------------------+---------------------------------------------------------------------------------------------------------------------------------|
| ~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 |
| ~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 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 |
| ~synthesis-outputs~ | ~bdd~ | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit)
| key name | (pointed) value type | description |
|---------------------+--------------------------------+-------------------------------------------------------------------------------------------------------------------------------------------------------|
| ~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()=) |
| ~original-clauses~ | ~std::vector<unsigned>~ | original DNF clause associated to each state in automata created by =dnf_to_streett()= |
| ~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 |
| ~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 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 |
| ~synthesis-outputs~ | ~bdd~ | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit) |
Objects referenced via named properties are automatically destroyed
when the automaton is destroyed, but this can be altered by passing a
custom destructor as a third parameter to =twa::set_named_prop()=.

59
spot/twaalgos/cobuchi.cc
View file

@ -134,38 +134,27 @@ namespace spot
unsigned nb_states_; // Number of states.
unsigned was_rabin_; // Was it Rabin before Streett?
std::vector<unsigned>* orig_states_; // Match old Rabin st. from new.
std::vector<unsigned>* orig_clauses_; // Associated Rabin clauses.
unsigned orig_num_st_; // Rabin original nb states.
// Keep information of states that are wanted to be seen infinitely
// often (cf Header).
void save_inf_nca_st(unsigned s, acc_cond::mark_t m,
vect_nca_info* nca_info)
void save_inf_nca_st(unsigned s, vect_nca_info* nca_info)
{
if (was_rabin_ && m)
const pair_state_nca& st = (*res_map_)[s];
auto bv = make_bitvect(orig_num_st_);
for (unsigned state : pmap_.states_of(st.second))
bv->set(state);
unsigned clause = 0;
unsigned state = st.first;
if (was_rabin_)
{
for (unsigned p = 0; p < nb_pairs_; ++p)
if (pairs_[p].fin || m & pairs_[p].inf)
{
const pair_state_nca& st = (*res_map_)[s];
auto bv = make_bitvect(orig_num_st_);
for (unsigned state : pmap_.states_of(st.second))
bv->set(state);
assert(!was_rabin_
|| ((int)(*orig_states_)[st.first] >= 0));
unsigned state = was_rabin_ ? (*orig_states_)[st.first]
: st.first;
unsigned clause_nb = was_rabin_ ? p / 2 : p;
nca_info->push_back(new nca_st_info(clause_nb, state, bv));
}
}
else if (!was_rabin_)
{
const pair_state_nca& st = (*res_map_)[s];
auto bv = make_bitvect(aut_->num_states());
for (unsigned state : pmap_.states_of(st.second))
bv->set(state);
nca_info->push_back(new nca_st_info(0, st.first, bv));
clause = (*orig_clauses_)[state];
assert((int)clause >= 0);
state = (*orig_states_)[state];
assert((int)state >= 0);
}
nca_info->push_back(new nca_st_info(clause, state, bv));
}
// Helper function that marks states that we want to see finitely often
@ -179,17 +168,11 @@ namespace spot
unsigned src_scc = si_.scc_of(s);
if (nca_is_inf_state[s])
{
acc_cond::mark_t m = 0u;
for (auto& e : res_->out(s))
{
if (nca_info && e.acc && (si_.scc_of(e.dst) == src_scc
|| state_based_))
m |= e.acc;
e.acc = 0u;
}
e.acc = 0U;
if (nca_info)
save_inf_nca_st(s, m, nca_info);
save_inf_nca_st(s, nca_info);
}
else
{
@ -223,11 +206,15 @@ namespace spot
| scc_info_options::TRACK_SUCCS)),
nb_states_(res_->num_states()),
was_rabin_(was_rabin),
orig_num_st_(orig_num_st)
orig_num_st_(orig_num_st ? orig_num_st : ref_prod->num_states())
{
if (was_rabin)
orig_states_ = ref_prod->get_named_prop<std::vector<unsigned>>
("original-states");
{
orig_states_ = ref_prod->get_named_prop<std::vector<unsigned>>
("original-states");
orig_clauses_ = ref_prod->get_named_prop<std::vector<unsigned>>
("original-clauses");
}
}
~nsa_to_nca_converter()

14
spot/twaalgos/totgba.cc
View file

@ -402,18 +402,22 @@ namespace spot
auto orig_states = new std::vector<unsigned>();
orig_states->resize(res_->num_states(), -1U);
res_->set_named_prop("original-states", orig_states);
auto orig_clauses = new std::vector<unsigned>();
orig_clauses->resize(res_->num_states(), -1U);
res_->set_named_prop("original-clauses", orig_clauses);
unsigned orig_num_states = in_->num_states();
for (unsigned orig = 0; orig < orig_num_states; ++orig)
{
if (!si_.is_useful_scc(si_.scc_of(orig)))
continue;
for (const auto& p : st_repr_[orig])
(*orig_states)[p.second] = orig;
{
(*orig_states)[p.second] = orig;
(*orig_clauses)[p.second] = p.first;
}
}
#if DEBUG
for (unsigned i = 1; i < orig_states->size(); ++i)
assert((int)(*orig_states)[i] >= 0);
#endif
}
set_acc_condition();

4
spot/twaalgos/totgba.hh
View file

@ -114,7 +114,9 @@ namespace spot
/// automaton and the original state of the input automaton. This 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.
/// to retrieve it. Additionally, the correspondence between each created
/// state and the associated DNF clause is recorded in the
/// "original-clauses" property (also a vector of unsigned).
SPOT_API twa_graph_ptr
dnf_to_streett(const const_twa_graph_ptr& aut, bool original_states = false);
}

13
tests/core/dca.test
View file

@ -356,3 +356,16 @@ trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0
4 State: 7 [!0&!1] 3 {2 5} State: 8 [0&!1] 1 {2} [!0&!1] 2 {2} State:
9 [!0&1] 6 {2 4} --END--
EOF
# Maximilien's automaton from issue #317
testeq<<EOF
HOA: v1 States: 11 Start: 0 AP: 2 "b" "c" Acceptance: 4 (Fin(0)|Fin(2))
| Inf(1) | Inf(3) properties: trans-labels explicit-labels trans-acc
complete --BODY-- State: 0 [!0&!1] 1 [!0&!1] 2 [!0&1] 3 [!0&1] 4 [0] 5
State: 1 [!1] 1 {0 2} [!0&!1] 2 [1] 3 [!0&1] 4 State: 2 [!0&!1] 2 {0 3}
[!0&1] 4 [0&1] 7 [0&!1] 10 State: 3 [1] 3 {0 2} [!0] 4 [!1] 9 {0 2} State:
4 [!0&1] 4 {0 3} [!0&!1] 6 {0 3} [0] 7 State: 5 [t] 5 {2} State: 6 [!0&1]
4 {3} [!0&!1] 6 {3} [0] 7 State: 7 [1] 7 {0 2} [!1] 8 {0 2} State: 8
[1] 7 {2} [!1] 8 {2} State: 9 [1] 3 {2} [!0] 4 [!1] 9 {2} State: 10 [1]
7 [!1] 10 {0 2} --END--
EOF