Rename src/tests/ltl2tgba as src/tests/ikwiad.
Fixes #23. * src/tests/ltl2tgba.cc: Rename as ... * src/tests/ikwiad.cc: ... this. * src/tests/Makefile.am, src/tests/babiak.test, src/tests/checkta.cc, src/tests/complementation.test, src/tests/cycles.test, src/tests/dbacomp.test, src/tests/degendet.test, src/tests/degenid.test, src/tests/det.test, src/tests/dfs.test, src/tests/dstar.test, src/tests/dupexp.test, src/tests/emptchke.test, src/tests/kv.test, src/tests/ltl2neverclaim-lbtt.test, src/tests/ltl2neverclaim.test, src/tests/ltl2tgba.test, src/tests/ltlcounter.test, src/tests/ltlcross.test, src/tests/neverclaimread.test, src/tests/obligation.test, src/tests/parseaut.test, src/tests/randaut.test, src/tests/randpsl.test, src/tests/renault.test, src/tests/satmin2.test, src/tests/sccsimpl.test, src/tests/sim2.test, src/tests/simdet.test, src/tests/spotlbtt.test, src/tests/wdba.test, src/tests/wdba2.test, bench/emptchk/README, bench/emptchk/defs.in, bench/ltlclasses/run, bench/ltlcounter/run, bench/wdba/run: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
4d848e988c
commit
17dc2f8654
38 changed files with 154 additions and 154 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@
|
|||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
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"
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@
|
|||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
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'"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 <formulae \
|
||||
"$ltl2tgba -t %f >%T" \
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
|
|
|
|||
|
|
@ -95,8 +95,8 @@ State: 8
|
|||
--END--
|
||||
EOF
|
||||
|
||||
run 0 ../ltl2tgba -CR -eSE05 -XH blue_counter
|
||||
run 0 ../ltl2tgba -CR -eTau03_opt -XH blue_counter
|
||||
run 0 ../ikwiad -CR -eSE05 -XH blue_counter
|
||||
run 0 ../ikwiad -CR -eTau03_opt -XH blue_counter
|
||||
|
||||
# s1->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
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
digraph G {
|
||||
|
|
@ -78,7 +78,7 @@ EOF
|
|||
diff expected stdout
|
||||
|
||||
|
||||
run 0 ../ltl2tgba -XDD dra.dstar | tee stdout
|
||||
run 0 ../ikwiad -XDD dra.dstar | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
@ -123,7 +123,7 @@ Acc-Sig:
|
|||
2
|
||||
EOF
|
||||
|
||||
run 0 ../ltl2tgba -XDB dsa.dstar | tee stdout
|
||||
run 0 ../ikwiad -XDB dsa.dstar | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
@ -213,7 +213,7 @@ Acc-Sig: +0 +1
|
|||
4
|
||||
EOF
|
||||
|
||||
run 0 ../ltl2tgba -XDD dra.dstar | tee stdout
|
||||
run 0 ../ikwiad -XDD dra.dstar | tee stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
|
|||
|
|
@ -28,8 +28,8 @@ set -e
|
|||
|
||||
dorun()
|
||||
{
|
||||
run 0 ../ltl2tgba -f -s "$1" >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 <output1` = `wc -l <output2`
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -28,14 +28,14 @@ set -e
|
|||
|
||||
expect_ce()
|
||||
{
|
||||
run 0 ../ltl2tgba -CR -e -XH "$1"
|
||||
run 0 ../ltl2tgba -CR -e -DT -XH "$1"
|
||||
run 0 ../ltl2tgba -CR -e'Cou99(shy)' -XH "$1"
|
||||
run 0 ../ltl2tgba -CR -e'Cou99(shy)' -DT -XH "$1"
|
||||
run 0 ../ltl2tgba -CR -eCVWY90 -XH "$1"
|
||||
run 0 ../ltl2tgba -CR -eGV04 -XH "$1"
|
||||
run 0 ../ltl2tgba -CR -eSE05 -XH "$1"
|
||||
run 0 ../ltl2tgba -CR -eTau03 -XH "$1"
|
||||
run 0 ../ikwiad -CR -e -XH "$1"
|
||||
run 0 ../ikwiad -CR -e -DT -XH "$1"
|
||||
run 0 ../ikwiad -CR -e'Cou99(shy)' -XH "$1"
|
||||
run 0 ../ikwiad -CR -e'Cou99(shy)' -DT -XH "$1"
|
||||
run 0 ../ikwiad -CR -eCVWY90 -XH "$1"
|
||||
run 0 ../ikwiad -CR -eGV04 -XH "$1"
|
||||
run 0 ../ikwiad -CR -eSE05 -XH "$1"
|
||||
run 0 ../ikwiad -CR -eTau03 -XH "$1"
|
||||
}
|
||||
|
||||
cat >input <<'EOF'
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
I -> 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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@
|
|||
. ./defs
|
||||
set -e
|
||||
|
||||
ltl2tgba=../ltl2tgba
|
||||
ltl2tgba=../ikwiad
|
||||
|
||||
|
||||
(
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ skip
|
|||
}
|
||||
EOF
|
||||
|
||||
run 0 ../ltl2tgba -XN -H input > stdout
|
||||
run 0 ../ikwiad -XN -H input > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
HOA: v1
|
||||
|
|
@ -89,7 +89,7 @@ od;
|
|||
}
|
||||
EOF
|
||||
|
||||
run 0 ../ltl2tgba -XN -H input > stdout
|
||||
run 0 ../ikwiad -XN -H input > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
HOA: v1
|
||||
|
|
@ -129,7 +129,7 @@ accept_all:
|
|||
skip
|
||||
}
|
||||
EOF
|
||||
run 0 ../ltl2tgba -XN input > stdout
|
||||
run 0 ../ikwiad -XN input > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
@ -172,7 +172,7 @@ EOF
|
|||
# but since the guard parser is more lenient, we just assume
|
||||
# that "p1 && " is an atomic property.
|
||||
|
||||
run 2 ../ltl2tgba -XN input > 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
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -1054,7 +1054,7 @@ expecterr non-existant<<EOF
|
|||
autfilt: Cannot open file non-existant
|
||||
EOF
|
||||
|
||||
run 2 ../ltl2tgba -XH foob 2>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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue