Commit 4a9bbbaf authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Add ltl3ba to the ltl2tgba benchmark.

* configure.ac: Search for ltl3ba.
* bench/ltl2tgba/defs.in: Define LTL3BA and HAVE_LTL3BA.
* bench/ltl2tgba/algorithms: Use LTL3BA. Also add simulation options
for LTL2BA.
* bench/ltl2tgba/README: Slight wording changes.
parent bf62d439
......@@ -162,7 +162,8 @@ Notes:
real binary with the locally built libraries.)
* Some tools will appear to have translated fewer automata than the
others. This normally indicates bugs in the translator. In that
case it is harder to compare the results. (Normalizing the other
values accordingly may not be fair: maybe the translator precisely
failed to translate the largest automata.)
others. This normally indicates bugs in the translator (incorrect
output) or timeouts. In that case it is harder to compare the
results. (Normalizing the other values accordingly may not be
fair: maybe the translator precisely failed to translate the
largest automata.)
......@@ -15,6 +15,37 @@ Algorithm
Enabled = $HAVE_LTL2BA
}
Algorithm
{
Name = "ltl3ba"
Path = "lbtt-translate"
Parameters = "--spin $LTL3BA"
Enabled = $HAVE_LTL3BA
}
Algorithm
{
Name = "ltl3ba -M"
Path = "lbtt-translate"
Parameters = "--spin '$LTL3BA -M'"
Enabled = $HAVE_LTL3BA
}
Algorithm
{
Name = "ltl3ba -S"
Path = "lbtt-translate"
Parameters = "--spin '$LTL3BA -S'"
Enabled = $HAVE_LTL3BA
}
Algorithm
{
Name = "ltl3ba -M -S"
Path = "lbtt-translate"
Parameters = "--spin '$LTL3BA -M -S'"
Enabled = $HAVE_LTL3BA
}
Algorithm
{
......@@ -87,6 +118,14 @@ Algorithm
Enabled = yes
}
Algorithm
{
Name = "Spot FM Sim (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -RDS -F'"
Enabled = yes
}
Algorithm
{
Name = "Spot FM WDBA (TGBA)"
......@@ -95,4 +134,11 @@ Algorithm
Enabled = yes
}
Algorithm
{
Name = "Spot FM WDBA+Sim (TGBA)"
Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -Rm -RDS -F'"
Enabled = yes
}
EOF
# -*- shell-script -*-
# -*- shell-script; coding: utf-8 -*-
# Copyright (C) 2012 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
# dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
......@@ -39,6 +41,7 @@ LBT="@LBT@"
LBTT="@LBTT@"
LBTT_TRANSLATE="@LBTT_TRANSLATE@"
LTL2BA="@LTL2BA@"
LTL3BA="@LTL3BA@"
LTL2NBA="@LTL2NBA@"
LTL2TGBA="@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@"
ELTL2TGBA="@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@"
......@@ -46,7 +49,7 @@ MODELLA="@MODELLA@"
SPIN="@SPIN@"
WRING2LBTT="@WRING2LBTT@"
for var in LBT LTL2BA LTL2NBA MODELLA SPIN WRING2LBTT
for var in LBT LTL2BA LTL3BA LTL2NBA MODELLA SPIN WRING2LBTT
do
if eval 'test -z "$'$var'"'; then
eval HAVE_$var=no
......
......@@ -89,6 +89,7 @@ AM_CONDITIONAL([NEVER], [false])
AC_PATH_PROG([DOT], [dot])
AC_CHECK_PROG([LBT], [lbt], [lbt])
AC_CHECK_PROG([LTL2BA], [ltl2ba], [ltl2ba])
AC_CHECK_PROG([LTL3BA], [ltl3ba], [ltl3ba])
AC_CHECK_PROG([MODELLA], [modella], [modella])
AC_CHECK_PROG([LTL2NBA], [script4lbtt.py], [script4lbtt.py])
AC_CHECK_PROG([PERL], [perl], [perl])
......
Supports Markdown
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