diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index 5355c3cc3..5c4d006c1 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -102,33 +102,13 @@ namespace spot ++it_trans; } - if (transitions_to_livelock_states) - { - state_ta_explicit::transitions::iterator it_trans; - - for (it_trans = transitions_to_livelock_states->begin(); - it_trans != transitions_to_livelock_states->end(); - ++it_trans) - { - if (artificial_livelock_acc_state) - { - testing_automata->create_transition - (source, - (*it_trans)->condition, - (*it_trans)->acceptance_conditions, - artificial_livelock_acc_state, true); - } - else - { - testing_automata->create_transition - (source, - (*it_trans)->condition, - (*it_trans)->acceptance_conditions, - ((*it_trans)->dest)->stuttering_reachable_livelock, - true); - } - } - } + for (auto* trans: *transitions_to_livelock_states) + testing_automata->create_transition + (source, trans->condition, + trans->acceptance_conditions, + artificial_livelock_acc_state ? + artificial_livelock_acc_state : + trans->dest->stuttering_reachable_livelock, true); } delete transitions_to_livelock_states; diff --git a/spot/twaalgos/are_isomorphic.cc b/spot/twaalgos/are_isomorphic.cc index 44b220c0d..127b5c6fa 100644 --- a/spot/twaalgos/are_isomorphic.cc +++ b/spot/twaalgos/are_isomorphic.cc @@ -30,19 +30,19 @@ namespace { typedef spot::twa_graph::graph_t::edge_storage_t tr_t; - bool + static bool tr_t_less_than(const tr_t& t1, const tr_t& t2) { return t1.cond.id() < t2.cond.id(); } - bool + static bool operator!=(const tr_t& t1, const tr_t& t2) { return t1.cond.id() != t2.cond.id(); } - bool + static bool are_isomorphic_det(const spot::const_twa_graph_ptr aut1, const spot::const_twa_graph_ptr aut2) { @@ -135,14 +135,12 @@ namespace spot trival autdet = aut->prop_deterministic(); if (ref_deterministic_) { - if (autdet || (!autdet && spot::is_deterministic(aut))) - return are_isomorphic_det(ref_, aut); - } - else - { - if (autdet || nondet_states_ != spot::count_nondet_states(aut)) + if (!spot::is_deterministic(aut)) return false; + return are_isomorphic_det(ref_, aut); } + if (autdet || nondet_states_ != spot::count_nondet_states(aut)) + return false; auto tmp = make_twa_graph(aut, twa::prop_set::all()); spot::canonicalize(tmp); diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 97318e200..5e779db1e 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -1781,15 +1781,11 @@ namespace spot } // Apply the fair-loop approximation if requested. - if (fair_loop_approx_) - { + if (fair_loop_approx_ // If the source cannot possibly be part of a fair // loop, make all possible promises. - if (fair_loop_approx_ - && f != formula::tt() - && !pflc_.check(f)) - t.symbolic &= all_promises_; - } + && !f.is_tt() && !pflc_.check(f)) + t.symbolic &= all_promises_; // Register the reverse mapping if it is not already done. if (b2f_.find(t.symbolic) == b2f_.end())