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

toparity: false transitions are not a problem anymore

Browse source 
* spot/twaalgos/toparity.cc: Do not remove false transitions.
* tests/python/toparity.py: Add a test case with false transitions.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-16 10:54:10 +02:00
parent 1e86463205
commit 875846f51f
2 changed files with 21 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

23
spot/twaalgos/toparity.cc
View file

@ -1703,34 +1703,13 @@ to_parity_options options;
std::vector<std::string>* names; std::vector<std::string>* names;
}; // car_generator }; // car_generator
static const_twa_graph_ptr
remove_false_transitions(const const_twa_graph_ptr& a)
{
// Do not do anything if the automaton has no false transition
for (auto edge : a->edges())
if (edge.cond == bddfalse)
goto doremoval;
return a;
doremoval:
auto res_ = make_twa_graph(a->get_dict());
res_->copy_ap_of(a);
res_->new_states(a->num_states());
for (auto edge : a->edges())
if (edge.cond != bddfalse)
res_->new_edge(edge.src, edge.dst, edge.cond, edge.acc);
res_->set_init_state(a->get_init_state_number());
res_->set_acceptance(a->get_acceptance());
res_->prop_copy(a, twa::prop_set::all());
return res_;
}
}// namespace }// namespace
twa_graph_ptr twa_graph_ptr
to_parity(const const_twa_graph_ptr &aut, const to_parity_options options) to_parity(const const_twa_graph_ptr &aut, const to_parity_options options)
{ {
return car_generator(remove_false_transitions(aut), options).run(); return car_generator(aut, options).run();
} }
// Old version of CAR. // Old version of CAR.

24
tests/python/toparity.py
View file

@ -19,7 +19,8 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>. # along with this program. If not, see <http://www.gnu.org/licenses/>.
import spot import spot
import itertools from itertools import zip_longest
from buddy import bddfalse
# Tests for the new version of to_parity # Tests for the new version of to_parity
@ -91,8 +92,7 @@ options = [
def test(aut, expected_num_states=[], full=True): def test(aut, expected_num_states=[], full=True):
for (opt, expected_num) in\ for (opt, expected_num) in zip_longest(options, expected_num_states):
itertools.zip_longest(options, expected_num_states):
p1 = spot.to_parity(aut, p1 = spot.to_parity(aut,
search_ex = opt.search_ex, search_ex = opt.search_ex,
use_last = opt.use_last, use_last = opt.use_last,
@ -107,8 +107,8 @@ def test(aut, expected_num_states=[], full=True):
pretty_print = opt.pretty_print, pretty_print = opt.pretty_print,
) )
assert spot.are_equivalent(aut, p1) assert spot.are_equivalent(aut, p1)
if (expected_num != None): if expected_num is not None:
assert(p1.num_states() == expected_num) assert p1.num_states() == expected_num
if full: if full:
# Make sure passing opt is the same as setting # Make sure passing opt is the same as setting
# each argument individually # each argument individually
@ -343,6 +343,20 @@ assert p.num_states() == 22
assert spot.are_equivalent(a, p) assert spot.are_equivalent(a, p)
test(a, [8, 7, 8, 8, 6, 7, 6]) test(a, [8, 7, 8, 8, 6, 7, 6])
# Force a few edges to false, to make sure to_parity() is OK with that.
for e in a.out(2):
if e.dst == 1:
e.cond = bddfalse
break
for e in a.out(3):
if e.dst == 3:
e.cond = bddfalse
break
p = spot.to_parity_old(a, True)
assert p.num_states() == 22
assert spot.are_equivalent(a, p)
test(a, [7, 6, 7, 7, 6, 6, 6])
for f in spot.randltl(4, 400): for f in spot.randltl(4, 400):
d = spot.translate(f, "det", "G") d = spot.translate(f, "det", "G")
p = spot.to_parity_old(d, True) p = spot.to_parity_old(d, True)