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

safra: Remove paths when leaving an SCC

Browse source 
* src/tests/safra.cc:  Add option.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh:  When a node leaves an
SCC, all the subpaths of that node are removed.
This commit is contained in:
Alexandre Lewkowicz 2015-09-22 14:06:39 +02:00 • committed by Alexandre Duret-Lutz
parent e8c428d0a3
commit 3bd95c32e7
3 changed files with 30 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/tests/safra.cc
View file

@ -45,6 +45,7 @@ int help()
int main(int argc, char* argv[])
{
bool emit_scc = false;
bool track_scc = false;
bool sim = false;
bool in_hoa = false;
bool in_ltl = false;
@ -80,8 +81,12 @@ int main(int argc, char* argv[])
pretty_print = true;
else if (!strncmp(argv[i], "-b", 2))
sim = true;
else if (!strncmp(argv[i], "--emit_scc", 2))
else if (!strncmp(argv[i], "--emit_scc", 10))
emit_scc = true;
else if (!strncmp(argv[i], "--track_scc", 11))
track_scc = true;
else
std::cerr << "Warning: " << argv[i] << " not used\n";
}
if (!input)
@ -99,7 +104,8 @@ int main(int argc, char* argv[])
spot::translator trans(dict);
trans.set_pref(spot::postprocessor::Deterministic);
auto tmp = trans.run(f);
res = spot::tgba_determinisation(tmp, sim, pretty_print, emit_scc);
res = spot::tgba_determinisation(tmp, sim, pretty_print, emit_scc,
track_scc);
f->destroy();
}
else if (in_hoa)
@ -108,7 +114,8 @@ int main(int argc, char* argv[])
auto aut = spot::parse_aut(input, pel, dict);
if (spot::format_parse_aut_errors(std::cerr, input, pel))
return 2;
res = tgba_determinisation(aut->aut, sim, pretty_print, emit_scc);
res = tgba_determinisation(aut->aut, sim, pretty_print, emit_scc,
track_scc);
}
res->merge_edges();

18
src/twaalgos/safra.cc
View file

@ -24,7 +24,6 @@
#include "safra.hh"
#include "twaalgos/degen.hh"
#include "twaalgos/sccinfo.hh"
#include "twaalgos/simulation.hh"
namespace spot
@ -174,7 +173,9 @@ namespace spot
std::unordered_map<bdd,
std::pair<unsigned, unsigned>,
bdd_hash>& deltas,
succs_t& res) const
succs_t& res,
const scc_info& scc,
bool track_scc) const
{
// Given a bdd returns index of associated safra_state in res
std::map<unsigned, unsigned> bdd2num;
@ -200,6 +201,13 @@ namespace spot
bddnums[j]);
}
safra_state& ss = res[idx].first;
(void) scc;
ss.update_succ(std::vector<node_helper::brace_t>(1, 0), t.dst, t.acc);
// Check if we are leaving the SCC, if so we delete all the
// braces as no cycles can be found with that node
if (track_scc && scc.scc_of(node.first) != scc.scc_of(t.dst))
ss.update_succ({ 0 }, t.dst, t.acc);
else
ss.update_succ(node.second, t.dst, t.acc);
assert(ss.nb_braces_.size() == ss.is_green_.size());
}
@ -364,7 +372,7 @@ namespace spot
unsigned nb_braces = val;
// One brace set
is_green_.assign(nb_braces, true);
// First brace has init_state hence one state inside the first braces.
// Newly created states are the empty mocrstate
nb_braces_.assign(nb_braces, 0);
}
}
@ -394,7 +402,7 @@ namespace spot
twa_graph_ptr
tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation,
bool pretty_print, bool emit_scc)
bool pretty_print, bool emit_scc, bool track_scc)
{
// Degeneralize
twa_graph_ptr aut = spot::degeneralize_tba(a);
@ -468,7 +476,7 @@ namespace spot
safra_state curr = todo.front();
unsigned src_num = seen.find(curr)->second;
todo.pop_front();
curr.compute_succs(aut, bddnums, deltas, succs);
curr.compute_succs(aut, bddnums, deltas, succs, scc, track_scc);
for (auto s: succs)
{
auto i = seen.find(s.first);

8
src/twaalgos/safra.hh
View file

@ -24,6 +24,7 @@
#include "misc/bddlt.hh"
#include "twa/twagraph.hh"
#include "twaalgos/sccinfo.hh"
namespace spot
{
@ -52,7 +53,9 @@ namespace spot
std::unordered_map<bdd,
std::pair<unsigned, unsigned>,
bdd_hash>& deltas,
succs_t& res) const;
succs_t& res,
const scc_info& scc,
bool track_scc = false) const;
// The outermost brace of each node cannot be green
void ungreenify_last_brace();
// Used when creating the list of successors
@ -78,5 +81,6 @@ namespace spot
tgba_determinisation(const const_twa_graph_ptr& aut,
bool bisimulation = false,
bool pretty_print = false,
bool emit_scc = false);
bool emit_scc = false,
bool track_scc = false);
}