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

stutter: new variant of Etessami's check

Browse source 
* src/tgbaalgos/stutter.cc: Add a new variant of Etessami's check,
closer to his original paper in IPL.
* src/ltltest/stutter.test: Add more tests.
* bench/stutter/user.sh: Include this new variant in the benchmark.
This commit is contained in:
Alexandre Duret-Lutz 2015-04-17 15:18:47 +02:00
parent ecfd9b7776
commit 9e959cdc7e
3 changed files with 45 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
bench/stutter/user.sh
View file

@ -8,9 +8,9 @@ set -e -x
(
must_exit=false
echo ap,algo,time,matched,exit.status
for ap in 1 2 3 4; do
for ap in 1 2 3; do
$RANDLTL $ap --tree-size=..30 -n -1 | $LTLFILT --ap=$ap | $LTLFILT -v --nox -n 500 > formulas
for algo in 1 2 3 4 5 6 7 8 0; do
for algo in 1 2 3 4 5 6 7 8 0 9; do
es=0
SPOT_STUTTER_CHECK=$algo /usr/bin/time -o user-$ap-$algo.csv -f "$ap,$algo,%e" $LTLFILT --stutter-invariant formulas > matched-$ap-$algo.ltl || must_exit=true es=$?
matched=`wc -l < matched-$ap-$algo.ltl`

25
src/ltltest/stutter.test
View file

@ -42,7 +42,7 @@ for i in 10 12 14 16 18 20; do
$randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
done
# We do not check i=0, it is too slow.
# We do not check i=0 and i=9, as they are too slow.
for i in 1 2 3 4 5 6 7 8; do
SPOT_STUTTER_CHECK=$i
export SPOT_STUTTER_CHECK
@ -53,3 +53,26 @@ done
for i in 2 3 4 5 6 7 8; do
diff res.1 res.$i
done
# Do a similar test on fewer formulas, so we can cover 0 and 9.
cat >$FILE <<EOF
F(a & X(!a & b))
F(a & X(!a & Xb))
F(a & X!a & Xb)
F(a & X(a & Xb))
F(a & Xb)
Xa
EOF
# We do not check i=0 and i=9, as they are too slow.
for i in 0 1 2 3 4 5 6 7 8 9; do
SPOT_STUTTER_CHECK=$i
export SPOT_STUTTER_CHECK
$time $ltlfilt --stutter-invariant -F $FILE > res.$i
done
# All results should be equal
for i in 1 2 3 4 5 6 7 8 9; do
diff res.0 res.$i
done

20
src/tgbaalgos/stutter.cc
View file

@ -25,8 +25,10 @@
#include "ltlvisit/apcollect.hh"
#include "translate.hh"
#include "ltlast/unop.hh"
#include "ltlast/binop.hh"
#include "ltlvisit/remove_x.hh"
#include "tgbaalgos/product.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgba/tgbaproduct.hh"
#include "tgba/bddprint.hh"
#include <deque>
@ -542,7 +544,7 @@ namespace spot
{
char* endptr;
long res = strtol(stutter_check, &endptr, 10);
if (*endptr || res < 0 || res > 8)
if (*endptr || res < 0 || res > 9)
throw
std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
return res;
@ -561,16 +563,28 @@ namespace spot
int algo = default_stutter_check_algorithm();
if (algo == 0) // Etessami's check via syntactic transformation.
if (algo == 0 || algo == 9)
// Etessami's check via syntactic transformation.
{
if (!f->is_ltl_formula())
throw std::runtime_error("Cannot use the syntactic "
"stutter-invariance check "
"for non-LTL formulas");
const ltl::formula* g = remove_x(f);
bool res;
if (algo == 0) // Equivalence check
{
ltl::ltl_simplifier ls;
bool res = ls.are_equivalent(f, g);
res = ls.are_equivalent(f, g);
g->destroy();
}
else
{
const ltl::formula* h = ltl::binop::instance(ltl::binop::Xor,
f->clone(), g);
res = ltl_to_tgba_fm(h, make_bdd_dict())->is_empty();
h->destroy();
}
return res;
}