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

Optimize the use of -RRS with -R3.

* src/tgbatest/ltl2tgba.cc: Change the order of the call to the
simulation and the cosimulation.
Call scc_filter when cosimulation is called with -R3.
Call scc_filter when simulation is called with -R3.
parent 0b74f549
...@@ -1053,6 +1053,23 @@ main(int argc, char** argv) ...@@ -1053,6 +1053,23 @@ main(int argc, char** argv)
} }
} }
if (reduction_dir_sim)
{
tm.start("Reduction w/ direct simulation");
temp_dir_sim = spot::simulation(a);
a = temp_dir_sim;
tm.stop("Reduction w/ direct simulation");
assume_sba = false;
if (scc_filter)
{
tm.start("reducing A_f w/ SCC");
delete aut_scc;
aut_scc = a = spot::scc_filter(a, scc_filter_all);
tm.stop("reducing A_f w/ SCC");
assume_sba = false;
}
}
if (reduction_rev_sim) if (reduction_rev_sim)
{ {
...@@ -1061,17 +1078,20 @@ main(int argc, char** argv) ...@@ -1061,17 +1078,20 @@ main(int argc, char** argv)
a = temp_rev_sim; a = temp_rev_sim;
tm.stop("Reduction w/ reverse simulation"); tm.stop("Reduction w/ reverse simulation");
assume_sba = false; assume_sba = false;
}
if (reduction_dir_sim) if (scc_filter)
{ {
tm.start("Reduction w/ direct simulation"); tm.start("reducing A_f w/ SCC");
temp_dir_sim = spot::simulation(a); delete aut_scc;
a = temp_dir_sim; aut_scc = a = spot::scc_filter(a, scc_filter_all);
tm.stop("Reduction w/ direct simulation"); tm.stop("reducing A_f w/ SCC");
assume_sba = false; assume_sba = false;
}
} }
if (reduction_iterated_sim) if (reduction_iterated_sim)
{ {
tm.start("Reduction w/ iterated simulations"); tm.start("Reduction w/ iterated simulations");
......
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