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

Don't use -Rm for two different things.

Browse source 
* src/tgbatest/ltl2tgba.cc: Introduce -RT to turn on bisimulation on
TA instead of hijacking -Rm.
* src/tgbatest/ltl2ta.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-24 13:35:12 +02:00
parent 6bd905c63e
commit 20c7f1e8cf
2 changed files with 50 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

54
src/tgbatest/ltl2ta.test
View file

@ -27,21 +27,21 @@ set -e
check () check ()
{ {
run 0 ../ltl2tgba -TA -ks "$1" run 0 ../ltl2tgba -TA -ks "$1"
run 0 ../ltl2tgba -TA -Rm -ks "$1" run 0 ../ltl2tgba -TA -RT -ks "$1"
run 0 ../ltl2tgba -TA -lv -ks "$1" run 0 ../ltl2tgba -TA -lv -ks "$1"
run 0 ../ltl2tgba -TA -sp -ks "$1" run 0 ../ltl2tgba -TA -sp -ks "$1"
run 0 ../ltl2tgba -TA -Rm -lv "$1" run 0 ../ltl2tgba -TA -RT -lv "$1"
run 0 ../ltl2tgba -TA -Rm -sp -ks "$1" run 0 ../ltl2tgba -TA -RT -sp -ks "$1"
run 0 ../ltl2tgba -TA -lv -sp -ks "$1" run 0 ../ltl2tgba -TA -lv -sp -ks "$1"
run 0 ../ltl2tgba -TA -DS -ks "$1" run 0 ../ltl2tgba -TA -DS -ks "$1"
run 0 ../ltl2tgba -TA -Rm -DS -ks "$1" run 0 ../ltl2tgba -TA -RT -DS -ks "$1"
run 0 ../ltl2tgba -TA -lv -DS -ks "$1" run 0 ../ltl2tgba -TA -lv -DS -ks "$1"
run 0 ../ltl2tgba -TA -sp -DS -ks "$1" run 0 ../ltl2tgba -TA -sp -DS -ks "$1"
run 0 ../ltl2tgba -TA -Rm -sp -DS -ks "$1" run 0 ../ltl2tgba -TA -RT -sp -DS -ks "$1"
run 0 ../ltl2tgba -TA -Rm -lv -DS -ks "$1" run 0 ../ltl2tgba -TA -RT -lv -DS -ks "$1"
run 0 ../ltl2tgba -TA -Rm -sp -lv -DS -ks "$1" run 0 ../ltl2tgba -TA -RT -sp -lv -DS -ks "$1"
run 0 ../ltl2tgba -TGTA -ks "$1" run 0 ../ltl2tgba -TGTA -ks "$1"
run 0 ../ltl2tgba -TGTA -Rm -ks "$1" run 0 ../ltl2tgba -TGTA -RT -ks "$1"
} }
# We don't check the output, but just running these might be enough to # We don't check the output, but just running these might be enough to
@ -71,7 +71,7 @@ done
for opt in -TA; do for opt in -TA; do
../ltl2tgba -ks $opt -Rm -in -DS 'a U (b U c)' > stdout ../ltl2tgba -ks $opt -RT -in -DS 'a U (b U c)' > stdout
grep 'transitions: 69$' stdout grep 'transitions: 69$' stdout
grep 'states: 10$' stdout grep 'states: 10$' stdout
done done
@ -79,14 +79,14 @@ done
for opt in -TA; do for opt in -TA; do
../ltl2tgba -ks $opt -Rm -DS '!(Ga U b)' > stdout ../ltl2tgba -ks $opt -RT -DS '!(Ga U b)' > stdout
grep 'transitions: 15$' stdout grep 'transitions: 15$' stdout
grep 'states: 5$' stdout grep 'states: 5$' stdout
done done
for opt in -TA; do for opt in -TA; do
../ltl2tgba -ks $opt -Rm -DS 'Ga U b' > stdout ../ltl2tgba -ks $opt -RT -DS 'Ga U b' > stdout
grep 'transitions: 13$' stdout grep 'transitions: 13$' stdout
grep 'states: 6$' stdout grep 'states: 6$' stdout
done done
@ -100,9 +100,9 @@ f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
grep 'transitions: 96$' stdout grep 'transitions: 96$' stdout
grep 'states: 21$' stdout grep 'states: 21$' stdout
# Note: after minimization with -TA -Rm. # Note: after minimization with -TA -RT.
# has 20 states and 89 transitions, after minimization. # has 20 states and 89 transitions, after minimization.
../ltl2tgba -ks -TA -Rm -DS "$f" > stdout ../ltl2tgba -ks -TA -RT -DS "$f" > stdout
grep 'transitions: 89$' stdout grep 'transitions: 89$' stdout
grep 'states: 20$' stdout grep 'states: 20$' stdout
@ -114,7 +114,7 @@ grep 'states: 449$' stdout
f='GFa & GFb & GFc & GFd & GFe & GFg' f='GFa & GFb & GFc & GFd & GFe & GFg'
../ltl2tgba -ks -TA -Rm -x -lv -DS "$f" > stdout ../ltl2tgba -ks -TA -RT -x -lv -DS "$f" > stdout
grep 'transitions: 18496$' stdout grep 'transitions: 18496$' stdout
grep 'states: 290$' stdout grep 'states: 290$' stdout
@ -124,41 +124,41 @@ run 0 ../ltl2tgba -ks -TA -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 882$' stdout grep 'transitions: 882$' stdout
grep 'states: 78$' stdout grep 'states: 78$' stdout
run 0 ../ltl2tgba -TA -Rm -ks -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout run 0 ../ltl2tgba -TA -RT -ks -lv -DS "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
grep 'transitions: 440$' stdout grep 'transitions: 440$' stdout
grep 'states: 28$' stdout grep 'states: 28$' stdout
run 0 ../ltl2tgba -TGTA -Rm -ks 'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout run 0 ../ltl2tgba -TGTA -RT -ks 'Gq|Gr|(G(q|FGp)&G(r|FG!p))' >stdout
grep 'transitions: 294$' stdout grep 'transitions: 294$' stdout
grep 'states: 21$' stdout grep 'states: 21$' stdout
f="FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)" f="FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)"
run 0 ../ltl2tgba -TA -Rm -ks -in -R3f -x -DS "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks -in -R3f -x -DS "$f" >stdout
grep 'transitions: 450$' stdout grep 'transitions: 450$' stdout
grep 'states: 38$' stdout grep 'states: 38$' stdout
run 0 ../ltl2tgba -TA -Rm -ks -lv -R3f -x -DS "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks -lv -R3f -x -DS "$f" >stdout
grep 'transitions: 555$' stdout grep 'transitions: 555$' stdout
grep 'states: 40$' stdout grep 'states: 40$' stdout
run 0 ../ltl2tgba -TA -Rm -ks "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks "$f" >stdout
grep 'transitions: 424$' stdout grep 'transitions: 424$' stdout
grep 'states: 31$' stdout grep 'states: 31$' stdout
run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -in "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks -sp -lv -in "$f" >stdout
grep 'transitions: 485$' stdout grep 'transitions: 485$' stdout
grep 'states: 32$' stdout grep 'states: 32$' stdout
run 0 ../ltl2tgba -TA -Rm -ks -in -R3 -x -DS "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks -in -R3 -x -DS "$f" >stdout
grep 'transitions: 436$' stdout grep 'transitions: 436$' stdout
grep 'states: 36$' stdout grep 'states: 36$' stdout
run 0 ../ltl2tgba -TA -Rm -ks -sp -lv -R3 -x -DS "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks -sp -lv -R3 -x -DS "$f" >stdout
grep 'transitions: 537$' stdout grep 'transitions: 537$' stdout
grep 'states: 38$' stdout grep 'states: 38$' stdout
@ -168,25 +168,25 @@ grep 'transitions: 609$' stdout
grep 'states: 46$' stdout grep 'states: 46$' stdout
run 0 ../ltl2tgba -TA -Rm -ks -sp -lv "$f" >stdout run 0 ../ltl2tgba -TA -RT -ks -sp -lv "$f" >stdout
grep 'transitions: 504$' stdout grep 'transitions: 504$' stdout
grep 'states: 33$' stdout grep 'states: 33$' stdout
run 0 ../ltl2tgba -TGTA -Rm -ks "$f" >stdout run 0 ../ltl2tgba -TGTA -RT -ks "$f" >stdout
grep 'transitions: 527$' stdout grep 'transitions: 527$' stdout
grep 'states: 32$' stdout grep 'states: 32$' stdout
g="G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))" g="G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))"
run 0 ../ltl2tgba -TA -Rm -ks -DS "$g" >stdout run 0 ../ltl2tgba -TA -RT -ks -DS "$g" >stdout
grep 'transitions: 2147$' stdout grep 'transitions: 2147$' stdout
grep 'states: 97$' stdout grep 'states: 97$' stdout
run 0 ../ltl2tgba -TA -Rm -ks -sp "$g" >stdout run 0 ../ltl2tgba -TA -RT -ks -sp "$g" >stdout
grep 'transitions: 887$' stdout grep 'transitions: 887$' stdout
grep 'states: 49$' stdout grep 'states: 49$' stdout
run 0 ../ltl2tgba -TGTA -Rm -ks "$g" >stdout run 0 ../ltl2tgba -TGTA -RT -ks "$g" >stdout
grep 'transitions: 935$' stdout grep 'transitions: 935$' stdout
grep 'states: 49$' stdout grep 'states: 49$' stdout

47
src/tgbatest/ltl2tgba.cc
View file

@ -216,7 +216,20 @@ syntax(char* prog)
<< "in BFS order" << std::endl << "in BFS order" << std::endl
<< std::endl << std::endl
<< "Options for performing emptiness checks:" << std::endl << "Conversion to Testing Automaton:" << std::endl
<< " -TA output a Generalized Testing Automaton (GTA),\n"
<< " or a Testing Automaton (TA) with -DS\n"
<< " -lv add an artificial livelock state to obtain a "
<< "Single-pass (G)TA\n"
<< " -sp convert into a single-pass (G)TA without artificial "
<< "livelock state\n"
<< " -in do not use an artificial initial state\n"
<< " -TGTA output a Transition-based Generalized TA"
<< std::endl
<< " -RT reduce the (G)TA/TGTA using bisimulation.\n"
<< std::endl
<< "Options for performing emptiness checks (on TGBA):" << std::endl
<< " -e[ALGO] run emptiness check, expect and compute an " << " -e[ALGO] run emptiness check, expect and compute an "
<< "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"
@ -279,26 +292,7 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -v display the BDD variables used by the automaton" << " -v display the BDD variables used by the automaton"
<< std::endl << std::endl
<< std::endl << std::endl;
<< "Options for Testing Automata:"
<< std::endl
<< " -TA Translate an LTL formula into a GTA (Generalized"
<< " Testing automata), for Testing Automata (TA) add '-DS' option"
<< std::endl
<< " -lv convert into a (G)TA with an artificial livelock state,"
<< " the obtained automaton is called S(G)TA "
<< "(Single-pass (Generalized) Testing Automata)"
<< std::endl
<< " -sp convert into a (G)TA involving a single-pass emptiness "
<< "check (without adding an artificial livelock state)"
<< std::endl
<< std::endl
<< " -in convert into a (G)TA without an artificial initial state"
<< std::endl
<< " -TGTA Translate an LTL formula into a TGTA "
<< "(Transition-based Generalised Testing Automata)"
<< std::endl;
exit(2); exit(2);
} }
@ -343,6 +337,7 @@ main(int argc, char** argv)
bool graph_run_tgba_opt = false; bool graph_run_tgba_opt = false;
bool opt_reduce = false; bool opt_reduce = false;
bool opt_minimize = false; bool opt_minimize = false;
bool opt_bisim_ta = false;
bool opt_monitor = false; bool opt_monitor = false;
bool containment = false; bool containment = false;
bool show_fc = false; bool show_fc = false;
@ -671,6 +666,10 @@ main(int argc, char** argv)
{ {
opt_minimize = true; opt_minimize = true;
} }
else if (!strcmp(argv[formula_index], "-RT"))
{
opt_bisim_ta = true;
}
else if (!strcmp(argv[formula_index], "-M")) else if (!strcmp(argv[formula_index], "-M"))
{ {
opt_monitor = true; opt_monitor = true;
@ -1006,7 +1005,7 @@ main(int argc, char** argv)
const spot::tgba* degeneralized = 0; const spot::tgba* degeneralized = 0;
spot::tgba* minimized = 0; spot::tgba* minimized = 0;
if (opt_minimize && !ta_opt && !tgta_opt) if (opt_minimize)
{ {
tm.start("obligation minimization"); tm.start("obligation minimization");
minimized = minimize_obligation(a, f); minimized = minimize_obligation(a, f);
@ -1125,7 +1124,7 @@ main(int argc, char** argv)
opt_with_artificial_livelock); opt_with_artificial_livelock);
spot::ta* testing_automata_nm = 0; spot::ta* testing_automata_nm = 0;
if (opt_minimize) if (opt_bisim_ta)
{ {
testing_automata_nm = testing_automata; testing_automata_nm = testing_automata;
testing_automata = minimize_ta(testing_automata); testing_automata = minimize_ta(testing_automata);
@ -1159,7 +1158,7 @@ main(int argc, char** argv)
if (tgta_opt) if (tgta_opt)
{ {
spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd); spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd);
if (opt_minimize) if (opt_bisim_ta)
{ {
a = minimize_tgta(tgta); a = minimize_tgta(tgta);
minimized = a; minimized = a;