* src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by
-eALGO and -EALGO to ease the addition of new algorithms. * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
7fce2b2a95
commit
4654da9ab5
4 changed files with 68 additions and 68 deletions
|
|
@ -1,5 +1,9 @@
|
|||
2004-10-29 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by
|
||||
-eALGO and -EALGO to ease the addition of new algorithms.
|
||||
* src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust.
|
||||
|
||||
* src/misc/version.cc: Fix trailing whitespace.
|
||||
* src/sanity/style.test: Diagnose trailing whitespace.
|
||||
|
||||
|
|
|
|||
|
|
@ -31,12 +31,12 @@ expect_ce()
|
|||
run 0 ./ltl2tgba -e -D "$1"
|
||||
run 0 ./ltl2tgba -e -f "$1"
|
||||
run 0 ./ltl2tgba -e -f -D "$1"
|
||||
run 0 ./ltl2tgba -e2 "$1"
|
||||
run 0 ./ltl2tgba -e2 -D "$1"
|
||||
run 0 ./ltl2tgba -e2 -f "$1"
|
||||
run 0 ./ltl2tgba -e2 -f -D "$1"
|
||||
run 0 ./ltl2tgba -m "$1"
|
||||
run 0 ./ltl2tgba -m -f "$1"
|
||||
run 0 ./ltl2tgba -ecouvreur99_shy "$1"
|
||||
run 0 ./ltl2tgba -ecouvreur99_shy -D "$1"
|
||||
run 0 ./ltl2tgba -ecouvreur99_shy -f "$1"
|
||||
run 0 ./ltl2tgba -ecouvreur99_shy -f -D "$1"
|
||||
run 0 ./ltl2tgba -emagic_search "$1"
|
||||
run 0 ./ltl2tgba -emagic_search -f "$1"
|
||||
}
|
||||
|
||||
expect_no()
|
||||
|
|
@ -45,12 +45,12 @@ expect_no()
|
|||
run 0 ./ltl2tgba -E -D "$1"
|
||||
run 0 ./ltl2tgba -E -f "$1"
|
||||
run 0 ./ltl2tgba -E -f -D "$1"
|
||||
run 0 ./ltl2tgba -E2 "$1"
|
||||
run 0 ./ltl2tgba -E2 -D "$1"
|
||||
run 0 ./ltl2tgba -E2 -f "$1"
|
||||
run 0 ./ltl2tgba -E2 -f -D "$1"
|
||||
run 0 ./ltl2tgba -M "$1"
|
||||
run 0 ./ltl2tgba -M -f "$1"
|
||||
run 0 ./ltl2tgba -Ecouvreur99_shy "$1"
|
||||
run 0 ./ltl2tgba -Ecouvreur99_shy -D "$1"
|
||||
run 0 ./ltl2tgba -Ecouvreur99_shy -f "$1"
|
||||
run 0 ./ltl2tgba -Ecouvreur99_shy -f -D "$1"
|
||||
run 0 ./ltl2tgba -Emagic_search "$1"
|
||||
run 0 ./ltl2tgba -Emagic_search -f "$1"
|
||||
}
|
||||
|
||||
expect_ce 'a'
|
||||
|
|
@ -67,5 +67,6 @@ expect_no '!((FF a) <=> (F a))'
|
|||
expect_no 'Xa && (!a U b) && !b && X!b'
|
||||
expect_no '(a U !b) && Gb'
|
||||
|
||||
# Expect at least four counter-examples.
|
||||
test `./ltl2tgba -n 'FFx <=> Fx' | grep Prefix: | wc -l` -ge 4
|
||||
# Expect at least four accepting runs
|
||||
test `./ltl2tgba -emagic_search_repeated 'FFx <=> Fx' |
|
||||
grep Prefix: | wc -l` -ge 4
|
||||
|
|
|
|||
|
|
@ -33,5 +33,5 @@ s1, "s2", "a & !b", c d;
|
|||
EOF
|
||||
|
||||
run 0 ./ltl2tgba -e -X input
|
||||
run 0 ./ltl2tgba -e2 -X input
|
||||
run 0 ./ltl2tgba -m -X input
|
||||
run 0 ./ltl2tgba -ecouvreur99_shy -X input
|
||||
run 0 ./ltl2tgba -emagic_search -X input
|
||||
|
|
|
|||
|
|
@ -58,24 +58,13 @@ syntax(char* prog)
|
|||
<< " -A same as -a, but as a set" << std::endl
|
||||
<< " -d turn on traces during parsing" << std::endl
|
||||
<< " -D degeneralize the automaton" << std::endl
|
||||
<< " -e emptiness-check (Couvreur), expect and compute "
|
||||
<< "a counter-example" << std::endl
|
||||
<< " -e2 emptiness-check (Couvreur variant), expect and compute "
|
||||
<< "a counter-example" << std::endl
|
||||
<< " -E emptiness-check (Couvreur), expect no counter-example "
|
||||
<< " -eALGO emptiness-check, expect and compute an accepting run"
|
||||
<< std::endl
|
||||
<< " -E2 emptiness-check (Couvreur variant), expect no "
|
||||
<< "counter-example " << std::endl
|
||||
<< " -EALGO emptiness-check, expect no accepting run" << std::endl
|
||||
<< " -f use Couvreur's FM algorithm for translation"
|
||||
<< std::endl
|
||||
<< " -F read the formula from the file" << std::endl
|
||||
<< " -L fair-loop approximation (implies -f)" << std::endl
|
||||
<< " -m magic-search (implies -D), expect a counter-example"
|
||||
<< std::endl
|
||||
<< " -M magic-search (implies -D), expect no counter-example"
|
||||
<< std::endl
|
||||
<< " -n same as -m, but display more counter-examples"
|
||||
<< std::endl
|
||||
<< " -N display the never clain for Spin "
|
||||
<< "(implies -D)" << std::endl
|
||||
<< " -p branching postponement (implies -f)" << std::endl
|
||||
|
|
@ -121,7 +110,14 @@ syntax(char* prog)
|
|||
<< " -X do not compute an automaton, read it from a file"
|
||||
<< std::endl
|
||||
<< " -y do not merge states with same symbolic representation "
|
||||
<< "(implies -f)" << std::endl;
|
||||
<< "(implies -f)" << std::endl
|
||||
<< std::endl
|
||||
<< "Where ALGO should be one of:" << std::endl
|
||||
<< " couvreur99" << std::endl
|
||||
<< " couvreur99_shy" << std::endl
|
||||
<< " magic_search" << std::endl
|
||||
<< " magic_search_repeated" << std::endl
|
||||
;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
|
|
@ -138,6 +134,7 @@ main(int argc, char** argv)
|
|||
bool file_opt = false;
|
||||
int output = 0;
|
||||
int formula_index = 0;
|
||||
std::string echeck_algo;
|
||||
enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None;
|
||||
enum { NoneDup, BFS, DFS } dupexp = NoneDup;
|
||||
bool magic_many = false;
|
||||
|
|
@ -176,27 +173,21 @@ main(int argc, char** argv)
|
|||
{
|
||||
degeneralize_opt = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-e"))
|
||||
else if (!strncmp(argv[formula_index], "-e", 2))
|
||||
{
|
||||
echeck = Couvreur;
|
||||
if (argv[formula_index][2] != 0)
|
||||
echeck_algo = argv[formula_index] + 2;
|
||||
else
|
||||
echeck_algo = "couvreur99";
|
||||
expect_counter_example = true;
|
||||
output = -1;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-e2"))
|
||||
else if (!strncmp(argv[formula_index], "-E", 2))
|
||||
{
|
||||
echeck = Couvreur2;
|
||||
expect_counter_example = true;
|
||||
output = -1;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-E"))
|
||||
{
|
||||
echeck = Couvreur;
|
||||
expect_counter_example = false;
|
||||
output = -1;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-E2"))
|
||||
{
|
||||
echeck = Couvreur2;
|
||||
if (argv[formula_index][2] != 0)
|
||||
echeck_algo = argv[formula_index] + 2;
|
||||
else
|
||||
echeck_algo = "couvreur99";
|
||||
expect_counter_example = false;
|
||||
output = -1;
|
||||
}
|
||||
|
|
@ -213,28 +204,6 @@ main(int argc, char** argv)
|
|||
fair_loop_approx = true;
|
||||
fm_opt = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-m"))
|
||||
{
|
||||
echeck = MagicSearch;
|
||||
degeneralize_opt = true;
|
||||
expect_counter_example = true;
|
||||
output = -1;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-M"))
|
||||
{
|
||||
echeck = MagicSearch;
|
||||
degeneralize_opt = true;
|
||||
expect_counter_example = false;
|
||||
output = -1;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-n"))
|
||||
{
|
||||
echeck = MagicSearch;
|
||||
degeneralize_opt = true;
|
||||
expect_counter_example = true;
|
||||
output = -1;
|
||||
magic_many = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-N"))
|
||||
{
|
||||
degeneralize_opt = true;
|
||||
|
|
@ -350,6 +319,32 @@ main(int argc, char** argv)
|
|||
}
|
||||
}
|
||||
|
||||
if (echeck_algo == "couvreur99")
|
||||
{
|
||||
echeck = Couvreur;
|
||||
}
|
||||
else if (echeck_algo == "couvreur99_shy")
|
||||
{
|
||||
echeck = Couvreur2;
|
||||
}
|
||||
else if (echeck_algo == "magic_search")
|
||||
{
|
||||
echeck = MagicSearch;
|
||||
degeneralize_opt = true;
|
||||
}
|
||||
else if (echeck_algo == "magic_search_repeated")
|
||||
{
|
||||
echeck = MagicSearch;
|
||||
degeneralize_opt = true;
|
||||
magic_many = true;
|
||||
}
|
||||
else
|
||||
{
|
||||
std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl;
|
||||
syntax(argv[0]);
|
||||
}
|
||||
|
||||
|
||||
std::string input;
|
||||
|
||||
if (file_opt)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue