From d7ab8dbe134724702cd05648a30db8034860d7e5 Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Wed, 15 Apr 2020 21:51:41 +0200 Subject: [PATCH] to_parity: Correct error with automata without transition * spot/twaalgos/toparity.cc: Check that an automaton is not just a useless SCC. --- spot/twaalgos/toparity.cc | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 8854e6887..49c9d7fcb 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -1655,8 +1655,25 @@ run() } } unsigned initial_state = aut_->get_init_state_number(); - auto initial_car = state2car.find(initial_state); - auto initial_state_res = car2num.find(initial_car->second); + auto initial_car_ptr = state2car.find(initial_state); + car_state initial_car; + // If we take an automaton with one state and without transition, + // the SCC was useless so state2car doesn't have initial_state + if (initial_car_ptr == state2car.end()) + { + assert(res_->num_states() == 0); + auto new_state = res_->new_state(); + car_state new_car = {initial_state, 0, perm_t()}; + state2car[initial_state] = new_car; + if (options.pretty_print) + names->push_back(new_car.to_string(None)); + num2car.insert(num2car.begin() + new_state, new_car); + car2num[new_car] = new_state; + initial_car = new_car; + } + else + initial_car = initial_car_ptr->second; + auto initial_state_res = car2num.find(initial_car); if (initial_state_res != car2num.end()) res_->set_init_state(initial_state_res->second); else