diff --git a/bench/emptchk/README b/bench/emptchk/README index 4ffd68ee3..03282890f 100644 --- a/bench/emptchk/README +++ b/bench/emptchk/README @@ -276,4 +276,4 @@ This directory contains: http://spot.lip6.fr/wiki/EmptinessCheckOptions) Besides randtgba, two other tools that you might find handy we - experimenting are src/bin/randltl and src/tgbatest/ltl2tgba. + experimenting are src/bin/randltl and src/tests/ikwiad. diff --git a/bench/emptchk/defs.in b/bench/emptchk/defs.in index d7275f2c6..2a3adcc12 100644 --- a/bench/emptchk/defs.in +++ b/bench/emptchk/defs.in @@ -33,6 +33,6 @@ test -f "$srcdir/defs.in" || { } RANDTGBA='@top_builddir@/src/tgbatest/randtgba@EXEEXT@' -LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@' +LTL2TGBA='@top_builddir@/src/tests/ikwiad@EXEEXT@' FORMULAE=$srcdir/formulae.ltl ALGORITHMS=$srcdir/algorithms diff --git a/bench/ltlclasses/run b/bench/ltlclasses/run index d4c979b62..5843581b4 100755 --- a/bench/ltlclasses/run +++ b/bench/ltlclasses/run @@ -19,7 +19,7 @@ # along with this program. If not, see . gen=../../src/bin/genltl -LTL2TGBA=../../src/tgbatest/ltl2tgba +LTL2TGBA=../../src/tests/ikwiad for F in alpha beta beta-prime phi xi; do echo "# Benching ltl2tgba_fm for family ccj-$F" diff --git a/bench/ltlcounter/run b/bench/ltlcounter/run index 6124f2d12..195b24689 100755 --- a/bench/ltlcounter/run +++ b/bench/ltlcounter/run @@ -19,7 +19,7 @@ # along with this program. If not, see . gen=../../src/bin/genltl -LTL2TGBA=../../src/tgbatest/ltl2tgba +LTL2TGBA=../../src/tests/ikwiad echo "# Benching ltl2tgba_fm..." echo "# the following values are also saved to file 'results.fm'" diff --git a/bench/wdba/run b/bench/wdba/run index 6ced198d8..b00e2c91b 100755 --- a/bench/wdba/run +++ b/bench/wdba/run @@ -61,7 +61,7 @@ Fr->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r G((q&Fr)->(p->(!r U (s&!r&!z&X((!r&!z) U t)))) U r) EOF -LTL2TGBA=../../src/tgbatest/ltl2tgba +LTL2TGBA=../../src/tests/ikwiad ( line=0 diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index b8bedfc51..bf8fdba51 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -26,7 +26,7 @@ LDADD = ../libspot.la # These are the most used test programs, and they are also useful # to run manually outside the test suite. Always build them. -noinst_PROGRAMS = ltl2tgba randtgba +noinst_PROGRAMS = ikwiad randtgba check_SCRIPTS = defs # Keep this sorted alphabetically. @@ -73,9 +73,9 @@ checkta_SOURCES = checkta.cc complement_SOURCES = complementation.cc emptchk_SOURCES = emptchk.cc graph_SOURCES = graph.cc +ikwiad_SOURCES = ikwiad.cc intvcomp_SOURCES = intvcomp.cc intvcmp2_SOURCES = intvcmp2.cc -ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc ngraph_SOURCES = ngraph.cc parse_print_SOURCES = parse_print_test.cc diff --git a/src/tests/babiak.test b/src/tests/babiak.test index 32dbfe87f..5b1413f8a 100755 --- a/src/tests/babiak.test +++ b/src/tests/babiak.test @@ -39,7 +39,7 @@ X((X(!p1 V F!p6)V F!p4)U p2)&(F(G((0 U(F p6))U((p1 U(G(p4 U F p0)))U X p7)))) (G(G(((F p5)U((((F!p1)V(p2 &!p4))|!p2)|((X!p7 U!p4)V(F(F((G p2)&p5))))))U p6))) EOF -ltl2tgba=../ltl2tgba +ltl2tgba=../ikwiad ../../bin/ltlcross %T" \ diff --git a/src/tests/checkta.cc b/src/tests/checkta.cc index 8db85bd37..5b13ad4e8 100644 --- a/src/tests/checkta.cc +++ b/src/tests/checkta.cc @@ -95,8 +95,8 @@ main(int argc, char** argv) auto a = ltl_to_tgba_fm(f, d); bdd ap_set = atomic_prop_collect_as_bdd(f, a); - // run 0 ../ltl2tgba -TGTA -ks "$1" - // run 0 ../ltl2tgba -TGTA -RT -ks "$1" + // run 0 ../ikwiad -TGTA -ks "$1" + // run 0 ../ikwiad -TGTA -RT -ks "$1" { auto t = spot::tgba_to_tgta(a, ap_set); stats("-TGTA", t); @@ -104,8 +104,8 @@ main(int argc, char** argv) } { - // run 0 ../ltl2tgba -TA -ks "$1" - // run 0 ../ltl2tgba -TA -RT -ks "$1" + // run 0 ../ikwiad -TA -ks "$1" + // run 0 ../ikwiad -TA -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, false, // degen (-DS) false, // artificial_initial_state (-in) @@ -116,8 +116,8 @@ main(int argc, char** argv) } { - // run 0 ../ltl2tgba -TA -lv -ks "$1" - // run 0 ../ltl2tgba -TA -lv -RT -ks "$1" + // run 0 ../ikwiad -TA -lv -ks "$1" + // run 0 ../ikwiad -TA -lv -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, false, // degen (-DS) false, // artificial_initial_state (-in) @@ -128,8 +128,8 @@ main(int argc, char** argv) } { - // run 0 ../ltl2tgba -TA -sp -ks "$1" - // run 0 ../ltl2tgba -TA -sp -RT -ks "$1" + // run 0 ../ikwiad -TA -sp -ks "$1" + // run 0 ../ikwiad -TA -sp -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, false, // degen (-DS) false, // artificial_initial_state (-in) @@ -140,8 +140,8 @@ main(int argc, char** argv) } { - // run 0 ../ltl2tgba -TA -lv -sp -ks "$1" - // run 0 ../ltl2tgba -TA -lv -sp -RT -ks "$1" + // run 0 ../ikwiad -TA -lv -sp -ks "$1" + // run 0 ../ikwiad -TA -lv -sp -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, false, // degen (-DS) false, // artificial_initial_state (-in) @@ -154,8 +154,8 @@ main(int argc, char** argv) a = spot::degeneralize(a); { - // run 0 ../ltl2tgba -TA -DS -ks "$1" - // run 0 ../ltl2tgba -TA -DS -RT -ks "$1" + // run 0 ../ikwiad -TA -DS -ks "$1" + // run 0 ../ikwiad -TA -DS -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, true, // degen (-DS) false, // artificial_initial_state (-in) @@ -166,8 +166,8 @@ main(int argc, char** argv) } { - // run 0 ../ltl2tgba -TA -DS -lv -ks "$1" - // run 0 ../ltl2tgba -TA -DS -lv -RT -ks "$1" + // run 0 ../ikwiad -TA -DS -lv -ks "$1" + // run 0 ../ikwiad -TA -DS -lv -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, true, // degen (-DS) false, // artificial_initial_state (-in) @@ -178,8 +178,8 @@ main(int argc, char** argv) } { - // run 0 ../ltl2tgba -TA -DS -sp -ks "$1" - // run 0 ../ltl2tgba -TA -DS -sp -RT -ks "$1" + // run 0 ../ikwiad -TA -DS -sp -ks "$1" + // run 0 ../ikwiad -TA -DS -sp -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, true, // degen (-DS) false, // artificial_initial_state (-in) @@ -190,8 +190,8 @@ main(int argc, char** argv) } { - // run 0 ../ltl2tgba -TA -DS -lv -sp -ks "$1" - // run 0 ../ltl2tgba -TA -DS -lv -sp -RT -ks "$1" + // run 0 ../ikwiad -TA -DS -lv -sp -ks "$1" + // run 0 ../ikwiad -TA -DS -lv -sp -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, true, // degen (-DS) false, // artificial_initial_state (-in) @@ -207,8 +207,8 @@ main(int argc, char** argv) bdd ap_set = atomic_prop_collect_as_bdd(f, a); { - // run 0 ../ltl2tgba -x -R3 -DS -TA -in -ks "$1" - // run 0 ../ltl2tgba -x -R3 -DS -TA -in -RT -ks "$1" + // run 0 ../ikwiad -x -R3 -DS -TA -in -ks "$1" + // run 0 ../ikwiad -x -R3 -DS -TA -in -RT -ks "$1" auto t = spot::tgba_to_ta(a, ap_set, true, // degen (-DS) false, // artificial_initial_state (-in) diff --git a/src/tests/complementation.test b/src/tests/complementation.test index 57438716d..201a4d440 100755 --- a/src/tests/complementation.test +++ b/src/tests/complementation.test @@ -60,10 +60,10 @@ State: 2 --END-- EOF # x.tgba accepts some run -run 0 ../ltl2tgba -XH -e x.hoa +run 0 ../ikwiad -XH -e x.hoa # so does its complement run 0 ../complement -H -a x.hoa > nx.hoa -run 0 ../ltl2tgba -XH -e nx.hoa +run 0 ../ikwiad -XH -e nx.hoa # however the intersection of both should not # accept any run. run 1 ../../bin/autfilt -q nx.hoa --intersect x.hoa diff --git a/src/tests/cycles.test b/src/tests/cycles.test index 99f8caa43..dbaee144e 100755 --- a/src/tests/cycles.test +++ b/src/tests/cycles.test @@ -66,9 +66,9 @@ State: 11 --END-- EOF -run 0 ../ltl2tgba -KC -XH johnson-fig1.hoa > out +run 0 ../ikwiad -KC -XH johnson-fig1.hoa > out test `wc -l < out` -eq 10 -run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out +run 0 ../ikwiad -KW '(Ga -> Gb) W c' > out test `grep 'is weak' out | wc -l` -eq 4 test `grep 'is not weak' out | wc -l` -eq 1 diff --git a/src/tests/dbacomp.test b/src/tests/dbacomp.test index e4e0b0f72..e5d1b1dbc 100755 --- a/src/tests/dbacomp.test +++ b/src/tests/dbacomp.test @@ -55,5 +55,5 @@ State: 2 EOF # Check emptiness of product with complement. -run 0 ../ltl2tgba -H -DC -C -XH input.hoa > output.hoa +run 0 ../ikwiad -H -DC -C -XH input.hoa > output.hoa run 1 ../../bin/autfilt -q input.hoa --intersect output.hoa diff --git a/src/tests/degendet.test b/src/tests/degendet.test index aa5acfea8..89c1dfa32 100755 --- a/src/tests/degendet.test +++ b/src/tests/degendet.test @@ -30,9 +30,9 @@ set -e # Make sure all these runs output the same automaton. # With valgrind -run 0 ../ltl2tgba -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out1 +run 0 ../ikwiad -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out1 # Without valgrind for i in 2 3 4 5; do - ../ltl2tgba -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out + ../ikwiad -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out cmp out out1 || exit 1 done diff --git a/src/tests/degenid.test b/src/tests/degenid.test index 91c3af5a7..e6dd9e7b9 100755 --- a/src/tests/degenid.test +++ b/src/tests/degenid.test @@ -26,12 +26,12 @@ set -e for f in 'FGa|GFb' 'GFa & GFb & GFc' 'GF(a->FGb)&GF(c->FGd)'; do for opt in -DS -DT; do - ../ltl2tgba $opt -H "$f" > autX.spot - ../ltl2tgba -XH -kt autX.spot > base.size + ../ikwiad $opt -H "$f" > autX.spot + ../ikwiad -XH -kt autX.spot > base.size cat base.size for x in X XX XXX; do - ../ltl2tgba -XH $opt -H aut$x.spot > autX$x.spot - ../ltl2tgba -XH -kt autX$x.spot > new.size + ../ikwiad -XH $opt -H aut$x.spot > autX$x.spot + ../ikwiad -XH -kt autX$x.spot > new.size cat new.size cmp base.size new.size done @@ -78,7 +78,7 @@ State: 5 --END-- EOF -run 0 ../ltl2tgba -ks -XH -DS bug > out +run 0 ../ikwiad -ks -XH -DS bug > out grep 'states: 6' out @@ -126,7 +126,7 @@ State: 7 --END-- EOF -run 0 ../ltl2tgba -ks -XH -DS bug2 >out +run 0 ../ikwiad -ks -XH -DS bug2 >out grep 'states: 8' out diff --git a/src/tests/det.test b/src/tests/det.test index 8b5bff541..37799fb87 100755 --- a/src/tests/det.test +++ b/src/tests/det.test @@ -110,11 +110,11 @@ State: 4 {0} --END-- EOF -run 0 ../ltl2tgba -H -DC -XH in.hoa > out.hoa +run 0 ../ikwiad -H -DC -XH in.hoa > out.hoa run 1 ../../bin/autfilt -q --are-isomorph in.hoa out.hoa run 0 ../../bin/autfilt -q --are-isomorph ex.hoa out.hoa -run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba +run 0 ../ikwiad -x -DC 'GFa & XGFb' > out.tgba cat >ex.tgba <s2->s3->(large composant from s4 to s9) # ^ || @@ -164,8 +164,8 @@ State: 8 --END-- EOF -run 0 ../ltl2tgba -CR -eSE05 -XH blue_last -run 0 ../ltl2tgba -CR -eTau03_opt -XH blue_last +run 0 ../ikwiad -CR -eSE05 -XH blue_last +run 0 ../ikwiad -CR -eTau03_opt -XH blue_last # _______ # | | @@ -237,7 +237,7 @@ State: 8 --END-- EOF -run 0 ../ltl2tgba -CR -eSE05 -XH red -run 0 ../ltl2tgba -CR -eTau03_opt -XH red +run 0 ../ikwiad -CR -eSE05 -XH red +run 0 ../ikwiad -CR -eTau03_opt -XH red rm -f red blue_counter blue_last diff --git a/src/tests/dstar.test b/src/tests/dstar.test index 1fdc3f9b3..f1fc8ff71 100755 --- a/src/tests/dstar.test +++ b/src/tests/dstar.test @@ -56,7 +56,7 @@ Acc-Sig: +0 2 EOF -run 0 ../ltl2tgba -XD dra.dstar | tee stdout +run 0 ../ikwiad -XD dra.dstar | tee stdout cat >expected <expected <expected <expected <output1 - run 0 ../ltl2tgba -f -S "$1" >output2 + run 0 ../ikwiad -f -s "$1" >output1 + run 0 ../ikwiad -f -S "$1" >output2 test `wc -l input <<'EOF' diff --git a/src/tests/ltl2tgba.cc b/src/tests/ikwiad.cc similarity index 100% rename from src/tests/ltl2tgba.cc rename to src/tests/ikwiad.cc diff --git a/src/tests/kv.test b/src/tests/kv.test index 80e3655e7..c72abc7af 100755 --- a/src/tests/kv.test +++ b/src/tests/kv.test @@ -25,7 +25,7 @@ set -e check () { - run 0 ../ltl2tgba -f -KV "$1" > out.dot + run 0 ../ikwiad -f -KV "$1" > out.dot test -z "$DOT" || "$DOT" out.dot > /dev/null rm -f out.dot } @@ -46,7 +46,7 @@ check '"G1"U"GG" && "FF"' # even after iterated simulation # Report from Etienne Renault. -../ltl2tgba -KV -R3 -RIS >out \ +../ikwiad -KV -R3 -RIS >out \ 'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"' x=`sed -n '/APrec/{ s/.*APrec=\[\([^]]*\)\].*/\1/p diff --git a/src/tests/ltl2neverclaim-lbtt.test b/src/tests/ltl2neverclaim-lbtt.test index eee0453c7..7b773e5af 100755 --- a/src/tests/ltl2neverclaim-lbtt.test +++ b/src/tests/ltl2neverclaim-lbtt.test @@ -35,7 +35,7 @@ Algorithm { Name = "Spot (Couvreur -- FM)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t'" + Parameters = "--spot '../ikwiad -F -f -t'" Enabled = yes } @@ -43,7 +43,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), with reductions" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r4 -R3f -F -f -t'" + Parameters = "--spot '../ikwiad -r4 -R3f -F -f -t'" Enabled = no } @@ -51,7 +51,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), degeneralized via never claim" Path = "${LBTT_TRANSLATE}" - Parameters = "--spin '../ltl2tgba -F -f -N'" + Parameters = "--spin '../ikwiad -F -f -N'" Enabled = yes } @@ -59,7 +59,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), reductions, degeneralized via never claim" Path = "${LBTT_TRANSLATE}" - Parameters = "--spin '../ltl2tgba -F -f -r4 -R3 -N'" + Parameters = "--spin '../ikwiad -F -f -r4 -R3 -N'" Enabled = yes } diff --git a/src/tests/ltl2neverclaim.test b/src/tests/ltl2neverclaim.test index 2d7c5f6e3..c12e95aa6 100755 --- a/src/tests/ltl2neverclaim.test +++ b/src/tests/ltl2neverclaim.test @@ -25,7 +25,7 @@ . ./defs set -e -ltl2tgba=../ltl2tgba +ltl2tgba=../ikwiad ../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 | ../../bin/ltlcross \ diff --git a/src/tests/ltl2tgba.test b/src/tests/ltl2tgba.test index 72e6f18e5..08fe5caca 100755 --- a/src/tests/ltl2tgba.test +++ b/src/tests/ltl2tgba.test @@ -103,12 +103,12 @@ test 1 -eq `../../bin/ltl2tgba -B false --stats %a` # In particular, Spot 0.9 would incorrectly reject the sequence: # (a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);... in 'G!{(b;1)*;a}' # This means the following automaton was incorrectly empty in Spot 0.9. -run 0 ../ltl2tgba -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))' +run 0 ../ikwiad -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))' # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization. for opt in '' -DT -DS; do - ../ltl2tgba -ks -f -R3 $opt 'a U (b U c)' > stdout + ../ikwiad -ks -f -R3 $opt 'a U (b U c)' > stdout grep 'transitions: 6$' stdout grep 'states: 3$' stdout done @@ -116,7 +116,7 @@ done # Make sure '!(Ga U b)' has 3 states and 6 transitions, # before and after degeneralization. for opt in '' -DT -DS; do - ../ltl2tgba -kt -f -R3 $opt '!(Ga U b)' > stdout + ../ikwiad -kt -f -R3 $opt '!(Ga U b)' > stdout grep 'sub trans.: 11$' stdout grep 'transitions: 6$' stdout grep 'states: 3$' stdout @@ -125,7 +125,7 @@ done # Make sure 'Ga U b' has 4 states and 6 transitions, # before and after degeneralization. for opt in '' -DT -DS; do - ../ltl2tgba -kt -f -R3 $opt 'Ga U b' > stdout + ../ikwiad -kt -f -R3 $opt 'Ga U b' > stdout grep 'sub trans.: 12$' stdout grep 'transitions: 6$' stdout grep 'states: 4$' stdout @@ -135,10 +135,10 @@ done # has 6 states and 15 transitions, before and after degeneralization. f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))' for opt in '' -DT -DS; do - ../ltl2tgba -ks -f -R3 $opt "$f" > stdout + ../ikwiad -ks -f -R3 $opt "$f" > stdout grep 'transitions: 15$' stdout grep 'states: 6$' stdout - ../ltl2tgba -ks -f -R3f $opt "$f" > stdout + ../ikwiad -ks -f -R3f $opt "$f" > stdout grep 'transitions: 15$' stdout grep 'states: 6$' stdout done @@ -146,21 +146,21 @@ done # Make sure 'GFa & GFb & GFc & GFd & GFe & GFf' # has 7 states and 34 transitions after degeneralization. f='GFa & GFb & GFc & GFd & GFe & GFg' -../ltl2tgba -ks -DS -x -f "$f" > stdout +../ikwiad -ks -DS -x -f "$f" > stdout grep 'transitions: 34$' stdout grep 'states: 7$' stdout # Make sure 'Ga & XXXX!a' is minimized to one state. f='Ga & XXXX!a' -../ltl2tgba -ks -f "$f" > stdout +../ikwiad -ks -f "$f" > stdout grep 'transitions: 4$' stdout grep 'states: 5$' stdout -../ltl2tgba -ks -Rm -f "$f" > stdout +../ikwiad -ks -Rm -f "$f" > stdout grep 'transitions: 0$' stdout grep 'states: 1$' stdout # Make sure a monitor for F(a & F(b)) accepts everything. -run 0 ../ltl2tgba -M -f "F(a & F(b))" | grep ' ->' > stdout +run 0 ../ikwiad -M -f "F(a & F(b))" | grep ' ->' > stdout cat >expected < 0 0 -> 0 [label="1"] @@ -168,12 +168,12 @@ EOF cmp stdout expected # This formula caused a segfault with Spot 0.7. -run 0 ../ltl2tgba -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout +run 0 ../ikwiad -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout grep 'transitions: 5$' stdout grep 'states: 3$' stdout # Adding -R3 used to make it work... -run 0 ../ltl2tgba -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout +run 0 ../ikwiad -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout grep 'transitions: 5$' stdout grep 'states: 3$' stdout @@ -181,14 +181,14 @@ grep 'states: 3$' stdout # output as a never claim or are a degeneralized BA in HOAF. # The option -R1q -R1t used to cause two degeneralizations to # occur. -run 0 ../ltl2tgba -R1q -R1t -N 'FGa|FGb' > out.never -run 0 ../ltl2tgba -XN -kt out.never > count.never -run 0 ../ltl2tgba -R1q -R1t -DS -H 'FGa|FGb' > out.hoa -run 0 ../ltl2tgba -XH -kt out.hoa > count.hoa +run 0 ../ikwiad -R1q -R1t -N 'FGa|FGb' > out.never +run 0 ../ikwiad -XN -kt out.never > count.never +run 0 ../ikwiad -R1q -R1t -DS -H 'FGa|FGb' > out.hoa +run 0 ../ikwiad -XH -kt out.hoa > count.hoa cmp count.never count.hoa # The following automaton should have only 4 states. -run 0 ../ltl2tgba -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout +run 0 ../ikwiad -R3 -ks -f '(p&XF!p)|(!p&XFp)|X(Fp&F!p)' >stdout grep 'transitions: 7$' stdout grep 'states: 4$' stdout diff --git a/src/tests/ltlcounter.test b/src/tests/ltlcounter.test index eea3d8318..47e178616 100755 --- a/src/tests/ltlcounter.test +++ b/src/tests/ltlcounter.test @@ -31,10 +31,10 @@ run='run 0' check_formula() { # First, check the satisfiability of the formula with Spot - $run ../ltl2tgba -CR -e -x -f "$1" >/dev/null + $run ../ikwiad -CR -e -x -f "$1" >/dev/null # Also check the satisfiability of the degeneralized formula - $run ../ltl2tgba -CR -e -DT -x -f "$1" >/dev/null - $run ../ltl2tgba -CR -e -DS -x -f "$1" >/dev/null + $run ../ikwiad -CR -e -DT -x -f "$1" >/dev/null + $run ../ikwiad -CR -e -DS -x -f "$1" >/dev/null } # Kristin Y. Rozier reported that the formulae with n=10 were badly diff --git a/src/tests/ltlcross.test b/src/tests/ltlcross.test index bccf485de..3fcc57572 100755 --- a/src/tests/ltlcross.test +++ b/src/tests/ltlcross.test @@ -21,7 +21,7 @@ . ./defs set -e -ltl2tgba=../ltl2tgba +ltl2tgba=../ikwiad ( diff --git a/src/tests/neverclaimread.test b/src/tests/neverclaimread.test index 885a2b468..87f607474 100755 --- a/src/tests/neverclaimread.test +++ b/src/tests/neverclaimread.test @@ -44,7 +44,7 @@ skip } EOF -run 0 ../ltl2tgba -XN -H input > stdout +run 0 ../ikwiad -XN -H input > stdout cat >expected < stdout +run 0 ../ikwiad -XN -H input > stdout cat >expected < stdout +run 0 ../ikwiad -XN input > stdout cat >expected < stdout 2>stderr +run 2 ../ikwiad -XN input > stdout 2>stderr cat >expected <<\EOF input:9.16: syntax error, unexpected ')', expecting fi or ':' EOF @@ -209,7 +209,7 @@ transitions: 6 states: 4 EOF -run 0 ../ltl2tgba -ks -XN input > output +run 0 ../ikwiad -ks -XN input > output diff output expected @@ -285,7 +285,7 @@ T2_S4: } EOF -run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr +run 2 ../ikwiad -ks -XN input > stdout 2>stderr cat stderr cat >expected-err <<\EOF input:48.1-10: redefinition of accept_S10... @@ -296,7 +296,7 @@ diff stderrfilt expected-err # DOS-style new lines should have the same output. perl -pi -e 's/$/\r/' input -run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr +run 2 ../ikwiad -ks -XN input > stdout 2>stderr cat stderr grep input: stderr > stderrfilt diff stderrfilt expected-err diff --git a/src/tests/obligation.test b/src/tests/obligation.test index ad7cb614a..410e8b91a 100755 --- a/src/tests/obligation.test +++ b/src/tests/obligation.test @@ -98,8 +98,8 @@ grok() success=: while read exp f; do - x=`../ltl2tgba -O "$f"` - y=`../ltl2tgba -O "!($f)"` + x=`../ikwiad -O "$f"` + y=`../ikwiad -O "!($f)"` resx=`grok "$x"` resy=`grok "$y"` echo "$resx $f" diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test index f9d39d818..ecc1a3270 100755 --- a/src/tests/parseaut.test +++ b/src/tests/parseaut.test @@ -1054,7 +1054,7 @@ expecterr non-existant<output.err +run 2 ../ikwiad -XH foob 2>output.err grep 'foob:1.1: Cannot open file foob' output.err # Make sure we can read multiple automata from stdin @@ -1081,7 +1081,7 @@ State: 1 --END-- EOF -run 0 ../ltl2tgba -d -XH input 2> output.err +run 0 ../ikwiad -d -XH input 2> output.err grep -- "--BODY--" output.err grep "identifier.*v1" output.err diff --git a/src/tests/randaut.test b/src/tests/randaut.test index 343fa04ca..b745ba7aa 100755 --- a/src/tests/randaut.test +++ b/src/tests/randaut.test @@ -25,7 +25,7 @@ set -e randaut=../../bin/randaut autfilt=../../bin/autfilt -$randaut --spin -Q4 a b | ../ltl2tgba -H -XN - >out +$randaut --spin -Q4 a b | ../ikwiad -H -XN - >out grep 'States: 4' out grep 'AP: 2' out grep 'state-acc' out diff --git a/src/tests/randpsl.test b/src/tests/randpsl.test index 916a684e9..24260ecf2 100755 --- a/src/tests/randpsl.test +++ b/src/tests/randpsl.test @@ -28,7 +28,7 @@ set -e ../../bin/randltl -n -1 --tree-size 30 --seed 12 --psl a b c | ../../bin/ltlfilt -r --size-min 12 --unique | ../../bin/ltlfilt -v --ltl -n 50 | tee formulas | -../../bin/ltlcross '../ltl2tgba -R3 -t %f >%T' '../ltl2tgba -x -R3 -t %f >%T' \ +../../bin/ltlcross '../ikwiad -R3 -t %f >%T' '../ikwiad -x -R3 -t %f >%T' \ -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}' test `wc -l < formulas` = 50 diff --git a/src/tests/renault.test b/src/tests/renault.test index 03df482c5..3fa907173 100755 --- a/src/tests/renault.test +++ b/src/tests/renault.test @@ -69,6 +69,6 @@ transitions: 12 states: 6 EOF -run 0 ../ltl2tgba -XH -ks -RDS file > out +run 0 ../ikwiad -XH -ks -RDS file > out cmp out outexp diff --git a/src/tests/satmin2.test b/src/tests/satmin2.test index a4b5cb0bc..451bbd694 100755 --- a/src/tests/satmin2.test +++ b/src/tests/satmin2.test @@ -57,7 +57,7 @@ states: 1 nondeterministic states: 0 EOF -../ltl2tgba -RS1 -kt -XH input.hoa > output +../ikwiad -RS1 -kt -XH input.hoa > output diff output expected # At some point, this formula was correctly minimized, but diff --git a/src/tests/sccsimpl.test b/src/tests/sccsimpl.test index f9421f79f..fc51e2966 100755 --- a/src/tests/sccsimpl.test +++ b/src/tests/sccsimpl.test @@ -66,7 +66,7 @@ State: 3 --END-- EOF -run 0 ../ltl2tgba -XH -R3 -H aut.txt > out.txt +run 0 ../ikwiad -XH -R3 -H aut.txt > out.txt grep '^Acceptance: 1 Inf(0)' out.txt @@ -87,7 +87,7 @@ State: 0 [3] 0 {2 3} --END-- EOF -run 0 ../ltl2tgba -XH -R3 -H aut2.txt > out2.txt +run 0 ../ikwiad -XH -R3 -H aut2.txt > out2.txt grep '^Acceptance: 2 ' out2.txt # only 3 transitions output, because [1] and [2] have been merged test `grep -c '\[.*\]' out2.txt` = 3 @@ -110,7 +110,7 @@ State: 0 [3] 0 {1 3} --END-- EOF -run 0 ../ltl2tgba -XH -R3 -H aut3.txt > out3.txt +run 0 ../ikwiad -XH -R3 -H aut3.txt > out3.txt grep '^Acceptance: 2 ' out3.txt # only 3 transitions output, because [0] and [1] have been merged test `grep -c '\[.*\]' out3.txt` = 3 @@ -134,7 +134,7 @@ State: 0 [4] 0 {2 3} --END-- EOF -run 0 ../ltl2tgba -XH -R3 -H aut4.txt > out4.txt +run 0 ../ikwiad -XH -R3 -H aut4.txt > out4.txt grep '^Acceptance: 4 ' out4.txt test `grep -c '\[.*\]' out4.txt` = 5 @@ -154,7 +154,7 @@ State: 0 [1 | 2] 0 --END-- EOF -run 0 ../ltl2tgba -XH -R3 -H aut5.txt > out5.txt +run 0 ../ikwiad -XH -R3 -H aut5.txt > out5.txt grep '^Acceptance: 0 t' out5.txt test `grep -c '\[.*\]' out5.txt` = 1 @@ -176,7 +176,7 @@ State: 0 [3] 0 {2 3} --END-- EOF -run 0 ../ltl2tgba -XH -R3 -H aut6.txt > out6.txt +run 0 ../ikwiad -XH -R3 -H aut6.txt > out6.txt grep '^Acceptance: 2 ' out6.txt test `grep -c '\[.*\]' out6.txt` = 2 @@ -227,16 +227,16 @@ State: 5 [1&!2 | !2&3] 5 {0 2} --END-- EOF -run 0 ../ltl2tgba -XH -R3 -H aut7.txt > out7.txt +run 0 ../ikwiad -XH -R3 -H aut7.txt > out7.txt grep '^Acceptance: 2 ' out7.txt -run 0 ../ltl2tgba -R3 -H '(GFa&GFb) | (GFc&GFd)' > out8.txt +run 0 ../ikwiad -R3 -H '(GFa&GFb) | (GFc&GFd)' > out8.txt grep 'Acceptance: 2 ' out8.txt # This formula gives a 12-state automaton in which one acceptance # condition can be removed, and after what direct simulation should # simplify the automaton to 6 states. -run 0 ../ltl2tgba -R3 -s -RDS -ks \ +run 0 ../ikwiad -R3 -s -RDS -ks \ '(G(!((b) R (a)))) R (((c) R (!(d))) U (G((a) | (!(G(e))))))' > out9.txt grep 'states: 6$' out9.txt diff --git a/src/tests/sim2.test b/src/tests/sim2.test index eacf6e112..88cc6dcb6 100755 --- a/src/tests/sim2.test +++ b/src/tests/sim2.test @@ -21,8 +21,8 @@ . ./defs set -e -../ltl2tgba -H -x -R3f -RDS '{(a&b)[*3]}<>=>G(a&!b)' > ref +../ikwiad -H -x -R3f -RDS '{(a&b)[*3]}<>=>G(a&!b)' > ref for i in -R3 -R3f '-R3 -RDS' '-R3f -RDS'; do - ../ltl2tgba -Pref -E -x $i '(X!b R F!a) U (!a | G!b)' + ../ikwiad -Pref -E -x $i '(X!b R F!a) U (!a | G!b)' done diff --git a/src/tests/simdet.test b/src/tests/simdet.test index db27431a1..9272a9416 100755 --- a/src/tests/simdet.test +++ b/src/tests/simdet.test @@ -21,16 +21,16 @@ . ./defs set -e -run 0 ../ltl2tgba -R3 -RIS \ +run 0 ../ikwiad -R3 -RIS \ 'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'\ > exp -run 0 ../ltl2tgba -R3 -RIS \ +run 0 ../ikwiad -R3 -RIS \ 'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'\ > out diff exp out -run 0 ../ltl2tgba -R3 -RIS \ +run 0 ../ikwiad -R3 -RIS \ 'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"'\ > out diff --git a/src/tests/spotlbtt.test b/src/tests/spotlbtt.test index 50ac7d28e..a3603cf05 100755 --- a/src/tests/spotlbtt.test +++ b/src/tests/spotlbtt.test @@ -34,7 +34,7 @@ Algorithm { Name = "Spot (Couvreur -- LaCIM), fake" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -T'" + Parameters = "--spot '../ikwiad -F -T'" Enabled = no } @@ -42,7 +42,7 @@ Algorithm { Name = "Spot (Couvreur -- FM)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t'" + Parameters = "--spot '../ikwiad -F -f -t'" Enabled = yes } @@ -50,7 +50,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), reduction of formula (pre reduction)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r4 -F -f -t'" + Parameters = "--spot '../ikwiad -r4 -F -f -t'" Enabled = yes } @@ -58,7 +58,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), reduction7 of formula (pre reduction)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r7 -F -f -t'" + Parameters = "--spot '../ikwiad -r7 -F -f -t'" Enabled = yes } @@ -66,7 +66,7 @@ Algorithm { Name = "Spot (Couvreur -- FM) reduction7+ru of formula (pre reduction)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r7 -ru -F -f -t'" + Parameters = "--spot '../ikwiad -r7 -ru -F -f -t'" Enabled = yes } @@ -74,7 +74,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), reduction of formula in FM" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -fr -r4 -F -f -t'" + Parameters = "--spot '../ikwiad -fr -r4 -F -f -t'" Enabled = no } @@ -82,7 +82,7 @@ Algorithm { Name = "Spot (Couvreur -- FM) reduction7 of formula in FM" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -fr -r7 -F -f -t'" + Parameters = "--spot '../ikwiad -fr -r7 -F -f -t'" Enabled = no } @@ -90,7 +90,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), post reduction with scc" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -R3 -F -f -t'" + Parameters = "--spot '../ikwiad -R3 -F -f -t'" Enabled = yes } @@ -98,7 +98,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), +pre +WDBA" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r4 -R3 -Rm -F -f -t'" + Parameters = "--spot '../ikwiad -r4 -R3 -Rm -F -f -t'" Enabled = yes } @@ -106,7 +106,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), +pre +WDBA(rejbig)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -r4 -R3 -RM -F -f -t'" + Parameters = "--spot '../ikwiad -r4 -R3 -RM -F -f -t'" Enabled = yes } @@ -114,7 +114,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), without symb_merge" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -y -t'" + Parameters = "--spot '../ikwiad -F -f -y -t'" Enabled = yes } @@ -122,7 +122,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), degeneralized" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t -DT'" + Parameters = "--spot '../ikwiad -F -f -t -DT'" Enabled = yes } @@ -130,7 +130,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), simulated" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t -RDS -r4 -R3'" + Parameters = "--spot '../ikwiad -F -f -t -RDS -r4 -R3'" Enabled = yes } @@ -138,7 +138,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), cosimulated" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t -RRS -r4 -R3'" + Parameters = "--spot '../ikwiad -F -f -t -RRS -r4 -R3'" Enabled = yes } @@ -146,7 +146,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), iterated simulation" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t -RIS -r4 -R3'" + Parameters = "--spot '../ikwiad -F -f -t -RIS -r4 -R3'" Enabled = yes } @@ -154,7 +154,7 @@ Algorithm { Name = "Spot (Couvreur -- TAA), simulated" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -taa -t -RDS -r4 -R3'" + Parameters = "--spot '../ikwiad -F -taa -t -RDS -r4 -R3'" Enabled = yes } @@ -162,7 +162,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), simulated and degeneralized on states." Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t -RDS -DS'" + Parameters = "--spot '../ikwiad -F -f -t -RDS -DS'" Enabled = yes } @@ -170,7 +170,7 @@ Algorithm { Name = "Compositional Suspension" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -u -F -f -t'" + Parameters = "--spot '../ikwiad -u -F -f -t'" Enabled = yes } @@ -178,7 +178,7 @@ Algorithm { Name = "Compositional Suspension (-r4)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -u -r4 -F -f -t'" + Parameters = "--spot '../ikwiad -u -r4 -F -f -t'" Enabled = yes } @@ -186,7 +186,7 @@ Algorithm { Name = "Compositional Suspension (-r4 -ru)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -u -r4 -ru -F -f -t'" + Parameters = "--spot '../ikwiad -u -r4 -ru -F -f -t'" Enabled = yes } @@ -194,7 +194,7 @@ Algorithm { Name = "Spot (Couvreur -- FM), degeneralized on states" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -t -DS'" + Parameters = "--spot '../ikwiad -F -f -t -DS'" Enabled = yes } @@ -202,7 +202,7 @@ Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -x -p -t'" + Parameters = "--spot '../ikwiad -F -f -x -p -t'" Enabled = yes } @@ -210,7 +210,7 @@ Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop + flapprox)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -x -p -L -t'" + Parameters = "--spot '../ikwiad -F -f -x -p -L -t'" Enabled = yes } @@ -218,7 +218,7 @@ Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop), degeneralized" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -p -x -t -DT'" + Parameters = "--spot '../ikwiad -F -f -p -x -t -DT'" Enabled = yes } @@ -226,7 +226,7 @@ Algorithm { Name = "Spot (Couvreur -- FM post_branch + exprop + flapprox), degeneralized" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -f -p -x -t -L -DT'" + Parameters = "--spot '../ikwiad -F -f -p -x -t -L -DT'" ENABLED = yes } @@ -234,7 +234,7 @@ Algorithm { Name = "Spot (Tauriainen -- TAA)" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -taa -t'" + Parameters = "--spot '../ikwiad -F -taa -t'" Enabled = yes } @@ -242,7 +242,7 @@ Algorithm { Name = "Spot (Tauriainen -- TAA) refined rules" Path = "${LBTT_TRANSLATE}" - Parameters = "--spot '../ltl2tgba -F -taa -t -c'" + Parameters = "--spot '../ikwiad -F -taa -t -c'" Enabled = yes } diff --git a/src/tests/wdba.test b/src/tests/wdba.test index d340a2183..f4ead1d25 100755 --- a/src/tests/wdba.test +++ b/src/tests/wdba.test @@ -91,13 +91,13 @@ while read f; do # detect any crash. Do that only for the first few formula, because # it takes a long time. if test $i -lt 5; then - run 0 ../ltl2tgba -f -R3 -DS -Rm "!($f)" >/dev/null + run 0 ../ikwiad -f -R3 -DS -Rm "!($f)" >/dev/null i=`expr $i + 1` fi # If the labels of the state have only digits, assume the minimization # worked. - x=`../ltl2tgba -f -Rm "!($f)" | + x=`../ikwiad -f -Rm "!($f)" | grep -v -- '->' | sed -n 's/.*label="\(..*\)".*/\1/p' | tr -d '0-9\n'` @@ -115,14 +115,14 @@ while read f; do # to detect any crash. Do that only for the first few formula, because # it takes a long time. if test $i -lt 5; then - run 0 ../ltl2tgba -taa -DS -Rm "!($f)" >/dev/null + run 0 ../ikwiad -taa -DS -Rm "!($f)" >/dev/null i=`expr $i + 1` fi # If the labels of the state have only digits, assume the minimization # worked. - ../ltl2tgba -kt -Rm "!($f)" > out1 - ../ltl2tgba -kt -R3 "!($f)" > out2 + ../ikwiad -kt -Rm "!($f)" > out1 + ../ikwiad -kt -R3 "!($f)" > out2 if cmp out1 out2; then echo "OK !($f)"; else diff --git a/src/tests/wdba2.test b/src/tests/wdba2.test index fd35fb02f..04d99ce2c 100755 --- a/src/tests/wdba2.test +++ b/src/tests/wdba2.test @@ -31,8 +31,8 @@ EOF # These two equivalent formulae used to produce # minimized automata of different sizes... -run 0 ../ltl2tgba -Rm -kt 'a | X(Gd|Fa)' > out -run 0 ../ltl2tgba -Rm -kt 'Fa | XGd' > out2 +run 0 ../ikwiad -Rm -kt 'a | X(Gd|Fa)' > out +run 0 ../ikwiad -Rm -kt 'Fa | XGd' > out2 cmp out expected cmp out2 expected