From 20c7f1e8cf3886753c0524b41189798c0b81f9c1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Jun 2012 13:35:12 +0200 Subject: [PATCH] Don't use -Rm for two different things. * src/tgbatest/ltl2tgba.cc: Introduce -RT to turn on bisimulation on TA instead of hijacking -Rm. * src/tgbatest/ltl2ta.test: Adjust. --- src/tgbatest/ltl2ta.test | 54 ++++++++++++++++++++-------------------- src/tgbatest/ltl2tgba.cc | 47 +++++++++++++++++----------------- 2 files changed, 50 insertions(+), 51 deletions(-) diff --git a/src/tgbatest/ltl2ta.test b/src/tgbatest/ltl2ta.test index 516f62a6a..57a025c10 100755 --- a/src/tgbatest/ltl2ta.test +++ b/src/tgbatest/ltl2ta.test @@ -27,21 +27,21 @@ set -e check () { 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 -sp -ks "$1" - run 0 ../ltl2tgba -TA -Rm -lv "$1" - run 0 ../ltl2tgba -TA -Rm -sp -ks "$1" + run 0 ../ltl2tgba -TA -RT -lv "$1" + run 0 ../ltl2tgba -TA -RT -sp -ks "$1" run 0 ../ltl2tgba -TA -lv -sp -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 -sp -DS -ks "$1" - run 0 ../ltl2tgba -TA -Rm -sp -DS -ks "$1" - run 0 ../ltl2tgba -TA -Rm -lv -DS -ks "$1" - run 0 ../ltl2tgba -TA -Rm -sp -lv -DS -ks "$1" + run 0 ../ltl2tgba -TA -RT -sp -DS -ks "$1" + run 0 ../ltl2tgba -TA -RT -lv -DS -ks "$1" + run 0 ../ltl2tgba -TA -RT -sp -lv -DS -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 @@ -71,7 +71,7 @@ done 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 'states: 10$' stdout done @@ -79,14 +79,14 @@ done 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 'states: 5$' stdout done 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 'states: 6$' stdout done @@ -100,9 +100,9 @@ f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' grep 'transitions: 96$' 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. -../ltl2tgba -ks -TA -Rm -DS "$f" > stdout +../ltl2tgba -ks -TA -RT -DS "$f" > stdout grep 'transitions: 89$' stdout grep 'states: 20$' stdout @@ -114,7 +114,7 @@ grep 'states: 449$' stdout 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 '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 '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 '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 'states: 21$' stdout 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 '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 'states: 40$' stdout -run 0 ../ltl2tgba -TA -Rm -ks "$f" >stdout +run 0 ../ltl2tgba -TA -RT -ks "$f" >stdout grep 'transitions: 424$' 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 '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 '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 'states: 38$' stdout @@ -168,25 +168,25 @@ grep 'transitions: 609$' 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 'states: 33$' stdout -run 0 ../ltl2tgba -TGTA -Rm -ks "$f" >stdout +run 0 ../ltl2tgba -TGTA -RT -ks "$f" >stdout grep 'transitions: 527$' stdout grep 'states: 32$' stdout 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 '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 'states: 49$' stdout -run 0 ../ltl2tgba -TGTA -Rm -ks "$g" >stdout +run 0 ../ltl2tgba -TGTA -RT -ks "$g" >stdout grep 'transitions: 935$' stdout grep 'states: 49$' stdout diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 401ad6f1d..2a3664c77 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -216,7 +216,20 @@ syntax(char* prog) << "in BFS order" << 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 " << "accepting run" << std::endl << " -E[ALGO] run emptiness check, expect no accepting run" @@ -279,26 +292,7 @@ syntax(char* prog) << std::endl << " -v display the BDD variables used by the automaton" << 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; - + << std::endl; exit(2); } @@ -343,6 +337,7 @@ main(int argc, char** argv) bool graph_run_tgba_opt = false; bool opt_reduce = false; bool opt_minimize = false; + bool opt_bisim_ta = false; bool opt_monitor = false; bool containment = false; bool show_fc = false; @@ -671,6 +666,10 @@ main(int argc, char** argv) { opt_minimize = true; } + else if (!strcmp(argv[formula_index], "-RT")) + { + opt_bisim_ta = true; + } else if (!strcmp(argv[formula_index], "-M")) { opt_monitor = true; @@ -1006,7 +1005,7 @@ main(int argc, char** argv) const spot::tgba* degeneralized = 0; spot::tgba* minimized = 0; - if (opt_minimize && !ta_opt && !tgta_opt) + if (opt_minimize) { tm.start("obligation minimization"); minimized = minimize_obligation(a, f); @@ -1125,7 +1124,7 @@ main(int argc, char** argv) opt_with_artificial_livelock); spot::ta* testing_automata_nm = 0; - if (opt_minimize) + if (opt_bisim_ta) { testing_automata_nm = testing_automata; testing_automata = minimize_ta(testing_automata); @@ -1159,7 +1158,7 @@ main(int argc, char** argv) if (tgta_opt) { spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd); - if (opt_minimize) + if (opt_bisim_ta) { a = minimize_tgta(tgta); minimized = a;