Commit edf278c3 authored by Florian Renkin's avatar Florian Renkin
Browse files

minimize_mealy_fast: correct inclusion + tests

parent 7e615a41
Pipeline #28725 failed with stage
in 159 minutes and 11 seconds
......@@ -967,6 +967,22 @@ namespace
bdd_digraph(bdd label, unsigned state) : label_(label), state_(state) {}
void
all_children_aux_(std::set<std::shared_ptr<bdd_digraph>>& res)
{
for (auto c : children_)
if (res.insert(c).second)
c->all_children_aux_(res);
}
std::set<std::shared_ptr<bdd_digraph>>
all_children()
{
std::set<std::shared_ptr<bdd_digraph>> res;
all_children_aux_(res);
return res;
}
void
add_aux_(std::shared_ptr<bdd_digraph>& new_node, std::vector<bool>& done)
{
......@@ -977,17 +993,22 @@ namespace
{
if (done[ch->state_])
continue;
if (bdd_implies(ch->label_, new_node->label_))
{
if (bdd_implies(new_node->label_, ch->label_))
ch->add_aux_(new_node, done);
else if (bdd_implies(ch->label_, new_node->label_))
{
auto ch_nodes = ch->all_children();
new_node->children_.push_back(ch);
for (auto& x : ch_nodes)
new_node->children_.push_back(x);
}
}
if (bdd_implies(new_node->label_, label_))
children_.push_back(new_node);
assert(bdd_implies(new_node->label_, label_));
children_.push_back(new_node);
}
void add(std::shared_ptr<bdd_digraph>& new_node, bool rec,
void
add(std::shared_ptr<bdd_digraph>& new_node, bool rec,
unsigned max_state)
{
if (new_node->label_ == bddtrue)
......@@ -1002,9 +1023,7 @@ namespace
add_aux_(new_node, done);
}
else
{
children_.push_back(new_node);
}
}
unsigned
......@@ -1015,21 +1034,11 @@ namespace
res.insert({label_, state_});
return state_;
}
unsigned nb_p = children_[0].use_count();
unsigned pos = 0;
for (unsigned i = 1; i < children_.size(); ++i)
{
unsigned nb_p_ch = children_[1].use_count();
if (nb_p_ch > nb_p)
{
nb_p = nb_p_ch;
pos = i;
}
}
auto ch_size = children_.size();
unsigned pos = ch_size - 1;
auto my_repr = children_[pos]->flatten_aux(res);
res.insert({label_, my_repr});
for (unsigned i = 0; i < children_.size(); ++i)
for (unsigned i = 0; i < ch_size; ++i)
{
if (i == pos)
continue;
......@@ -1045,6 +1054,23 @@ namespace
flatten_aux(res);
return res;
}
// Transforms children_ such that the child with the higher use_count() is
// at the end.
void
sort_nodes()
{
if (!children_.empty())
{
auto max_pos = std::max_element(children_.begin(), children_.end(),
[](const std::shared_ptr<bdd_digraph>& n1,
const std::shared_ptr<bdd_digraph>& n2)
{
return n1.use_count() < n2.use_count();
});
std::iter_swap(max_pos, children_.end() - 1);
}
}
};
......@@ -1063,7 +1089,7 @@ namespace
std::vector<bdd> signatures(a_num_states);
sig_calculator red(a, rec);
red.main_loop();
if (red.bdd_lstate_.size() == a_num_states)
if (!rec && red.bdd_lstate_.size() == a_num_states)
{
repr[0] = -1U;
return repr;
......@@ -1088,13 +1114,25 @@ namespace
}
}
}
graph.sort_nodes();
auto repr_map = graph.flatten();
bool is_useless_map = true;
for (unsigned i = 0; i < a_num_states; ++i)
{
if (owner_ptr && (*owner_ptr)[i] == 0)
repr[i] = i;
else
{
repr[i] = repr_map[signatures[i]];
is_useless_map &= (repr[i] == i);
}
}
if (is_useless_map)
{
repr[0] = -1U;
return repr;
}
// We have a new destination for the edges that leave the states controlled
// by the environment but we have to change the initial state.
......
......@@ -411,6 +411,7 @@ TESTS_python = \
python/merge.py \
python/mergedge.py \
python/minato.py \
python/minimize.py \
python/misc-ec.py \
python/optionmap.py \
python/origstate.py \
......
import spot
spot.setup()
# Syntcomp: Alarm_2d1010f8.tlsf
aut = spot.automaton("""HOA: v1
States: 17
Start: 0
AP: 6 "u02alarm29control02alarm29control"
"u02alarm29control0f1d2alarm29turn2off1b"
"u02alarm29control0f1d2alarm29turn2on1b" "p0p0off02alarm29intent"
"p0p0on02alarm29intent" "p0b02alarm29alarm"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4
| 0&!1&!2&3&4] 1
[!0&!1&2&!3&4&!5 | !0&!1&2&3&!4&5] 2
[!0&!1&2&!3&4&5 | !0&!1&2&3&!4&!5] 3
State: 1
[!0&!1&2 | !0&1&!2 | 0&!1&!2] 1
State: 2
[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4
| 0&!1&!2&3&4] 4
[!0&!1&2&!3&4&!5] 5
[!0&!1&2&3&!4&!5] 6
[!0&!1&2&!3&4&5] 7
[!0&1&!2&3&!4&5] 8
State: 3
[!0&!1&2&3&!4&5] 2
[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4
| 0&!1&!2&3&4] 4
[!0&!1&2&!3&4&!5] 5
[!0&!1&2&3&!4&!5] 6
[!0&!1&2&!3&4&5] 7
State: 4
[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&!1&2&!4&5 | !0&1&!2&!3&!4 | !0&1&!2&3&4
| !0&1&!2&!4&5 | 0&!1&!2&!3&!4 | 0&!1&!2&3&4 | 0&!1&!2&!4&5] 4
[!0&!1&2&!3&4 | !0&1&!2&!3&4 | 0&!1&!2&!3&4] 9
[!0&!1&2&3&!4&!5 | !0&1&!2&3&!4&!5 | 0&!1&!2&3&!4&!5] 10
State: 5
[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4
[!0&!1&2&!3&4] 5
[!0&!1&2&3&4 | !0&1&!2&3&4 | 0&!1&!2&3&4] 9
[!0&!1&2&3&!4] 11
State: 6
[!0&!1&2&!3&!4 | !0&!1&2&3&4&5 | !0&1&!2&!3&!4 | !0&1&!2&3&4&5 | 0&!1&!2&!3&!4
| 0&!1&!2&3&4&5] 4
[!0&!1&2&!3&4] 5
[!0&!1&2&3&!4&!5] 6
[!0&!1&2&3&!4&5] 11
[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 10
State: 7
[!0&!1&2&3&!4&5] 2
[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4
[!0&!1&2&!3&4&!5] 5
[!0&!1&2&!3&4&5] 7
[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 9
[!0&!1&2&3&!4&!5] 11
[!0&!1&2&3&4&5 | !0&1&!2&3&4&5 | 0&!1&!2&3&4&5] 12
State: 8
[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4
| 0&!1&!2&3&4] 4
[!0&!1&2&3&!4&5] 11
[!0&!1&2&!3&4&5] 13
[!0&!1&2&!3&4&!5] 14
[!0&1&!2&3&!4&!5] 15
State: 9
[!0&!1&2&!4 | !0&1&!2&!4 | 0&!1&!2&!4] 4
[!0&!1&2&4 | !0&1&!2&4 | 0&!1&!2&4] 9
State: 10
[!0&!1&2&!3&!4 | !0&!1&2&3&5 | !0&1&!2&!3&!4 | !0&1&!2&3&5 | 0&!1&!2&!3&!4
| 0&!1&!2&3&5] 4
[!0&!1&2&!3&4 | !0&1&!2&!3&4 | 0&!1&!2&!3&4] 9
[!0&!1&2&3&!5 | !0&1&!2&3&!5 | 0&!1&!2&3&!5] 10
State: 11
[!0&!1&2&!3&!4 | !0&!1&2&3&4 | !0&1&!2&!3&!4 | !0&1&!2&3&4 | 0&!1&!2&!3&!4
| 0&!1&!2&3&4] 4
[!0&!1&2&!3&4] 5
[!0&!1&2&3&!4&!5] 6
[!0&!1&2&3&!4&5] 11
State: 12
[!0&!1&2&!4 | !0&1&!2&!4 | 0&!1&!2&!4] 4
[!0&!1&2&4&!5 | !0&1&!2&4&!5 | 0&!1&!2&4&!5] 9
[!0&!1&2&4&5 | !0&1&!2&4&5 | 0&!1&!2&4&5] 12
State: 13
[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4
[!0&!1&2&!3&4&!5] 5
[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 9
[!0&!1&2&3&!4] 11
[!0&!1&2&3&4&5 | !0&1&!2&3&4&5 | 0&!1&!2&3&4&5] 12
[!0&!1&2&!3&4&5] 13
State: 14
[!0&!1&2&3&!4&5] 2
[!0&!1&2&!3&!4 | !0&1&!2&!3&!4 | 0&!1&!2&!3&!4] 4
[!0&!1&2&!3&4&!5] 5
[!0&!1&2&!3&4&5] 7
[!0&!1&2&3&4 | !0&1&!2&3&4 | 0&!1&!2&3&4] 9
[!0&!1&2&3&!4&!5] 11
State: 15
[!0&!1&2&!3&!4 | !0&!1&2&3&4&5 | !0&1&!2&!3&!4 | !0&1&!2&3&4&5 | 0&!1&!2&!3&!4
| 0&!1&!2&3&4&5] 4
[!0&!1&2&!3&4&5] 5
[!0&!1&2&3&!4&5] 11
[!0&!1&2&!3&4&!5] 14
[!0&1&!2&3&!4&!5] 15
[!0&!1&2&3&4&!5 | !0&1&!2&3&4&!5 | 0&!1&!2&3&4&!5] 16
State: 16
[!0&!1&2&!3&!4 | !0&!1&2&3&5 | !0&1&!2&!3&!4 | !0&1&!2&3&5 | 0&!1&!2&!3&!4
| 0&!1&!2&3&5] 4
[!0&!1&2&!3&4 | !0&1&!2&!3&4 | 0&!1&!2&!3&4] 9
[!0&!1&2&3&!5 | !0&1&!2&3&!5 | 0&!1&!2&3&!5] 16
--END--""")
# Build an equivalent deterministic monitor
min_equiv = spot.minimize_mealy_fast(aut, False)
assert min_equiv.num_states() == 6
assert spot.are_equivalent(min_equiv, aut)
# Build an automaton that recognizes a subset of the language of the original
# automaton
min_sub = spot.minimize_mealy_fast(aut, True)
assert min_sub.num_states() == 5
prod = spot.product(spot.complement(aut), min_sub)
assert spot.generic_emptiness_check(prod)
aut = spot.automaton("""
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0&!1] 1
[!0&1] 2
[0] 3
State: 1
[0] 1
State: 2
[1] 2
State: 3
[0&1] 3
--END--
""")
exp = """HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0&1] 0
--END--"""
# An example that shows that we should not build a tree when we use inclusion.
res = spot.minimize_mealy_fast(aut, True)
assert res.to_str() == exp
aut = spot.automaton("""
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[!0&!1] 1
[!0&1] 2
[0&!1] 3
State: 1
[0] 1
State: 2
[1] 2
State: 3
[0&1] 3
--END--
""")
exp = """HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0&!1] 1
[!0&1] 1
[0&!1] 1
State: 1
[0&1] 1
--END--"""
res = spot.minimize_mealy_fast(aut, True)
assert res.to_str() == exp
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