Commit f88154e5 authored by Alexandre Lewkowicz's avatar Alexandre Lewkowicz Committed by Alexandre Duret-Lutz
Browse files

safra: Add bisimulation optimisation

* src/tests/safra.cc, src/twaalgos/safra.cc,
src/twaalgos/safra.hh, spot/twaalgos/simulation.cc,
spot/twaalgos/simulation.hh: Here.
parent d15b5f43
...@@ -344,10 +344,10 @@ namespace spot ...@@ -344,10 +344,10 @@ namespace spot
} }
// The core loop of the algorithm. // The core loop of the algorithm.
twa_graph_ptr run() twa_graph_ptr run(std::map<int, bdd>* implications = nullptr)
{ {
main_loop(); main_loop();
return build_result(); return build_result(implications);
} }
// Take a state and compute its signature. // Take a state and compute its signature.
...@@ -484,7 +484,7 @@ namespace spot ...@@ -484,7 +484,7 @@ namespace spot
} }
// Build the minimal resulting automaton. // Build the minimal resulting automaton.
twa_graph_ptr build_result() twa_graph_ptr build_result(std::map<int, bdd>* implications = nullptr)
{ {
twa_graph_ptr res = make_twa_graph(a_->get_dict()); twa_graph_ptr res = make_twa_graph(a_->get_dict());
res->copy_ap_of(a_); res->copy_ap_of(a_);
...@@ -503,6 +503,8 @@ namespace spot ...@@ -503,6 +503,8 @@ namespace spot
// its class, or by all the implied classes. // its class, or by all the implied classes.
auto s = gb->new_state(cl.id()); auto s = gb->new_state(cl.id());
gb->alias_state(s, relation_[cl].id()); gb->alias_state(s, relation_[cl].id());
if (implications)
(*implications)[s] = relation_[cl];
} }
// Acceptance of states. Only used if Sba && Cosimulation. // Acceptance of states. Only used if Sba && Cosimulation.
...@@ -631,7 +633,7 @@ namespace spot ...@@ -631,7 +633,7 @@ namespace spot
res->purge_unreachable_states(); res->purge_unreachable_states();
delete gb; delete gb;
res->prop_copy(original_, res->prop_copy(original_,
{ false, // state-based acc forced below { false, // state-based acc forced below
true, // weakness preserved, true, // weakness preserved,
...@@ -735,6 +737,14 @@ namespace spot ...@@ -735,6 +737,14 @@ namespace spot
return simul.run(); return simul.run();
} }
twa_graph_ptr
simulation(const const_twa_graph_ptr& t,
std::map<int, bdd>* implications)
{
direct_simulation<false, false> simul(t);
return simul.run(implications);
}
twa_graph_ptr twa_graph_ptr
simulation_sba(const const_twa_graph_ptr& t) simulation_sba(const const_twa_graph_ptr& t)
{ {
......
...@@ -70,6 +70,9 @@ namespace spot ...@@ -70,6 +70,9 @@ namespace spot
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
simulation(const const_twa_graph_ptr& automaton); simulation(const const_twa_graph_ptr& automaton);
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
simulation(const const_twa_graph_ptr& automaton,
std::map<int, bdd>* implementation);
SPOT_API twa_graph_ptr
simulation_sba(const const_twa_graph_ptr& automaton); simulation_sba(const const_twa_graph_ptr& automaton);
/// @} /// @}
......
...@@ -46,6 +46,7 @@ int help() ...@@ -46,6 +46,7 @@ int help()
int main(int argc, char* argv[]) int main(int argc, char* argv[])
{ {
bool scc_opt = false; bool scc_opt = false;
bool use_bisim = false;
bool sim = false; bool sim = false;
bool in_hoa = false; bool in_hoa = false;
bool in_ltl = false; bool in_ltl = false;
...@@ -83,6 +84,8 @@ int main(int argc, char* argv[]) ...@@ -83,6 +84,8 @@ int main(int argc, char* argv[])
sim = true; sim = true;
else if (!strncmp(argv[i], "--scc_opt", 9)) else if (!strncmp(argv[i], "--scc_opt", 9))
scc_opt = true; scc_opt = true;
else if (!strncmp(argv[i], "--bisim_opt", 10))
use_bisim = true;
else else
{ {
std::cerr << "Warning: " << argv[i] << " not used\n"; std::cerr << "Warning: " << argv[i] << " not used\n";
...@@ -104,14 +107,16 @@ int main(int argc, char* argv[]) ...@@ -104,14 +107,16 @@ int main(int argc, char* argv[])
spot::translator trans(dict); spot::translator trans(dict);
trans.set_pref(spot::postprocessor::Deterministic); trans.set_pref(spot::postprocessor::Deterministic);
auto tmp = trans.run(f); auto tmp = trans.run(f);
res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt); res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt,
use_bisim);
} }
else if (in_hoa) else if (in_hoa)
{ {
auto aut = spot::parse_aut(input, dict); auto aut = spot::parse_aut(input, dict);
if (aut->format_errors(std::cerr)) if (aut->format_errors(std::cerr))
return 2; return 2;
res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt); res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt,
use_bisim);
} }
res->merge_edges(); res->merge_edges();
......
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
#include "safra.hh" #include "safra.hh"
#include "twaalgos/degen.hh" #include "twaalgos/degen.hh"
#include "twaalgos/sccfilter.hh"
#include "twaalgos/simulation.hh" #include "twaalgos/simulation.hh"
namespace spot namespace spot
...@@ -186,7 +187,10 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, ...@@ -186,7 +187,10 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut,
bdd_hash>& deltas, bdd_hash>& deltas,
succs_t& res, succs_t& res,
const scc_info& scc, const scc_info& scc,
bool scc_opt) const const std::map<int, bdd>& implications,
const std::vector<bool>& is_connected,
bool scc_opt,
bool use_bisimulation) const
{ {
// Given a bdd returns index of associated safra_state in res // Given a bdd returns index of associated safra_state in res
std::map<unsigned, unsigned> bdd2num; std::map<unsigned, unsigned> bdd2num;
...@@ -242,11 +246,45 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, ...@@ -242,11 +246,45 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut,
for (auto& s: res) for (auto& s: res)
{ {
safra_state& tmp = s.first; safra_state& tmp = s.first;
if (use_bisimulation)
tmp.merge_redundant_states(implications, scc, is_connected);
tmp.ungreenify_last_brace(); tmp.ungreenify_last_brace();
s.first.color_ = tmp.finalize_construction(); s.first.color_ = tmp.finalize_construction();
} }
} }
void
safra_state::merge_redundant_states(const std::map<int, bdd>& implications,
const scc_info& scc,
const std::vector<bool>& is_connected)
{
std::vector<int> to_remove;
for (auto& n1: nodes_)
{
for (auto& n2: nodes_)
{
if (n1 == n2)
continue;
// index to see if there is a path from scc2 -> scc1
unsigned idx = scc.scc_count() * scc.scc_of(n2.first) +
scc.scc_of(n1.first);
if (bdd_implies(implications.at(n1.first),
implications.at(n2.first)) && !is_connected[idx])
{
to_remove.push_back(n1.first);
}
}
}
for (auto& n: to_remove)
{
for (auto& brace: nodes_[n])
{
--nb_braces_[brace];
}
nodes_.erase(n);
}
}
void safra_state::ungreenify_last_brace() void safra_state::ungreenify_last_brace()
{ {
// Step A4: For a brace to emit green it must surround other braces. // Step A4: For a brace to emit green it must surround other braces.
...@@ -438,17 +476,42 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, ...@@ -438,17 +476,42 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut,
} }
} }
std::vector<bool>
find_scc_paths(const scc_info& scc)
{
unsigned scccount = scc.scc_count();
std::vector<bool> res(scccount * scccount, 0);
for (unsigned i = 0; i < scccount; ++i)
res[i + scccount * i] = 1;
for (unsigned i = 0; i < scccount; ++i)
{
std::stack<unsigned> s;
s.push(i);
while (!s.empty())
{
unsigned src = s.top();
s.pop();
for (auto& d: scc.succ(src))
{
s.push(d);
unsigned idx = scccount * i + d;
res[idx] = 1;
}
}
}
return res;
}
twa_graph_ptr twa_graph_ptr
tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation, tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation,
bool pretty_print, bool scc_opt) bool pretty_print, bool scc_opt, bool use_bisimulation)
{ {
// Degeneralize // Degeneralize
twa_graph_ptr aut = spot::degeneralize_tba(a); twa_graph_ptr aut = spot::scc_filter(spot::degeneralize_tba(a));
std::map<int, bdd> implications;
aut = simulation(aut, &implications);
scc_info scc = scc_info(aut); scc_info scc = scc_info(aut);
// TODO std::vector<bool> is_connected = find_scc_paths(scc);
// if (emit_scc)
// emit_accepting_scc(aut, scc);
bdd allap = bddtrue; bdd allap = bddtrue;
{ {
...@@ -518,7 +581,8 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, ...@@ -518,7 +581,8 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut,
safra_state curr = todo.front(); safra_state curr = todo.front();
unsigned src_num = seen.find(curr)->second; unsigned src_num = seen.find(curr)->second;
todo.pop_front(); todo.pop_front();
curr.compute_succs(aut, bddnums, deltas, succs, scc, scc_opt); curr.compute_succs(aut, bddnums, deltas, succs, scc, implications,
is_connected, scc_opt, use_bisimulation);
for (auto s: succs) for (auto s: succs)
{ {
auto i = seen.find(s.first); auto i = seen.find(s.first);
...@@ -551,6 +615,7 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, ...@@ -551,6 +615,7 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut,
res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets)); res->set_acceptance(sets, acc_cond::acc_code::parity(false, true, sets));
res->prop_deterministic(true); res->prop_deterministic(true);
res->prop_state_acc(false); res->prop_state_acc(false);
if (bisimulation) if (bisimulation)
res = simulation(res); res = simulation(res);
if (pretty_print) if (pretty_print)
......
...@@ -61,12 +61,19 @@ namespace spot ...@@ -61,12 +61,19 @@ namespace spot
bdd_hash>& deltas, bdd_hash>& deltas,
succs_t& res, succs_t& res,
const scc_info& scc, const scc_info& scc,
bool scc_opt = false) const; const std::map<int, bdd>& implications,
const std::vector<bool>& is_connected,
bool scc_opt = false,
bool use_bisimulation = false) const;
// scc_id has to be an accepting SCC. This function tries to find a node // scc_id has to be an accepting SCC. This function tries to find a node
// who lives in that SCC and if it does, we return the brace_id of that SCC. // who lives in that SCC and if it does, we return the brace_id of that SCC.
unsigned find_scc_brace_id(unsigned scc_id, const scc_info& scc); unsigned find_scc_brace_id(unsigned scc_id, const scc_info& scc);
// The outermost brace of each node cannot be green // The outermost brace of each node cannot be green
void ungreenify_last_brace(); void ungreenify_last_brace();
// When a nodes a implies a node b, remove the node a.
void merge_redundant_states(const std::map<int, bdd>& implications,
const scc_info& scc,
const std::vector<bool>& is_connected);
// Used when creating the list of successors // Used when creating the list of successors
// A new intermediate node is created with src's braces and with dst as id // A new intermediate node is created with src's braces and with dst as id
// A merge is done if dst already existed in *this // A merge is done if dst already existed in *this
...@@ -90,5 +97,6 @@ namespace spot ...@@ -90,5 +97,6 @@ namespace spot
tgba_determinisation(const const_twa_graph_ptr& aut, tgba_determinisation(const const_twa_graph_ptr& aut,
bool bisimulation = false, bool bisimulation = false,
bool pretty_print = false, bool pretty_print = false,
bool scc_opt = false); bool scc_opt = false,
bool use_bisimulation = false);
} }
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