Commit fa8dd7f1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Have scc_map keep track of APs that are reachable from a SCC.

* src/tgbaalgos/scc.hh (scc_map::scc): Add a supp_rec member to
hold reachable APs.
* src/tgbaalgos/scc.cc (scc_map::update_supp_rec): New function,
to update supp_rec.
(scc_map::build_map): Call it.
(scc_map::aprec_set_of): New function.
(dump_scc_dot): Show the output of aprec_set_of().
parent b3486965
2009-09-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Have scc_map keep track of APs that are reachable from a SCC.
* src/tgbaalgos/scc.hh (scc_map::scc): Add a supp_rec member to
hold reachable APs.
* src/tgbaalgos/scc.cc (scc_map::update_supp_rec): New function,
to update supp_rec.
(scc_map::build_map): Call it.
(scc_map::aprec_set_of): New function.
(dump_scc_dot): Show the output of aprec_set_of().
2009-09-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Have scc_map keep track of APs that are occurring in a SCC.
......
......@@ -104,6 +104,28 @@ namespace spot
return n;
}
// recursively update supp rec
bdd
scc_map::update_supp_rec(unsigned state)
{
assert(scc_map_.size() > state);
bdd& res = scc_map_[state].supp_rec;
if (res == bddtrue)
{
const succ_type& s = succ(state);
succ_type::const_iterator it;
for (it = s.begin(); it != s.end(); ++it)
res &= update_supp_rec(it->first);
res &= scc_map_[state].supp;
}
return res;
}
void
scc_map::build_map()
{
......@@ -266,6 +288,9 @@ namespace spot
root_.front().conds.insert(conds.begin(), conds.end());
root_.front().supp &= supp;
}
// recursively update supp_rec
(void) update_supp_rec(initial());
}
unsigned scc_map::scc_of_state(const state* s) const
......@@ -288,6 +313,13 @@ namespace spot
}
bdd scc_map::aprec_set_of(unsigned n) const
{
assert(scc_map_.size() > n);
return scc_map_[n].supp_rec;
}
bdd scc_map::acc_set_of(unsigned n) const
{
assert(scc_map_.size() > n);
......@@ -433,9 +465,12 @@ namespace spot
ostr << ", ";
bdd_print_formula(ostr, m.get_aut()->get_dict(), *i);
}
ostr << "]\\n APs=[";
ostr << "]\\n AP=[";
bdd_print_sat(ostr, m.get_aut()->get_dict(),
m.ap_set_of(state));
ostr << "]\\n APrec=[";
bdd_print_sat(ostr, m.get_aut()->get_dict(),
m.ap_set_of(state)) << "]";
m.aprec_set_of(state)) << "]";
}
std::cout << " " << state << " [shape=box,"
......
......@@ -113,6 +113,14 @@ namespace spot
/// \pre This should only be called once build_map() has run.
bdd ap_set_of(unsigned n) const;
/// \brief Return the set of atomic properties reachable from this SCC.
///
/// \return a BDD that is a conjuction of all atomic properties
/// occurring on the transitions reachable from this SCC n.
///
/// \pre This should only be called once build_map() has run.
bdd aprec_set_of(unsigned n) const;
/// \brief Return the set of acceptance conditions occurring in an SCC.
///
/// \pre This should only be called once build_map() has run.
......@@ -135,13 +143,14 @@ namespace spot
unsigned self_loops() const;
protected:
bdd update_supp_rec(unsigned state);
int relabel_component();
struct scc
{
public:
scc(int index) : index(index), acc(bddfalse), supp(bddtrue) {};
scc(int index) : index(index), acc(bddfalse),
supp(bddtrue), supp_rec(bddtrue) {};
/// Index of the SCC.
int index;
/// The union of all acceptance conditions of transitions which
......@@ -153,6 +162,8 @@ namespace spot
cond_set conds;
/// Conjunction of atomic propositions used in the SCC.
bdd supp;
/// Conjunction of atomic propositions used in the SCC.
bdd supp_rec;
/// Successor SCC.
succ_type succ;
};
......@@ -186,7 +197,7 @@ namespace spot
// SCC number "n" in H_ corresponds to entry
// "n" in SCC_MAP_.
unsigned self_loops_; // Self loops count.
};
};
scc_stats build_scc_stats(const tgba* a);
scc_stats build_scc_stats(const scc_map& m);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment