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

Do not output a counterexample by default in ltl2tgba, introduce

Browse source 
options -C and -CR for that.

* src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control
whether we want the accepting run to be printed or replayed.
* src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test,
src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR.
This commit is contained in:
Alexandre Duret-Lutz 2010-11-06 15:38:00 +01:00
parent fe1f59cd30
commit a6677c2984
7 changed files with 103 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,3 +1,14 @@
2010-11-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Do not output a counterexample by default in ltl2tgba, introduce
options -C and -CR for that.
* src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control
whether we want the accepting run to be printed or replayed.
* src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test,
src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR.
2010-11-06 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-11-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Make sure the neverclaim parser works on the output of spin and Make sure the neverclaim parser works on the output of spin and

14
src/tgbatest/dfs.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -79,8 +79,8 @@ s9, s8,,;
s9, s9,,; s9, s9,,;
EOF EOF
run 0 ../ltl2tgba -eSE05 -X blue_counter run 0 ../ltl2tgba -CR -eSE05 -X blue_counter
run 0 ../ltl2tgba -eTau03_opt -X blue_counter run 0 ../ltl2tgba -CR -eTau03_opt -X blue_counter
# s1->s2->s3->(large composant from s4 to s9) # s1->s2->s3->(large composant from s4 to s9)
# ^ || # ^ ||
@ -131,8 +131,8 @@ s9, s8,,;
s9, s9,,; s9, s9,,;
EOF EOF
run 0 ../ltl2tgba -eSE05 -X blue_last run 0 ../ltl2tgba -CR -eSE05 -X blue_last
run 0 ../ltl2tgba -eTau03_opt -X blue_last run 0 ../ltl2tgba -CR -eTau03_opt -X blue_last
# _______ # _______
# | | # | |
@ -187,7 +187,7 @@ s9, s8,,;
s9, s9,,; s9, s9,,;
EOF EOF
run 0 ../ltl2tgba -eSE05 -X red run 0 ../ltl2tgba -CR -eSE05 -X red
run 0 ../ltl2tgba -eTau03_opt -X red run 0 ../ltl2tgba -CR -eTau03_opt -X red
rm -f red blue_counter blue_last rm -f red blue_counter blue_last

6
src/tgbatest/eltl2tgba.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -33,11 +33,11 @@ check_construct()
# translated using FM. # translated using FM.
check_true() check_true()
{ {
run 0 ../ltl2tgba -e -Poutput -f "$1" run 0 ../ltl2tgba -CR -e -Poutput -f "$1"
} }
check_false() check_false()
{ {
run 1 ../ltl2tgba -e -Poutput -f "$1" run 1 ../ltl2tgba -CR -e -Poutput -f "$1"
} }
# Create the prelude file. # Create the prelude file.

82
src/tgbatest/emptchk.test
View file

@ -35,52 +35,54 @@ expect_ce_do()
expect_ce() expect_ce()
{ {
expect_ce_do -e -l "$1" expect_ce_do -CR -e -l "$1"
expect_ce_do -e -l -D "$1" expect_ce_do -CR -e -l -D "$1"
expect_ce_do -e -f "$1" expect_ce_do -CR -e -f "$1"
expect_ce_do -e -f -D "$1" expect_ce_do -CR -e -f -D "$1"
expect_ce_do -e'Cou99(shy)' -l "$1" expect_ce_do -CR -e'Cou99(shy)' -l "$1"
expect_ce_do -e'Cou99(shy)' -l -D "$1" expect_ce_do -CR -e'Cou99(shy)' -l -D "$1"
expect_ce_do -e'Cou99(shy)' -f "$1" expect_ce_do -CR -e'Cou99(shy)' -f "$1"
expect_ce_do -e'Cou99(shy)' -f -D "$1" expect_ce_do -CR -e'Cou99(shy)' -f -D "$1"
expect_ce_do -eCVWY90 -l "$1" expect_ce_do -CR -eCVWY90 -l "$1"
expect_ce_do -eCVWY90 -f "$1" expect_ce_do -CR -eCVWY90 -f "$1"
run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -l "$1" run 0 ../ltl2tgba -CR -e'CVWY90(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -f "$1" run 0 ../ltl2tgba -CR -e'CVWY90(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -eSE05 -l "$1" run 0 ../ltl2tgba -CR -eSE05 -l "$1"
run 0 ../ltl2tgba -eSE05 -f "$1" run 0 ../ltl2tgba -CR -eSE05 -f "$1"
run 0 ../ltl2tgba -e'SE05(bsh=10M)' -l "$1" run 0 ../ltl2tgba -CR -e'SE05(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -e'SE05(bsh=10M)' -f "$1" run 0 ../ltl2tgba -CR -e'SE05(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -eTau03_opt -f "$1" run 0 ../ltl2tgba -CR -eTau03_opt -f "$1"
run 0 ../ltl2tgba -eGV04 -f "$1" run 0 ../ltl2tgba -CR -eGV04 -f "$1"
# Expect multiple accepting runs # Expect multiple accepting runs
test `../ltl2tgba -e'CVWY90(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2 test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "$1" |
test `../ltl2tgba -e'SE05(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2 grep Prefix: | wc -l` -ge $2
test `../ltl2tgba -CR -e'SE05(repeated)' -l "$1" |
grep Prefix: | wc -l` -ge $2
} }
expect_no() expect_no()
{ {
run 0 ../ltl2tgba -E -l "$1" run 0 ../ltl2tgba -CR -E -l "$1"
run 0 ../ltl2tgba -E -l -D "$1" run 0 ../ltl2tgba -CR -E -l -D "$1"
run 0 ../ltl2tgba -E -f "$1" run 0 ../ltl2tgba -CR -E -f "$1"
run 0 ../ltl2tgba -E -f -D "$1" run 0 ../ltl2tgba -CR -E -f -D "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' -l "$1" run 0 ../ltl2tgba -CR -E'Cou99(shy)' -l "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' -l -D "$1" run 0 ../ltl2tgba -CR -E'Cou99(shy)' -l -D "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' -f "$1" run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' -f -D "$1" run 0 ../ltl2tgba -CR -E'Cou99(shy)' -f -D "$1"
run 0 ../ltl2tgba -ECVWY90 -l "$1" run 0 ../ltl2tgba -CR -ECVWY90 -l "$1"
run 0 ../ltl2tgba -ECVWY90 -f "$1" run 0 ../ltl2tgba -CR -ECVWY90 -f "$1"
run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -l "$1" run 0 ../ltl2tgba -CR -E'CVWY90(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -f "$1" run 0 ../ltl2tgba -CR -E'CVWY90(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -ESE05 -l "$1" run 0 ../ltl2tgba -CR -ESE05 -l "$1"
run 0 ../ltl2tgba -ESE05 -f "$1" run 0 ../ltl2tgba -CR -ESE05 -f "$1"
run 0 ../ltl2tgba -E'SE05(bsh=10M)' -l "$1" run 0 ../ltl2tgba -CR -E'SE05(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1" run 0 ../ltl2tgba -CR -E'SE05(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -ETau03_opt -f "$1" run 0 ../ltl2tgba -CR -ETau03_opt -f "$1"
run 0 ../ltl2tgba -EGV04 -f "$1" run 0 ../ltl2tgba -CR -EGV04 -f "$1"
test `../ltl2tgba -e'CVWY90(repeated)' -l "!($1)" | test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "!($1)" |
grep Prefix: | wc -l` -ge $2 grep Prefix: | wc -l` -ge $2
test `../ltl2tgba -e'SE05(repeated)' -l "!($1)" | test `../ltl2tgba -CR -e'SE05(repeated)' -l "!($1)" |
grep Prefix: | wc -l` -ge $2 grep Prefix: | wc -l` -ge $2
} }

16
src/tgbatest/emptchke.test
View file

@ -29,14 +29,14 @@ set -e
expect_ce() expect_ce()
{ {
run 0 ../ltl2tgba -e -X "$1" run 0 ../ltl2tgba -CR -e -X "$1"
run 0 ../ltl2tgba -e -D -X "$1" run 0 ../ltl2tgba -CR -e -D -X "$1"
run 0 ../ltl2tgba -e'Cou99(shy)' -X "$1" run 0 ../ltl2tgba -CR -e'Cou99(shy)' -X "$1"
run 0 ../ltl2tgba -e'Cou99(shy)' -D -X "$1" run 0 ../ltl2tgba -CR -e'Cou99(shy)' -D -X "$1"
run 0 ../ltl2tgba -eCVWY90 -X "$1" run 0 ../ltl2tgba -CR -eCVWY90 -X "$1"
run 0 ../ltl2tgba -eGV04 -X "$1" run 0 ../ltl2tgba -CR -eGV04 -X "$1"
run 0 ../ltl2tgba -eSE05 -X "$1" run 0 ../ltl2tgba -CR -eSE05 -X "$1"
run 0 ../ltl2tgba -eTau03 -X "$1" run 0 ../ltl2tgba -CR -eTau03 -X "$1"
} }
cat >input <<'EOF' cat >input <<'EOF'

28
src/tgbatest/ltl2tgba.cc
View file

@ -214,6 +214,10 @@ syntax(char* prog)
<< "accepting run" << std::endl << "accepting run" << std::endl
<< " -E[ALGO] run emptiness check, expect no accepting run" << " -E[ALGO] run emptiness check, expect no accepting run"
<< std::endl << std::endl
<< " -C compute an accepting run (Counterexample) if it exists"
<< std::endl
<< " -CR compute and replay an accepting run (implies -C)"
<< std::endl
<< " -g graph the accepting run on the automaton (requires -e)" << " -g graph the accepting run on the automaton (requires -e)"
<< std::endl << std::endl
<< " -G graph the accepting run seen as an automaton " << " -G graph the accepting run seen as an automaton "
@ -287,6 +291,8 @@ main(int argc, char** argv)
spot::emptiness_check_instantiator* echeck_inst = 0; spot::emptiness_check_instantiator* echeck_inst = 0;
enum { NoneDup, BFS, DFS } dupexp = NoneDup; enum { NoneDup, BFS, DFS } dupexp = NoneDup;
bool expect_counter_example = false; bool expect_counter_example = false;
bool accepting_run = false;
bool accepting_run_replay = false;
bool from_file = false; bool from_file = false;
bool read_neverclaim = false; bool read_neverclaim = false;
int reduc_aut = spot::Reduce_None; int reduc_aut = spot::Reduce_None;
@ -341,6 +347,15 @@ main(int argc, char** argv)
containment = true; containment = true;
translation = TransTAA; translation = TransTAA;
} }
else if (!strcmp(argv[formula_index], "-C"))
{
accepting_run = true;
}
else if (!strcmp(argv[formula_index], "-CR"))
{
accepting_run = true;
accepting_run_replay = true;
}
else if (!strcmp(argv[formula_index], "-d")) else if (!strcmp(argv[formula_index], "-d"))
{ {
debug_opt = true; debug_opt = true;
@ -440,10 +455,12 @@ main(int argc, char** argv)
} }
else if (!strcmp(argv[formula_index], "-g")) else if (!strcmp(argv[formula_index], "-g"))
{ {
accepting_run = true;
graph_run_opt = true; graph_run_opt = true;
} }
else if (!strcmp(argv[formula_index], "-G")) else if (!strcmp(argv[formula_index], "-G"))
{ {
accepting_run = true;
graph_run_tgba_opt = true; graph_run_tgba_opt = true;
} }
else if (!strcmp(argv[formula_index], "-k")) else if (!strcmp(argv[formula_index], "-k"))
@ -1111,7 +1128,7 @@ main(int argc, char** argv)
std::cout << std::endl; std::cout << std::endl;
break; break;
} }
else else if (accepting_run)
{ {
tm.start("computing accepting run"); tm.start("computing accepting run");
@ -1148,7 +1165,9 @@ main(int argc, char** argv)
else else
{ {
spot::print_tgba_run(std::cout, a, run); spot::print_tgba_run(std::cout, a, run);
if (!spot::replay_tgba_run(std::cout, a, run,
if (accepting_run_replay
&& !spot::replay_tgba_run(std::cout, a, run,
true)) true))
exit_code = 1; exit_code = 1;
} }
@ -1156,6 +1175,11 @@ main(int argc, char** argv)
tm.stop("printing accepting run"); tm.stop("printing accepting run");
} }
} }
else
{
std::cout << "an accepting run exists "
<< "(use -C to print it)" << std::endl;
}
} }
delete res; delete res;
} }

8
src/tgbatest/ltlcounter.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement de # Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de
# l'EPITA (LRDE) # l'EPITA (LRDE)
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -36,10 +36,10 @@ run='run 0'
check_formula() check_formula()
{ {
# First, check the satisfiability of the formula with Spot # First, check the satisfiability of the formula with Spot
$run ../ltl2tgba -e -x -f "$1" >/dev/null $run ../ltl2tgba -CR -e -x -f "$1" >/dev/null
# Also check the satisfiability of the degeneralized formula # Also check the satisfiability of the degeneralized formula
$run ../ltl2tgba -e -D -x -f "$1" >/dev/null $run ../ltl2tgba -CR -e -D -x -f "$1" >/dev/null
$run ../ltl2tgba -e -DS -x -f "$1" >/dev/null $run ../ltl2tgba -CR -e -DS -x -f "$1" >/dev/null
} }
# Kristin Y. Rozier reported that the formulae with n=10 were badly # Kristin Y. Rozier reported that the formulae with n=10 were badly