Commit a0cce105 authored by Thomas Badie's avatar Thomas Badie Committed by Alexandre Duret-Lutz
Browse files

Create the iterated simulations.

* src/tgbaalgos/simulation.cc: Create the iterated_simulations.
(direct_simulation) Add an attribute "stat" that represents the
number of states and transitions of the resulting automaton.
* src/tgbaalgos/simulation.hh: Declare the iterated_simulations.
* src/tgbatest/spotlbtt.test: Test the iterated_simulations.
* src/tgbatest/ltl2tgba.cc: Associate the option -RIS to the
iterated_simulations.
parent 242386b1
...@@ -28,6 +28,7 @@ ...@@ -28,6 +28,7 @@
#include "misc/minato.hh" #include "misc/minato.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
#include "tgbaalgos/reachiter.hh" #include "tgbaalgos/reachiter.hh"
#include "tgbaalgos/sccfilter.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
// automaton, and reverse all these acceptance conditions. We reverse // automaton, and reverse all these acceptance conditions. We reverse
...@@ -104,6 +105,22 @@ namespace spot ...@@ -104,6 +105,22 @@ namespace spot
typedef std::map<bdd, std::list<const state*>, typedef std::map<bdd, std::list<const state*>,
bdd_less_than> map_bdd_lstate; bdd_less_than> map_bdd_lstate;
struct automaton_size
{
automaton_size()
: transitions(0),
states(0)
{
}
inline bool operator!= (const automaton_size& r)
{
return transitions != r.transitions || states != r.states;
}
int transitions;
int states;
};
// This class takes an automaton and creates a copy with all // This class takes an automaton and creates a copy with all
// acceptance conditions complemented. // acceptance conditions complemented.
...@@ -146,7 +163,6 @@ namespace spot ...@@ -146,7 +163,6 @@ namespace spot
int src = get_state(in_s); int src = get_state(in_s);
int dst = get_state(out_s); int dst = get_state(out_s);
// In the case of the cosimulation, we want to have all the // In the case of the cosimulation, we want to have all the
// ingoing transition, and to keep the rest of the code // ingoing transition, and to keep the rest of the code
// similar, we just create equivalent transition in the other // similar, we just create equivalent transition in the other
...@@ -223,7 +239,6 @@ namespace spot ...@@ -223,7 +239,6 @@ namespace spot
bdd init = bdd_ithvar(set_num++); bdd init = bdd_ithvar(set_num++);
used_var_.push_back(init); used_var_.push_back(init);
all_class_var_ = init;
// We fetch the result the run of acc_compl_automaton which // We fetch the result the run of acc_compl_automaton which
// has recorded all the state in a hash table, and we set all // has recorded all the state in a hash table, and we set all
...@@ -240,6 +255,7 @@ namespace spot ...@@ -240,6 +255,7 @@ namespace spot
// of these in a variable all_class_var_ which will be used // of these in a variable all_class_var_ which will be used
// to understand the destination part in the signature when // to understand the destination part in the signature when
// building the resulting automaton. // building the resulting automaton.
all_class_var_ = init;
for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i) for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i)
{ {
free_var_.push(i); free_var_.push(i);
...@@ -443,6 +459,14 @@ namespace spot ...@@ -443,6 +459,14 @@ namespace spot
} }
} }
automaton_size get_stat() const
{
assert(stat.states != 0);
return stat;
}
// Build the minimal resulting automaton. // Build the minimal resulting automaton.
tgba* build_result() tgba* build_result()
{ {
...@@ -489,6 +513,9 @@ namespace spot ...@@ -489,6 +513,9 @@ namespace spot
bdd2state[relation_[part]] = current_max; bdd2state[relation_[part]] = current_max;
} }
stat.states = bdd_lstate_.size();
stat.transitions = 0;
// For each partition, we will create // For each partition, we will create
// all the transitions between the states. // all the transitions between the states.
for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
...@@ -533,6 +560,8 @@ namespace spot ...@@ -533,6 +560,8 @@ namespace spot
bdd cond_acc_dest; bdd cond_acc_dest;
while ((cond_acc_dest = isop.next()) != bddfalse) while ((cond_acc_dest = isop.next()) != bddfalse)
{ {
++stat.transitions;
// Take the transition, and keep only the variable which // Take the transition, and keep only the variable which
// are used to represent the class. // are used to represent the class.
bdd dest = bdd_existcomp(cond_acc_dest, bdd dest = bdd_existcomp(cond_acc_dest,
...@@ -665,6 +694,8 @@ namespace spot ...@@ -665,6 +694,8 @@ namespace spot
// Initial state of the automaton we are working on // Initial state of the automaton we are working on
state* initial_state; state* initial_state;
automaton_size stat;
}; };
} // End namespace anonymous. } // End namespace anonymous.
...@@ -685,4 +716,38 @@ namespace spot ...@@ -685,4 +716,38 @@ namespace spot
return simul.run(); return simul.run();
} }
tgba*
iterated_simulations(const tgba* t)
{
tgba* res = const_cast<tgba*> (t);
automaton_size prev;
automaton_size next;
do
{
prev = next;
direct_simulation<false> simul(res);
tgba* after_simulation = simul.run();
if (res != t)
delete res;
direct_simulation<true> cosimul(after_simulation);
tgba* after_cosimulation = cosimul.run();
next = cosimul.get_stat();
res = scc_filter(after_cosimulation, false);
delete after_cosimulation;
delete after_simulation;
}
while (prev != next);
return res;
}
} // End namespace spot. } // End namespace spot.
...@@ -85,6 +85,12 @@ namespace spot ...@@ -85,6 +85,12 @@ namespace spot
/// one /// one
tgba* cosimulation(const tgba* automaton); tgba* cosimulation(const tgba* automaton);
/// \brief Run a loop: simulation / cosimulation / scc_filter until
/// a fix point is reached.
tgba* iterated_simulations(const tgba* automaton);
/// @} /// @}
} // End namespace spot. } // End namespace spot.
......
...@@ -206,6 +206,9 @@ syntax(char* prog) ...@@ -206,6 +206,9 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -RRS minimize the automaton with reverse simulation" << " -RRS minimize the automaton with reverse simulation"
<< std::endl << std::endl
<< " -RPS minimize the automaton with an alternance"
<< " reverse simulation and simulation"
<< std::endl
<< " -Rm attempt to WDBA-minimize the automata" << std::endl << " -Rm attempt to WDBA-minimize the automata" << std::endl
<< std::endl << std::endl
...@@ -355,6 +358,7 @@ main(int argc, char** argv) ...@@ -355,6 +358,7 @@ main(int argc, char** argv)
bool assume_sba = false; bool assume_sba = false;
bool reduction_dir_sim = false; bool reduction_dir_sim = false;
bool reduction_rev_sim = false; bool reduction_rev_sim = false;
bool reduction_iterated_sim = false;
spot::tgba* temp_dir_sim = 0; spot::tgba* temp_dir_sim = 0;
bool ta_opt = false; bool ta_opt = false;
bool tgta_opt = false; bool tgta_opt = false;
...@@ -362,6 +366,8 @@ main(int argc, char** argv) ...@@ -362,6 +366,8 @@ main(int argc, char** argv)
bool opt_single_pass_emptiness_check = false; bool opt_single_pass_emptiness_check = false;
bool opt_with_artificial_livelock = false; bool opt_with_artificial_livelock = false;
spot::tgba* temp_rev_sim = 0; spot::tgba* temp_rev_sim = 0;
spot::tgba* temp_iterated_sim = 0;
for (;;) for (;;)
{ {
...@@ -663,6 +669,10 @@ main(int argc, char** argv) ...@@ -663,6 +669,10 @@ main(int argc, char** argv)
{ {
reduction_dir_sim = true; reduction_dir_sim = true;
} }
else if (!strcmp(argv[formula_index], "-RIS"))
{
reduction_iterated_sim = true;
}
else if (!strcmp(argv[formula_index], "-rL")) else if (!strcmp(argv[formula_index], "-rL"))
{ {
simpltl = true; simpltl = true;
...@@ -1062,6 +1072,15 @@ main(int argc, char** argv) ...@@ -1062,6 +1072,15 @@ main(int argc, char** argv)
assume_sba = false; assume_sba = false;
} }
if (reduction_iterated_sim)
{
tm.start("Reduction w/ iterated simulations");
temp_iterated_sim = spot::iterated_simulations(a);
a = temp_iterated_sim;
tm.stop("Reduction w/ iterated simulations");
assume_sba = false;
}
unsigned int n_acc = a->number_of_acceptance_conditions(); unsigned int n_acc = a->number_of_acceptance_conditions();
if (echeck_inst if (echeck_inst
...@@ -1523,6 +1542,7 @@ main(int argc, char** argv) ...@@ -1523,6 +1542,7 @@ main(int argc, char** argv)
delete echeck_inst; delete echeck_inst;
delete temp_dir_sim; delete temp_dir_sim;
delete temp_rev_sim; delete temp_rev_sim;
delete temp_iterated_sim;
} }
else else
{ {
......
...@@ -207,6 +207,14 @@ Algorithm ...@@ -207,6 +207,14 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "Spot (Couvreur -- FM), iterated simulation"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -f -t -RIS -r4 -R3'"
Enabled = yes
}
Algorithm Algorithm
{ {
......
Supports Markdown
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