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

* iface/dve2/dve2check.cc: Add option -W and simplify formulae.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2011-07-26 18:55:19 +02:00
parent 1719287b1e
commit cdb4e36121
2 changed files with 37 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2011-07-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/dve2/dve2check.cc: Add option -W and simplify formulae.
2011-07-26 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-07-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
-e means we expect an accepting run. -e means we expect an accepting run.

34
iface/dve2/dve2check.cc
View file

@ -23,8 +23,10 @@
#include "ltlenv/defaultenv.hh" #include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlparse/public.hh" #include "ltlparse/public.hh"
#include "ltlvisit/reduce.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/reducerun.hh"
#include "tgba/tgbaproduct.hh" #include "tgba/tgbaproduct.hh"
@ -60,6 +62,8 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -T time the different phases of the execution" << " -T time the different phases of the execution"
<< std::endl << std::endl
<< " -W enable WDBA minimization"
<< std::endl
<< " -z compress states to handle larger models" << " -z compress states to handle larger models"
<< std::endl << std::endl
<< " -Z compress states (faster) " << " -Z compress states (faster) "
@ -80,6 +84,7 @@ main(int argc, char **argv)
output = EmptinessCheck; output = EmptinessCheck;
bool accepting_run = false; bool accepting_run = false;
bool expect_counter_example = false; bool expect_counter_example = false;
bool wdba = false;
char *dead = 0; char *dead = 0;
int compress_states = 0; int compress_states = 0;
@ -130,6 +135,9 @@ main(int argc, char **argv)
case 'T': case 'T':
use_timer = true; use_timer = true;
break; break;
case 'W':
wdba = true;
break;
case 'z': case 'z':
compress_states = 1; compress_states = 1;
break; break;
@ -159,7 +167,7 @@ main(int argc, char **argv)
spot::ltl::atomic_prop_set ap; spot::ltl::atomic_prop_set ap;
spot::bdd_dict* dict = new spot::bdd_dict(); spot::bdd_dict* dict = new spot::bdd_dict();
spot::kripke* model = 0; spot::kripke* model = 0;
spot::tgba* prop = 0; const spot::tgba* prop = 0;
spot::tgba* product = 0; spot::tgba* product = 0;
spot::emptiness_check_instantiator* echeck_inst = 0; spot::emptiness_check_instantiator* echeck_inst = 0;
int exit_code = 0; int exit_code = 0;
@ -204,6 +212,14 @@ main(int argc, char **argv)
if (exit_code) if (exit_code)
goto safe_exit; goto safe_exit;
tm.start("reducing formula");
{
spot::ltl::formula* r = spot::ltl::reduce(f);
f->destroy();
f = r;
}
tm.stop("reducing formula");
atomic_prop_collect(f, &ap); atomic_prop_collect(f, &ap);
@ -241,6 +257,22 @@ main(int argc, char **argv)
} }
tm.stop("reducing A_f w/ SCC"); tm.stop("reducing A_f w/ SCC");
if (wdba)
{
tm.start("WDBA minimization");
const spot::tgba* minimized = 0;
minimized = minimize_obligation(prop, f);
if (minimized != prop)
{
delete prop;
prop = minimized;
}
tm.stop("WDBA minimization");
}
if (output == DotFormula) if (output == DotFormula)
{ {
tm.start("dotty output"); tm.start("dotty output");