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

improve some conditions, as hinted by PVS-Studio

Browse source 
For #192.

* spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/are_isomorphic.cc,
spot/taalgos/tgba2ta.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-28 22:59:12 +02:00
parent 40b8bab890
commit 835b5ee1cf
3 changed files with 17 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

34
spot/taalgos/tgba2ta.cc
View file

@ -102,33 +102,13 @@ namespace spot
++it_trans; ++it_trans;
} }
if (transitions_to_livelock_states) for (auto* trans: *transitions_to_livelock_states)
{ testing_automata->create_transition
state_ta_explicit::transitions::iterator it_trans; (source, trans->condition,
trans->acceptance_conditions,
for (it_trans = transitions_to_livelock_states->begin(); artificial_livelock_acc_state ?
it_trans != transitions_to_livelock_states->end(); artificial_livelock_acc_state :
++it_trans) trans->dest->stuttering_reachable_livelock, true);
{
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);
}
}
}
} }
delete transitions_to_livelock_states; delete transitions_to_livelock_states;

16
spot/twaalgos/are_isomorphic.cc
View file

@ -30,19 +30,19 @@
namespace namespace
{ {
typedef spot::twa_graph::graph_t::edge_storage_t tr_t; 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) tr_t_less_than(const tr_t& t1, const tr_t& t2)
{ {
return t1.cond.id() < t2.cond.id(); return t1.cond.id() < t2.cond.id();
} }
bool static bool
operator!=(const tr_t& t1, const tr_t& t2) operator!=(const tr_t& t1, const tr_t& t2)
{ {
return t1.cond.id() != t2.cond.id(); return t1.cond.id() != t2.cond.id();
} }
bool static bool
are_isomorphic_det(const spot::const_twa_graph_ptr aut1, are_isomorphic_det(const spot::const_twa_graph_ptr aut1,
const spot::const_twa_graph_ptr aut2) const spot::const_twa_graph_ptr aut2)
{ {
@ -135,14 +135,12 @@ namespace spot
trival autdet = aut->prop_deterministic(); trival autdet = aut->prop_deterministic();
if (ref_deterministic_) if (ref_deterministic_)
{ {
if (autdet || (!autdet && spot::is_deterministic(aut))) if (!spot::is_deterministic(aut))
return are_isomorphic_det(ref_, aut);
}
else
{
if (autdet || nondet_states_ != spot::count_nondet_states(aut))
return false; 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()); auto tmp = make_twa_graph(aut, twa::prop_set::all());
spot::canonicalize(tmp); spot::canonicalize(tmp);

10
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -1781,15 +1781,11 @@ namespace spot
} }
// Apply the fair-loop approximation if requested. // 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 // If the source cannot possibly be part of a fair
// loop, make all possible promises. // loop, make all possible promises.
if (fair_loop_approx_ && !f.is_tt() && !pflc_.check(f))
&& f != formula::tt() t.symbolic &= all_promises_;
&& !pflc_.check(f))
t.symbolic &= all_promises_;
}
// Register the reverse mapping if it is not already done. // Register the reverse mapping if it is not already done.
if (b2f_.find(t.symbolic) == b2f_.end()) if (b2f_.find(t.symbolic) == b2f_.end())