twa_graph: add a method to merge states with same outgoing edges
* spot/twa/twagraph.hh, spot/twa/twagraph.cc: here * NEWS: document it * tests/core/twagraph.cc, tests/core/tgbagraph.test: test it
This commit is contained in:
parent
5b9088006c
commit
5a819e0c93
5 changed files with 89 additions and 1 deletions
5
NEWS
5
NEWS
|
|
@ -24,6 +24,11 @@ New in spot 2.5.3.dev (not yet released)
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
||||||
|
- spot::twa_graph::merge_states() is a new method that merges states
|
||||||
|
with the exact same outgoing edges. As it performs no reordering of
|
||||||
|
the edges, it is better to call it when you know that the edges in
|
||||||
|
the twa_graph are sorted (e.g. after a call to merge_edges()).
|
||||||
|
|
||||||
- You can now specify to Spot the number of acceptance marks you
|
- You can now specify to Spot the number of acceptance marks you
|
||||||
wish to use. This is a compile-time option, accessible through
|
wish to use. This is a compile-time option, accessible through
|
||||||
option --enable-max-accsets of the configure script. The default
|
option --enable-max-accsets of the configure script. The default
|
||||||
|
|
|
||||||
|
|
@ -231,6 +231,48 @@ namespace spot
|
||||||
g_.chain_edges_();
|
g_.chain_edges_();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void twa_graph::merge_states()
|
||||||
|
{
|
||||||
|
if (!is_existential())
|
||||||
|
throw std::runtime_error(
|
||||||
|
"twa_graph::merge_states() does not work on alternating automata");
|
||||||
|
|
||||||
|
const unsigned nb_states = num_states();
|
||||||
|
std::vector<unsigned> remap(nb_states, -1U);
|
||||||
|
for (unsigned i = 0; i != nb_states; ++i)
|
||||||
|
{
|
||||||
|
auto out1 = out(i);
|
||||||
|
for (unsigned j = 0; j != i; ++j)
|
||||||
|
{
|
||||||
|
auto out2 = out(j);
|
||||||
|
if (std::equal(out1.begin(), out1.end(), out2.begin(), out2.end(),
|
||||||
|
[](const edge_storage_t& a,
|
||||||
|
const edge_storage_t& b)
|
||||||
|
{ return a.dst == b.dst && a.data() == b.data(); }))
|
||||||
|
{
|
||||||
|
remap[i] = j;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
for (auto& e: edges())
|
||||||
|
if (remap[e.dst] != -1U)
|
||||||
|
e.dst = remap[e.dst];
|
||||||
|
|
||||||
|
if (remap[get_init_state_number()] != -1U)
|
||||||
|
set_init_state(remap[get_init_state_number()]);
|
||||||
|
|
||||||
|
unsigned st = 0;
|
||||||
|
for (auto& s: remap)
|
||||||
|
if (s == -1U)
|
||||||
|
s = st++;
|
||||||
|
else
|
||||||
|
s = -1U;
|
||||||
|
|
||||||
|
defrag_states(std::move(remap), st);
|
||||||
|
}
|
||||||
|
|
||||||
void twa_graph::purge_unreachable_states(shift_action* f, void* action_data)
|
void twa_graph::purge_unreachable_states(shift_action* f, void* action_data)
|
||||||
{
|
{
|
||||||
unsigned num_states = g_.num_states();
|
unsigned num_states = g_.num_states();
|
||||||
|
|
|
||||||
|
|
@ -553,6 +553,14 @@ namespace spot
|
||||||
/// This is already called by merge_edges().
|
/// This is already called by merge_edges().
|
||||||
void merge_univ_dests();
|
void merge_univ_dests();
|
||||||
|
|
||||||
|
/// \brief Merge states that can be merged.
|
||||||
|
///
|
||||||
|
/// This merges states that have the exact same outgoing edges. This method
|
||||||
|
/// compares the successors of states in the order in which they are stored.
|
||||||
|
/// Therefore, it is better to call it when you know that the edges are
|
||||||
|
/// stored, e.g. after a call to merge_edges().
|
||||||
|
void merge_states();
|
||||||
|
|
||||||
/// \brief Remove all dead states
|
/// \brief Remove all dead states
|
||||||
///
|
///
|
||||||
/// Dead states are all the states that cannot be part of
|
/// Dead states are all the states that cannot be part of
|
||||||
|
|
|
||||||
|
|
@ -30,7 +30,7 @@
|
||||||
|
|
||||||
set -e
|
set -e
|
||||||
|
|
||||||
run 0 ../tgbagraph | tee stdout
|
run 0 ../tgbagraph > stdout
|
||||||
|
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
p1
|
p1
|
||||||
|
|
@ -289,6 +289,18 @@ State: 1
|
||||||
State: 2
|
State: 2
|
||||||
[t] 0&1
|
[t] 0&1
|
||||||
--END--
|
--END--
|
||||||
|
HOA: v1
|
||||||
|
States: 1
|
||||||
|
Start: 0
|
||||||
|
AP: 0
|
||||||
|
acc-name: all
|
||||||
|
Acceptance: 0 t
|
||||||
|
properties: trans-labels explicit-labels state-acc complete
|
||||||
|
properties: deterministic
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[t] 0
|
||||||
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
diff stdout expected
|
diff stdout expected
|
||||||
|
|
|
||||||
|
|
@ -158,10 +158,31 @@ static void f4()
|
||||||
spot::print_hoa(std::cout, tg, "1.1") << '\n';
|
spot::print_hoa(std::cout, tg, "1.1") << '\n';
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Test merge_states()
|
||||||
|
static void f5()
|
||||||
|
{
|
||||||
|
auto d = spot::make_bdd_dict();
|
||||||
|
auto tg = make_twa_graph(d);
|
||||||
|
|
||||||
|
auto s1 = tg->new_state();
|
||||||
|
auto s2 = tg->new_state();
|
||||||
|
auto s3 = tg->new_state();
|
||||||
|
|
||||||
|
tg->set_init_state(s3);
|
||||||
|
tg->new_edge(s1, s2, bddtrue);
|
||||||
|
tg->new_edge(s2, s2, bddtrue);
|
||||||
|
tg->new_edge(s3, s2, bddtrue);
|
||||||
|
|
||||||
|
tg->merge_states();
|
||||||
|
|
||||||
|
spot::print_hoa(std::cout, tg) << '\n';
|
||||||
|
}
|
||||||
|
|
||||||
int main()
|
int main()
|
||||||
{
|
{
|
||||||
f1();
|
f1();
|
||||||
f2();
|
f2();
|
||||||
f3();
|
f3();
|
||||||
f4();
|
f4();
|
||||||
|
f5();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue