dve2: use postprocessor to simplify the code.
* iface/dve2/dve2check.cc: Use postprocessor to simplify the code. * iface/dve2/dve2check.test: Adjust to some different output values when a counterexample is found, caused by nondeterminism introduced by the orders of transitions.
This commit is contained in:
Alexandre Duret-Lutz
parent
09b540315a
commit
40de47f159
2 changed files with 35 additions and 65 deletions
|
|
@ -24,10 +24,9 @@
|
||||||
#include "ltlast/allnodes.hh"
|
#include "ltlast/allnodes.hh"
|
||||||
#include "ltlparse/public.hh"
|
#include "ltlparse/public.hh"
|
||||||
#include "tgbaalgos/ltl2tgba_fm.hh"
|
#include "tgbaalgos/ltl2tgba_fm.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 "tgbaalgos/postproc.hh"
|
||||||
#include "tgba/tgbaproduct.hh"
|
#include "tgba/tgbaproduct.hh"
|
||||||
#include "misc/timer.hh"
|
#include "misc/timer.hh"
|
||||||
#include "misc/memusage.hh"
|
#include "misc/memusage.hh"
|
||||||
|
|
@ -43,36 +42,23 @@ syntax(char* prog)
|
||||||
if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
|
if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
|
||||||
prog = slash + 4;
|
prog = slash + 4;
|
||||||
|
|
||||||
std::cerr << "usage: " << prog << " [options] model formula" << std::endl
|
std::cerr << "usage: " << prog << " [options] model formula\n\
|
||||||
<< std::endl
|
\n\
|
||||||
<< "Options:" << std::endl
|
Options:\n\
|
||||||
<< " -dDEAD use DEAD as property for marking DEAD states"
|
-dDEAD use DEAD as property for marking DEAD states\n\
|
||||||
<< std::endl
|
(by default DEAD = true)\n\
|
||||||
<< " (by default DEAD = true)" << std::endl
|
-e[ALGO] run emptiness check, expect an accepting run\n\
|
||||||
<< " -e[ALGO] run emptiness check, expect an accepting run"
|
-E[ALGO] run emptiness check, expect no accepting run\n\
|
||||||
<< std::endl
|
-C compute an accepting run (Counterexample) if it exists\n\
|
||||||
<< " -E[ALGO] run emptiness check, expect no accepting run"
|
-D favor a deterministic translation over a small transition\n\
|
||||||
<< std::endl
|
-gf output the automaton of the formula in dot format\n\
|
||||||
<< " -C compute an accepting run (Counterexample) if it exists"
|
-gm output the model state-space in dot format\n\
|
||||||
<< std::endl
|
-gK output the model state-space in Kripke format\n\
|
||||||
<< " -gf output the automaton of the formula in dot format"
|
-gp output the product state-space in dot format\n\
|
||||||
<< std::endl
|
-T time the different phases of the execution\n\
|
||||||
<< " -gm output the model state-space in dot format"
|
-z compress states to handle larger models\n\
|
||||||
<< std::endl
|
-Z compress states (faster) assuming all values in [0 .. 2^28-1]\n\
|
||||||
<< " -gK output the model state-space in Kripke format"
|
";
|
||||||
<< std::endl
|
|
||||||
<< " -gp output the product state-space in dot format"
|
|
||||||
<< std::endl
|
|
||||||
<< " -T time the different phases of the execution"
|
|
||||||
<< std::endl
|
|
||||||
<< " -W enable WDBA minimization"
|
|
||||||
<< std::endl
|
|
||||||
<< " -z compress states to handle larger models"
|
|
||||||
<< std::endl
|
|
||||||
<< " -Z compress states (faster) "
|
|
||||||
<< "assuming all values in [0 .. 2^28-1]"
|
|
||||||
<< std::endl;
|
|
||||||
|
|
||||||
exit(1);
|
exit(1);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -87,7 +73,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;
|
bool deterministic = false;
|
||||||
char *dead = 0;
|
char *dead = 0;
|
||||||
int compress_states = 0;
|
int compress_states = 0;
|
||||||
|
|
||||||
|
|
@ -108,6 +94,9 @@ main(int argc, char **argv)
|
||||||
case 'd':
|
case 'd':
|
||||||
dead = opt + 1;
|
dead = opt + 1;
|
||||||
break;
|
break;
|
||||||
|
case 'D':
|
||||||
|
deterministic = true;
|
||||||
|
break;
|
||||||
case 'e':
|
case 'e':
|
||||||
case 'E':
|
case 'E':
|
||||||
{
|
{
|
||||||
|
|
@ -141,9 +130,6 @@ 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;
|
||||||
|
|
@ -179,6 +165,7 @@ main(int argc, char **argv)
|
||||||
int exit_code = 0;
|
int exit_code = 0;
|
||||||
const spot::ltl::formula* f = 0;
|
const spot::ltl::formula* f = 0;
|
||||||
const spot::ltl::formula* deadf = 0;
|
const spot::ltl::formula* deadf = 0;
|
||||||
|
spot::postprocessor post;
|
||||||
|
|
||||||
if (dead == 0 || !strcasecmp(dead, "true"))
|
if (dead == 0 || !strcasecmp(dead, "true"))
|
||||||
{
|
{
|
||||||
|
|
@ -230,7 +217,6 @@ main(int argc, char **argv)
|
||||||
|
|
||||||
atomic_prop_collect(f, &ap);
|
atomic_prop_collect(f, &ap);
|
||||||
|
|
||||||
|
|
||||||
if (output != DotFormula)
|
if (output != DotFormula)
|
||||||
{
|
{
|
||||||
tm.start("loading dve2");
|
tm.start("loading dve2");
|
||||||
|
|
@ -264,29 +250,12 @@ main(int argc, char **argv)
|
||||||
prop = spot::ltl_to_tgba_fm(f, dict);
|
prop = spot::ltl_to_tgba_fm(f, dict);
|
||||||
tm.stop("translating formula");
|
tm.stop("translating formula");
|
||||||
|
|
||||||
tm.start("reducing A_f w/ SCC");
|
if (deterministic)
|
||||||
{
|
post.set_pref(spot::postprocessor::Deterministic);
|
||||||
spot::tgba* aut_scc = spot::scc_filter(prop, true);
|
|
||||||
delete prop;
|
|
||||||
prop = aut_scc;
|
|
||||||
}
|
|
||||||
tm.stop("reducing A_f w/ SCC");
|
|
||||||
|
|
||||||
if (wdba)
|
tm.start("postprocessing A_f");
|
||||||
{
|
prop = post.run(prop, f);
|
||||||
tm.start("WDBA minimization");
|
tm.stop("postprocessing A_f");
|
||||||
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)
|
||||||
{
|
{
|
||||||
|
|
@ -306,7 +275,6 @@ main(int argc, char **argv)
|
||||||
goto safe_exit;
|
goto safe_exit;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
assert(echeck_inst);
|
assert(echeck_inst);
|
||||||
|
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -39,13 +39,15 @@ for opt in '' '-z'; do
|
||||||
# time with valgrind.).
|
# time with valgrind.).
|
||||||
|
|
||||||
../dve2check $opt -E $srcdir/beem-peterson.4.dve \
|
../dve2check $opt -E $srcdir/beem-peterson.4.dve \
|
||||||
'!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
|
'!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
|
||||||
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
|
| grep -v pages > stdout1
|
||||||
'!G(P_0.wait -> F P_0.CS)' | grep -v pages > stdout1
|
|
||||||
# same formula, different syntax.
|
# same formula, different syntax.
|
||||||
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
|
../dve2check $opt -E $srcdir/beem-peterson.4.dve \
|
||||||
'!G("P_0 == wait" -> F "P_0 == CS")' | grep -v pages > stdout2
|
'!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3== CS")' \
|
||||||
|
| grep -v pages > stdout2
|
||||||
cmp stdout1 stdout2
|
cmp stdout1 stdout2
|
||||||
|
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve \
|
||||||
|
'!G(P_0.wait -> F P_0.CS)'
|
||||||
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
|
run 0 ../dve2check $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
|
||||||
done
|
done
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue