merge_states: don't call defrag_states if unnecessary
* spot/twa/twagraph.cc (merge_states): Return the number of removed states, and use that to decide if defrag_states is needed. * spot/twa/twagraph.hh, NEWS: Document that. * tests/core/tgbagraph.test, tests/core/twagraph.cc: Adjust test case.
This commit is contained in:
parent
d019ea61fe
commit
4570c735f3
5 changed files with 40 additions and 12 deletions
2
NEWS
2
NEWS
|
|
@ -228,6 +228,8 @@ New in spot 2.9.7.dev (not yet released)
|
||||||
before attempting to detect mergeable states. When merging states
|
before attempting to detect mergeable states. When merging states
|
||||||
with identical outgoing transitions, it will now also consider
|
with identical outgoing transitions, it will now also consider
|
||||||
self-looping transitions has having identical destinations.
|
self-looping transitions has having identical destinations.
|
||||||
|
Additionally, this function now returns the number of states that
|
||||||
|
have been merged (and therefore removed from the automaton).
|
||||||
|
|
||||||
Python:
|
Python:
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -289,7 +289,7 @@ namespace spot
|
||||||
g_.chain_edges_();
|
g_.chain_edges_();
|
||||||
}
|
}
|
||||||
|
|
||||||
void twa_graph::merge_states()
|
unsigned twa_graph::merge_states()
|
||||||
{
|
{
|
||||||
if (!is_existential())
|
if (!is_existential())
|
||||||
throw std::runtime_error(
|
throw std::runtime_error(
|
||||||
|
|
@ -379,7 +379,10 @@ namespace spot
|
||||||
else
|
else
|
||||||
s = -1U;
|
s = -1U;
|
||||||
|
|
||||||
defrag_states(remap, st);
|
unsigned merged = num_states() - st;
|
||||||
|
if (merged)
|
||||||
|
defrag_states(remap, st);
|
||||||
|
return merged;
|
||||||
}
|
}
|
||||||
|
|
||||||
void twa_graph::purge_unreachable_states(shift_action* f, void* action_data)
|
void twa_graph::purge_unreachable_states(shift_action* f, void* action_data)
|
||||||
|
|
|
||||||
|
|
@ -579,8 +579,19 @@ namespace spot
|
||||||
///
|
///
|
||||||
/// The implementation will sort the edges of the automaton to
|
/// The implementation will sort the edges of the automaton to
|
||||||
/// ease the comparison between two states. This may miss some
|
/// ease the comparison between two states. This may miss some
|
||||||
/// self-loop based in non-deterministic automata.
|
/// self-loop equivalences in non-deterministic automata.
|
||||||
void merge_states();
|
///
|
||||||
|
/// States whose input have been redirected as a consequence of a
|
||||||
|
/// merge are removed from the automaton. This procedure
|
||||||
|
/// therefore renumber states.
|
||||||
|
///
|
||||||
|
/// Merging states might create duplicate transitions in the
|
||||||
|
/// automaton. For instance (1)-a->(2) and (1)-a->(3) will become
|
||||||
|
/// (1)-a->(1) and (1)-a->(1) if (1), (2) and (3) are merged into
|
||||||
|
/// (1).
|
||||||
|
///
|
||||||
|
/// \return the number of states that have been merged and removed.
|
||||||
|
unsigned merge_states();
|
||||||
|
|
||||||
/// \brief Remove all dead states
|
/// \brief Remove all dead states
|
||||||
///
|
///
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
#!/bin/sh
|
#!/bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et
|
# Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et
|
||||||
# Développement de l'Epita (LRDE).
|
# Développement de l'Epita (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
|
|
@ -291,16 +291,20 @@ State: 2
|
||||||
[t] 0&1
|
[t] 0&1
|
||||||
--END--
|
--END--
|
||||||
HOA: v1
|
HOA: v1
|
||||||
States: 1
|
States: 2
|
||||||
Start: 0
|
Start: 1
|
||||||
AP: 0
|
AP: 0
|
||||||
acc-name: all
|
acc-name: all
|
||||||
Acceptance: 0 t
|
Acceptance: 0 t
|
||||||
properties: trans-labels explicit-labels state-acc complete
|
properties: trans-labels explicit-labels state-acc complete
|
||||||
properties: deterministic
|
|
||||||
--BODY--
|
--BODY--
|
||||||
State: 0
|
State: 0
|
||||||
[t] 0
|
[t] 0
|
||||||
|
State: 1
|
||||||
|
[t] 0
|
||||||
|
[t] 0
|
||||||
|
[t] 0
|
||||||
|
[t] 0
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
|
// Copyright (C) 2014-2019, 2021 Laboratoire de Recherche et Développement
|
||||||
// de l'Epita (LRDE).
|
// de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -167,14 +167,22 @@ static void f5()
|
||||||
auto s1 = tg->new_state();
|
auto s1 = tg->new_state();
|
||||||
auto s2 = tg->new_state();
|
auto s2 = tg->new_state();
|
||||||
auto s3 = tg->new_state();
|
auto s3 = tg->new_state();
|
||||||
|
auto s4 = tg->new_state();
|
||||||
|
auto s5 = tg->new_state();
|
||||||
|
|
||||||
tg->set_init_state(s3);
|
tg->set_init_state(s5);
|
||||||
tg->new_edge(s1, s2, bddtrue);
|
tg->new_edge(s1, s2, bddtrue);
|
||||||
tg->new_edge(s2, s2, bddtrue);
|
tg->new_edge(s2, s2, bddtrue);
|
||||||
tg->new_edge(s3, s2, bddtrue);
|
tg->new_edge(s3, s2, bddtrue);
|
||||||
|
tg->new_edge(s4, s4, bddtrue);
|
||||||
|
tg->new_edge(s5, s1, bddtrue);
|
||||||
|
tg->new_edge(s5, s2, bddtrue);
|
||||||
|
tg->new_edge(s5, s3, bddtrue);
|
||||||
|
tg->new_edge(s5, s4, bddtrue);
|
||||||
|
|
||||||
tg->merge_states();
|
unsigned out = tg->merge_states();
|
||||||
|
std::cerr << out << '\n';
|
||||||
|
assert(out == 3);
|
||||||
spot::print_hoa(std::cout, tg) << '\n';
|
spot::print_hoa(std::cout, tg) << '\n';
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue