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

* src/tgbatest/babiak.test: Rewrite using ltlcross.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2013-01-10 18:42:36 +01:00
parent 081aa0d120
commit 2580fc6f91
1 changed files with 8 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

80
src/tgbatest/babiak.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement # Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -27,7 +27,6 @@
# buildfarm will timeout if it does). # buildfarm will timeout if it does).
. ./defs . ./defs
need_lbtt
set -e set -e
@ -40,73 +39,10 @@ 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))) (G(G(((F p5)U((((F!p1)V(p2 &!p4))|!p2)|((X!p7 U!p4)V(F(F((G p2)&p5))))))U p6)))
EOF EOF
cat > config <<EOF ltl2tgba=../ltl2tgba
Algorithm
{
Name = "Spot/FM basic"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -f -t'"
Enabled = yes
}
Algorithm ../../bin/ltlcross <formulae \
{ "$ltl2tgba -t %f >%T" \
Name = "Spot/FM, with reductions + degeneralization (neverclaim)" "$ltl2tgba -N -r4 -R3f %f >%N" \
Path = "${LBTT_TRANSLATE}" "$ltl2tgba -N -r7 -R3 -x -Rm %f >%N" \
Parameters = "--spin '../ltl2tgba -r4 -R3f -F -f -N'" "$ltl2tgba -t -r7 -R3 -f -x -DS -Rm %f >%T"
Enabled = yes
}
Algorithm
{
Name = "Spot/FM, with reducetion + WDBA + degeneralization (neverclaim)"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spin '../ltl2tgba -r7 -R3 -f -x -N -F -Rm'"
Enabled = yes
}
Algorithm
{
Name = "Spot/FM, with reducetion + WDBA + degeneralization (DS)"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -r7 -R3 -f -x -DS -t -F -Rm'"
Enabled = yes
}
GlobalOptions
{
Rounds = 6
Interactive = Never
# Verbosity = 5
# ComparisonCheck = no
# ConsistencyCheck = no
# IntersectionCheck = no
}
# Not used, but LBTT seems to want it.
FormulaOptions
{
Size = 1...13
Propositions = 6
AbbreviatedOperators = Yes
GenerateMode = Normal
OutputMode = Normal
PropositionPriority = 50
TruePriority = 1
FalsePriority = 1
AndPriority = 10
OrPriority = 10
XorPriority = 0
# EquivalencePriority = 0
BeforePriority = 0
DefaultOperatorPriority = 5
}
EOF
${LBTT} --formulafile=formulae
rm config