Commit ba4345a4 authored by Alexandre GBAGUIDI AISSE's avatar Alexandre GBAGUIDI AISSE Committed by Alexandre Duret-Lutz
Browse files

dtgbasat: Fix dtgbasat bench errors

* bench/dtgbasat/formulas: Fix bin's path.
* bench/dtgbasat/prepare.sh: Fix bin's path & ltl2tgba@-sD option.
* bench/dtgbasat/stats.sh: Fix bin's path.
* bench/dtgbasat/stat.sh: Fix bin's path, ltl2tgba@-sD option
parent 3b5fa22a
......@@ -93,7 +93,7 @@ G(G!a | F!c | G!b)
# randltl -n -1 a b c |
# ltlfilt --remove-wm -r -u --size-min=3 --size-max=15 --syntactic-recurrence |
# ltlfilt -v --obligation |
# ../../src/bin/ltl2tgba -F - -x tba-det -D --stats='%d,%f' |
../../bin/ltl2tgba -F - -x tba-det -D --stats='%d,%f' |
# grep 0, | head -n 30
X(Fc W b) R Fa
......
#!/bin/sh
ltlfilt=../../src/bin/ltlfilt
ltl2tgba=../../src/bin/ltl2tgba
dstar2tgba=../../src/bin/dstar2tgba
ltlfilt=../../bin/ltlfilt
ltl2tgba=../../bin/ltl2tgba
dstar2tgba=../../bin/dstar2tgba
# Rename all formulas using a b c... suppress duplicates.
$ltlfilt --ignore-errors --relabel=abc -u formulas > nodups.ltl
......@@ -16,7 +16,7 @@ while read f; do
echo "$f, trad, $acc, $acc2"
elif test `$ltl2tgba "$f" -x tba-det -D --stats="%d"` = 1; then
echo "$f, TCONG, $acc, $acc2"
elif test `$ltlfilt --remove-wm -f "$f" -l | ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - - | $dstar2tgba -D --low --stats="%d"` = 1; then
elif test `$ltlfilt --remove-wm -f "$f" -l | ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - - | $dstar2tgba -D --low --stats="%d"` = 1; then
echo "$f, DRA, $acc, $acc2"
else
echo "$f, not DBA-realizable, $acc, $acc2"
......
#!/bin/sh
ltlfilt=../../src/bin/ltlfilt
ltl2tgba=../../src/bin/ltl2tgba
dstar2tgba=../../src/bin/dstar2tgba
ltlfilt=../../bin/ltlfilt
ltl2tgba=../../bin/ltl2tgba
dstar2tgba=../../bin/dstar2tgba
timeout='timeout -sKILL 2h'
stats=--stats="%s, %e, %t, %a, %c, %d, %p, %r"
empty='-, -, -, -, -, -, -, -'
......@@ -49,7 +49,7 @@ case $type in
mindtba=`get_stats DTBA $ltl2tgba "$f" -D -x 'sat-minimize=-1,sat-acc=1'`
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer..." 1>&2
$ltlfilt --remove-wm -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$
dbamin=`get_dbamin_stats dra.$$`
dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
rm dra.$$
......@@ -70,7 +70,7 @@ case $type in
*TCONG*) dbamin="n/a, n/a" dra="n/a";;
*trad*)
$ltlfilt --remove-wm -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$
dbamin=`get_dbamin_stats dra.$$`
dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
rm dra.$$
......@@ -80,7 +80,7 @@ case $type in
*DRA*)
echo "$f, $accmax, $type... " 1>&2
$ltlfilt --remove-wm -f "$f" -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - dra.$$
input=`get_stats TBA $dstar2tgba dra.$$ -D -x '!wdba-minimize'`
echo "$f, $accmax, $type, $input, DBA, ... " 1>&2
dba=`get_stats BA $dstar2tgba dra.$$ -BD -x '!wdba-minimize'`
......
#!/bin/sh
ltlfilt=../../src/bin/ltlfilt
ltl2tgba=../../src/bin/ltl2tgba
dstar2tgba=../../src/bin/dstar2tgba
ltlfilt=../../bin/ltlfilt
ltl2tgba=../../bin/ltl2tgba
dstar2tgba=../../bin/dstar2tgba
timeout='timeout -sKILL 1h'
stats=--stats="%s, %e, %t, %a, %c, %d, %p, %r"
empty='-, -, -, -, -, -, -, -'
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment