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

use mask_keep_accessible_states

Browse source 
* bin/autfilt.cc, spot/twaalgos/isweakscc.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sccinfo.cc: Use mask_keep_accessible_states instead of
mask_keep_states.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-18 22:39:54 +02:00
parent 4c1147e497
commit 3dc084c4f6
4 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
bin/autfilt.cc
View file

@ -685,7 +685,6 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_keep_states.resize(res + 1, false); opt_keep_states.resize(res + 1, false);
opt_keep_states[res] = true; opt_keep_states[res] = true;
} }
opt_rem_unreach = true;
break; break;
} }
case OPT_MERGE: case OPT_MERGE:
@ -1125,7 +1124,8 @@ namespace
aut = spot::sl2(std::move(aut)); aut = spot::sl2(std::move(aut));
if (!opt_keep_states.empty()) if (!opt_keep_states.empty())
aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial); aut = mask_keep_accessible_states(aut, opt_keep_states,
opt_keep_states_initial);
if (opt_rem_dead) if (opt_rem_dead)
aut->purge_dead_states(); aut->purge_dead_states();
else if (opt_rem_unreach) else if (opt_rem_unreach)

6
spot/twaalgos/isweakscc.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// Developpement de l'Epita (LRDE). // et Developpement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -33,7 +33,7 @@ namespace spot
auto& states = map.states_of(scc); auto& states = map.states_of(scc);
for (auto s: states) for (auto s: states)
keep[s] = true; keep[s] = true;
auto sccaut = mask_keep_states(aut, keep, states.front()); auto sccaut = mask_keep_accessible_states(aut, keep, states.front());
sccaut->set_acceptance(sccaut->acc().num_sets(), sccaut->set_acceptance(sccaut->acc().num_sets(),
sccaut->get_acceptance().complement()); sccaut->get_acceptance().complement());
return !sccaut->is_empty(); return !sccaut->is_empty();

4
spot/twaalgos/remfin.cc
View file

@ -82,10 +82,10 @@ namespace spot
std::vector<bool> keep(aut->num_states(), false); std::vector<bool> keep(aut->num_states(), false);
for (auto s: states) for (auto s: states)
keep[s] = true; keep[s] = true;
auto sccaut = mask_keep_states(aut, keep, states.front()); auto sccaut = mask_keep_accessible_states(aut, keep, states.front());
// Force SBA to false. It does not affect the emptiness // Force SBA to false. It does not affect the emptiness
// check result, however it prevent recurring into this // check result, however it prevent recurring into this
// procedure, because empty() will call to_tgba() wich will // procedure, because empty() will call to_tgba() which will
// call remove_fin()... // call remove_fin()...
sccaut->prop_state_acc(false); sccaut->prop_state_acc(false);
// If SCCAUT is empty, the SCC is BA-type (and none // If SCCAUT is empty, the SCC is BA-type (and none

3
spot/twaalgos/sccinfo.cc
View file

@ -330,7 +330,8 @@ namespace spot
k.resize(aut_->num_states()); k.resize(aut_->num_states());
for (auto i: node.states_) for (auto i: node.states_)
k[i] = true; k[i] = true;
if (mask_keep_states(aut_, k, node.states_.front())->is_empty()) if (mask_keep_accessible_states(aut_, k, node.states_.front())
->is_empty())
node.rejecting_ = true; node.rejecting_ = true;
else else
node.accepting_ = true; node.accepting_ = true;