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

simulation: take a tgba_digraph as input

Browse source 
Issue #45.

* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Take
a tgba_digraph is input.
* src/tgbatest/ltl2tgba.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-19 18:07:59 +01:00
parent 0159027395
commit 64469f3dbd
3 changed files with 78 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

130
src/tgbaalgos/simulation.cc
View file

@ -28,7 +28,6 @@
#include "tgbaalgos/reachiter.hh" #include "tgbaalgos/reachiter.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/sccinfo.hh" #include "tgbaalgos/sccinfo.hh"
#include "tgbaalgos/dupexp.hh"
#include "misc/bddlt.hh" #include "misc/bddlt.hh"
// The way we developed this algorithm is the following: We take an // The way we developed this algorithm is the following: We take an
@ -84,9 +83,6 @@ namespace spot
// Used to get the signature of the state. // Used to get the signature of the state.
typedef std::vector<bdd> vector_state_bdd; typedef std::vector<bdd> vector_state_bdd;
typedef std::vector<const state*> vector_state_state;
// Get the list of state for each class. // Get the list of state for each class.
typedef std::map<bdd, std::list<unsigned>, typedef std::map<bdd, std::list<unsigned>,
bdd_less_than> map_bdd_lstate; bdd_less_than> map_bdd_lstate;
@ -187,67 +183,67 @@ namespace spot
return aut->acc().marks(res.begin(), res.end()); return aut->acc().marks(res.begin(), res.end());
} }
direct_simulation(const const_tgba_ptr& t) direct_simulation(const const_tgba_digraph_ptr& in)
: a_(0), : po_size_(0),
po_size_(0),
all_class_var_(bddtrue), all_class_var_(bddtrue),
original_(t) original_(in)
{ {
// We need to do a dupexp for being able to run scc_info later. // Call get_init_state_number() before anything else as it
// new_original_ is the map that contains the relation between // might add a state.
// the names (addresses) of the states in the automaton unsigned init_state_number = in->get_init_state_number();
// returned by dupexp, and in automaton given in argument to scc_info_.reset(new scc_info(in));
// the constructor.
a_ = tgba_dupexp_dfs(t, { true, true, true, true }, new_original_); unsigned ns = in->num_states();
scc_info_.reset(new scc_info(a_)); assert(ns > 0);
old_a_ = a_; size_a_ = ns;
// Replace all the acceptance conditions by their complements. // Replace all the acceptance conditions by their complements.
// (In the case of Cosimulation, we also flip the transitions.) // (In the case of Cosimulation, we also flip the transitions.)
{ if (Cosimulation)
if (Cosimulation) {
{ a_ = make_tgba_digraph(in->get_dict());
a_ = make_tgba_digraph(a_->get_dict()); a_->copy_ap_of(in);
a_->copy_ap_of(old_a_); a_->copy_acceptance_conditions_of(in);
a_->copy_acceptance_conditions_of(old_a_);
}
unsigned ns = old_a_->num_states();
if (Cosimulation)
a_->new_states(ns); a_->new_states(ns);
for (unsigned s = 0; s < ns; ++s) auto& acccond = in->acc();
{
for (auto& t: old_a_->out(s)) for (unsigned s = 0; s < ns; ++s)
{ {
acc_cond::mark_t acc; for (auto& t: in->out(s))
if (Sba && Cosimulation) {
{ acc_cond::mark_t acc;
// If the acceptance is interpreted as if (Sba)
// state-based, to apply the reverse simulation {
// on a SBA, we should pull the acceptance of // If the acceptance is interpreted as
// the destination state on its incoming arcs // state-based, to apply the reverse simulation
// (which now become outgoing arcs after // on a SBA, we should pull the acceptance of
// transposition). // the destination state on its incoming arcs
acc = 0U; // (which now become outgoing arcs after
for (auto& td: old_a_->out(t.dst)) // transposition).
{ acc = 0U;
acc = old_a_->acc().comp(td.acc); for (auto& td: in->out(t.dst))
break; {
} acc = acccond.comp(td.acc);
} break;
else }
{ }
acc = old_a_->acc().comp(t.acc); else
} {
if (Cosimulation) acc = acccond.comp(t.acc);
}
a_->new_transition(t.dst, s, t.cond, acc); a_->new_transition(t.dst, s, t.cond, acc);
else }
t.acc = acc; a_->set_init_state(init_state_number);
} }
if (Cosimulation) }
a_->set_init_state(old_a_->get_init_state_number()); else
} {
size_a_ = ns; a_ = make_tgba_digraph(in, tgba::prop_set::all());
} auto& acccond = a_->acc();
for (auto& t: a_->transitions())
t.acc = acccond.comp(t.acc);
}
assert(a_->num_states() == size_a_);
// Now, we have to get the bdd which will represent the // Now, we have to get the bdd which will represent the
// class. We register one bdd by state, because in the worst // class. We register one bdd by state, because in the worst
@ -678,7 +674,6 @@ namespace spot
protected: protected:
// The automaton which is simulated. // The automaton which is simulated.
tgba_digraph_ptr a_; tgba_digraph_ptr a_;
tgba_digraph_ptr old_a_;
// Relation is aimed to represent the same thing than // Relation is aimed to represent the same thing than
// rel_. The difference is in the way it does. // rel_. The difference is in the way it does.
@ -720,37 +715,36 @@ namespace spot
automaton_size stat; automaton_size stat;
std::unique_ptr<scc_info> scc_info_; std::unique_ptr<scc_info> scc_info_;
std::vector<const state*> new_original_;
const_tgba_ptr original_; const const_tgba_digraph_ptr& original_;
}; };
} // End namespace anonymous. } // End namespace anonymous.
tgba_digraph_ptr tgba_digraph_ptr
simulation(const const_tgba_ptr& t) simulation(const const_tgba_digraph_ptr& t)
{ {
direct_simulation<false, false> simul(t); direct_simulation<false, false> simul(t);
return simul.run(); return simul.run();
} }
tgba_digraph_ptr tgba_digraph_ptr
simulation_sba(const const_tgba_ptr& t) simulation_sba(const const_tgba_digraph_ptr& t)
{ {
direct_simulation<false, true> simul(t); direct_simulation<false, true> simul(t);
return simul.run(); return simul.run();
} }
tgba_digraph_ptr tgba_digraph_ptr
cosimulation(const const_tgba_ptr& t) cosimulation(const const_tgba_digraph_ptr& t)
{ {
direct_simulation<true, false> simul(t); direct_simulation<true, false> simul(t);
return simul.run(); return simul.run();
} }
tgba_digraph_ptr tgba_digraph_ptr
cosimulation_sba(const const_tgba_ptr& t) cosimulation_sba(const const_tgba_digraph_ptr& t)
{ {
direct_simulation<true, true> simul(t); direct_simulation<true, true> simul(t);
return simul.run(); return simul.run();
@ -759,7 +753,7 @@ namespace spot
template<bool Sba> template<bool Sba>
tgba_digraph_ptr tgba_digraph_ptr
iterated_simulations_(const const_tgba_ptr& t) iterated_simulations_(const const_tgba_digraph_ptr& t)
{ {
tgba_digraph_ptr res = 0; tgba_digraph_ptr res = 0;
automaton_size prev; automaton_size prev;
@ -788,13 +782,13 @@ namespace spot
} }
tgba_digraph_ptr tgba_digraph_ptr
iterated_simulations(const const_tgba_ptr& t) iterated_simulations(const const_tgba_digraph_ptr& t)
{ {
return iterated_simulations_<false>(t); return iterated_simulations_<false>(t);
} }
tgba_digraph_ptr tgba_digraph_ptr
iterated_simulations_sba(const const_tgba_ptr& t) iterated_simulations_sba(const const_tgba_digraph_ptr& t)
{ {
return iterated_simulations_<true>(t); return iterated_simulations_<true>(t);
} }

16
src/tgbaalgos/simulation.hh
View file

@ -68,8 +68,10 @@ namespace spot
/// \param automaton the automaton to simulate. /// \param automaton the automaton to simulate.
/// \return a new automaton which is at worst a copy of the received /// \return a new automaton which is at worst a copy of the received
/// one /// one
SPOT_API tgba_digraph_ptr simulation(const const_tgba_ptr& automaton); SPOT_API tgba_digraph_ptr
SPOT_API tgba_digraph_ptr simulation_sba(const const_tgba_ptr& automaton); simulation(const const_tgba_digraph_ptr& automaton);
SPOT_API tgba_digraph_ptr
simulation_sba(const const_tgba_digraph_ptr& automaton);
/// @} /// @}
/// @{ /// @{
@ -119,8 +121,10 @@ namespace spot
/// \param automaton the automaton to simulate. /// \param automaton the automaton to simulate.
/// \return a new automaton which is at worst a copy of the received /// \return a new automaton which is at worst a copy of the received
/// one /// one
SPOT_API tgba_digraph_ptr cosimulation(const const_tgba_ptr& automaton); SPOT_API tgba_digraph_ptr
SPOT_API tgba_digraph_ptr cosimulation_sba(const const_tgba_ptr& automaton); cosimulation(const const_tgba_digraph_ptr& automaton);
SPOT_API tgba_digraph_ptr
cosimulation_sba(const const_tgba_digraph_ptr& automaton);
/// @} /// @}
/// @{ /// @{
@ -139,9 +143,9 @@ namespace spot
/// \return a new automaton which is at worst a copy of the received /// \return a new automaton which is at worst a copy of the received
/// one /// one
SPOT_API tgba_digraph_ptr SPOT_API tgba_digraph_ptr
iterated_simulations(const const_tgba_ptr& automaton); iterated_simulations(const const_tgba_digraph_ptr& automaton);
SPOT_API tgba_digraph_ptr SPOT_API tgba_digraph_ptr
iterated_simulations_sba(const const_tgba_ptr& automaton); iterated_simulations_sba(const const_tgba_digraph_ptr& automaton);
/// @} /// @}
} // End namespace spot. } // End namespace spot.

12
src/tgbatest/ltl2tgba.cc
View file

@ -1209,7 +1209,7 @@ checked_main(int argc, char** argv)
if (reduction_dir_sim && !reduction_iterated_sim) if (reduction_dir_sim && !reduction_iterated_sim)
{ {
tm.start("direct simulation"); tm.start("direct simulation");
a = spot::simulation(a); a = spot::simulation(ensure_digraph(a));
tm.stop("direct simulation"); tm.stop("direct simulation");
assume_sba = false; assume_sba = false;
} }
@ -1217,7 +1217,7 @@ checked_main(int argc, char** argv)
if (reduction_rev_sim && !reduction_iterated_sim) if (reduction_rev_sim && !reduction_iterated_sim)
{ {
tm.start("reverse simulation"); tm.start("reverse simulation");
a = spot::cosimulation(a); a = spot::cosimulation(ensure_digraph(a));
tm.stop("reverse simulation"); tm.stop("reverse simulation");
assume_sba = false; assume_sba = false;
} }
@ -1226,7 +1226,7 @@ checked_main(int argc, char** argv)
if (reduction_iterated_sim) if (reduction_iterated_sim)
{ {
tm.start("Reduction w/ iterated simulations"); tm.start("Reduction w/ iterated simulations");
a = spot::iterated_simulations(a); a = spot::iterated_simulations(ensure_digraph(a));
tm.stop("Reduction w/ iterated simulations"); tm.stop("Reduction w/ iterated simulations");
assume_sba = false; assume_sba = false;
} }
@ -1291,7 +1291,7 @@ checked_main(int argc, char** argv)
if (reduction_dir_sim && !reduction_iterated_sim) if (reduction_dir_sim && !reduction_iterated_sim)
{ {
tm.start("direct simulation 2"); tm.start("direct simulation 2");
a = spot::simulation(a); a = spot::simulation(ensure_digraph(a));
tm.stop("direct simulation 2"); tm.stop("direct simulation 2");
assume_sba = false; assume_sba = false;
} }
@ -1299,7 +1299,7 @@ checked_main(int argc, char** argv)
if (reduction_rev_sim && !reduction_iterated_sim) if (reduction_rev_sim && !reduction_iterated_sim)
{ {
tm.start("reverse simulation 2"); tm.start("reverse simulation 2");
a = spot::cosimulation(a); a = spot::cosimulation(ensure_digraph(a));
tm.stop("reverse simulation 2"); tm.stop("reverse simulation 2");
assume_sba = false; assume_sba = false;
} }
@ -1307,7 +1307,7 @@ checked_main(int argc, char** argv)
if (reduction_iterated_sim) if (reduction_iterated_sim)
{ {
tm.start("Reduction w/ iterated simulations"); tm.start("Reduction w/ iterated simulations");
a = spot::iterated_simulations(a); a = spot::iterated_simulations(ensure_digraph(a));
tm.stop("Reduction w/ iterated simulations"); tm.stop("Reduction w/ iterated simulations");
assume_sba = false; assume_sba = false;
} }