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

twagraph: fix merge_states() on automata without edges

Browse source 
This corner case was simply causing segfaults.

* tests/python/mergedge.py: Add a test case.
* spot/twa/twagraph.cc (merge_states): Add special handling for
the case where the automaton has no edges.
This commit is contained in:
Alexandre Duret-Lutz 2023-09-20 00:00:15 +02:00
parent 202ab92d1d
commit 858629dd3a
2 changed files with 39 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

23
spot/twa/twagraph.cc
View file

@ -363,6 +363,24 @@ namespace spot
throw std::runtime_error(
"twa_graph::merge_states() does not work on alternating automata");
const unsigned n_states = num_states();
const auto& e_vec = edge_vector();
unsigned n_edges = e_vec.size();
if (n_edges <= 1)
{
if (n_states == 1)
return 0;
// We don't have a very convenient way to resize the state
// vector.
std::vector<unsigned> remap(n_states, -1U);
remap[0] = 0;
get_graph().defrag_states(remap, 1);
SPOT_ASSERT(num_states() == 1);
set_init_state(0);
return n_states - 1;
}
#ifdef ENABLE_PTHREAD
const unsigned nthreads = ppolicy.nthreads();
#else
@ -387,8 +405,6 @@ namespace spot
}, nthreads);
g_.chain_edges_();
const unsigned n_states = num_states();
// Edges are nicely chained and there are no erased edges
// -> We can work with the edge_vector
@ -406,9 +422,6 @@ namespace spot
for (unsigned i = 0; i < n_states; ++i)
hash_of_state.push_back(i);
const auto& e_vec = edge_vector();
unsigned n_edges = e_vec.size();
// For each state we need 4 indices of the edge vector
// [first, first_non_sfirst_selflooplfloop, first_selfloop, end]
// The init value makes sure nothing is done for dead end states

22
tests/python/mergedge.py
View file

@ -1,6 +1,6 @@
#!/usr/bin/python3
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2020-2022 Laboratoire de Recherche et Développement de
# Copyright (C) 2020-2023 Laboratoire de Recherche et Développement de
# l'EPITA.
#
# This file is part of Spot, a model checking library.
@ -56,6 +56,26 @@ aut.merge_edges()
tc.assertEqual(aut.num_edges(), 5)
tc.assertTrue(spot.is_deterministic(aut))
aut = spot.automaton("""
HOA: v1
States: 3
Start: 2
AP: 0
Acceptance: 0 t
--BODY--
State: 0
State: 1
State: 2
--END--""")
tc.assertEqual(aut.num_states(), 3)
tc.assertEqual(aut.num_edges(), 0)
tc.assertEqual(aut.get_init_state_number(), 2)
tc.assertEqual(aut.merge_states(), 2);
tc.assertEqual(aut.num_states(), 1)
tc.assertEqual(aut.num_edges(), 0)
tc.assertEqual(aut.get_init_state_number(), 0)
tc.assertEqual(aut.merge_states(), 0);
for nthread in range(1, 16, 2):
aut = spot.automaton("""
HOA: v1