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

Use -l wherever we where expecting ltl2tgba to default to LaCIM.

Browse source 
* bench/ltl2tgba/algorithms: Use -l for all LaCIM invocations.
* src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
src/tgbatest/spotlbtt.test: Likewise.
This commit is contained in:
Alexandre Duret-Lutz 2009-11-12 16:46:04 +01:00
parent c9b65cff71
commit 8cdc196719
5 changed files with 33 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2009-11-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Use -l wherever we where expecting ltl2tgba to default to LaCIM.
* bench/ltl2tgba/algorithms: Use -l for all LaCIM invocations.
* src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
src/tgbatest/spotlbtt.test: Likewise.
2009-11-12 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-11-12 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Cleanup the help of ltl2tgba. Cleanup the help of ltl2tgba.

8
bench/ltl2tgba/algorithms
View file

@ -3,7 +3,7 @@ Algorithm
{ {
Name = "LaCIM, degen" Name = "LaCIM, degen"
Path = "$LBTT_TRANSLATE" Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -t -D -F'" Parameters = "--spot '$LTL2TGBA -l -t -D -F'"
Enabled = yes Enabled = yes
} }
@ -11,7 +11,7 @@ Algorithm
{ {
Name = "LaCIM, gen" Name = "LaCIM, gen"
Path = "$LBTT_TRANSLATE" Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -t -F'" Parameters = "--spot '$LTL2TGBA -l -t -F'"
Enabled = yes Enabled = yes
} }
@ -19,7 +19,7 @@ Algorithm
{ {
Name = "LaCIM, degen, +pre" Name = "LaCIM, degen, +pre"
Path = "$LBTT_TRANSLATE" Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -t -D -r4 -F'" Parameters = "--spot '$LTL2TGBA -l -t -D -r4 -F'"
Enabled = yes Enabled = yes
} }
@ -27,7 +27,7 @@ Algorithm
{ {
Name = "LaCIM, gen, +pre" Name = "LaCIM, gen, +pre"
Path = "$LBTT_TRANSLATE" Path = "$LBTT_TRANSLATE"
Parameters = "--spot '$LTL2TGBA -t -r4 -F'" Parameters = "--spot '$LTL2TGBA -l -t -r4 -F'"
Enabled = yes Enabled = yes
} }

4
src/tgbatest/dupexp.test
View file

@ -31,8 +31,8 @@ dorun()
run 0 ../ltl2tgba -f -S "$1" >output2 run 0 ../ltl2tgba -f -S "$1" >output2
test `wc -l <output1` = `wc -l <output2` test `wc -l <output1` = `wc -l <output2`
run 0 ../ltl2tgba -s "$1" >output1 run 0 ../ltl2tgba -l -s "$1" >output1
run 0 ../ltl2tgba -S "$1" >output2 run 0 ../ltl2tgba -l -S "$1" >output2
test `wc -l <output1` = `wc -l <output2` test `wc -l <output1` = `wc -l <output2`
} }

32
src/tgbatest/emptchk.test
View file

@ -33,21 +33,21 @@ expect_ce_do()
expect_ce() expect_ce()
{ {
expect_ce_do -e "$1" expect_ce_do -e -l "$1"
expect_ce_do -e -D "$1" expect_ce_do -e -l -D "$1"
expect_ce_do -e -f "$1" expect_ce_do -e -f "$1"
expect_ce_do -e -f -D "$1" expect_ce_do -e -f -D "$1"
expect_ce_do -e'Cou99(shy)' "$1" expect_ce_do -e'Cou99(shy)' -l "$1"
expect_ce_do -e'Cou99(shy)' -D "$1" expect_ce_do -e'Cou99(shy)' -l -D "$1"
expect_ce_do -e'Cou99(shy)' -f "$1" expect_ce_do -e'Cou99(shy)' -f "$1"
expect_ce_do -e'Cou99(shy)' -f -D "$1" expect_ce_do -e'Cou99(shy)' -f -D "$1"
expect_ce_do -eCVWY90 "$1" expect_ce_do -eCVWY90 -l "$1"
expect_ce_do -eCVWY90 -f "$1" expect_ce_do -eCVWY90 -f "$1"
run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' "$1" run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -f "$1" run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -eSE05 "$1" run 0 ../ltl2tgba -eSE05 -l "$1"
run 0 ../ltl2tgba -eSE05 -f "$1" run 0 ../ltl2tgba -eSE05 -f "$1"
run 0 ../ltl2tgba -e'SE05(bsh=10M)' "$1" run 0 ../ltl2tgba -e'SE05(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -e'SE05(bsh=10M)' -f "$1" run 0 ../ltl2tgba -e'SE05(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -eTau03_opt -f "$1" run 0 ../ltl2tgba -eTau03_opt -f "$1"
run 0 ../ltl2tgba -eGV04 -f "$1" run 0 ../ltl2tgba -eGV04 -f "$1"
@ -58,21 +58,21 @@ expect_ce()
expect_no() expect_no()
{ {
run 0 ../ltl2tgba -E "$1" run 0 ../ltl2tgba -E -l "$1"
run 0 ../ltl2tgba -E -D "$1" run 0 ../ltl2tgba -E -l -D "$1"
run 0 ../ltl2tgba -E -f "$1" run 0 ../ltl2tgba -E -f "$1"
run 0 ../ltl2tgba -E -f -D "$1" run 0 ../ltl2tgba -E -f -D "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' "$1" run 0 ../ltl2tgba -E'Cou99(shy)' -l "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' -D "$1" run 0 ../ltl2tgba -E'Cou99(shy)' -l -D "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' -f "$1" run 0 ../ltl2tgba -E'Cou99(shy)' -f "$1"
run 0 ../ltl2tgba -E'Cou99(shy)' -f -D "$1" run 0 ../ltl2tgba -E'Cou99(shy)' -f -D "$1"
run 0 ../ltl2tgba -ECVWY90 "$1" run 0 ../ltl2tgba -ECVWY90 -l "$1"
run 0 ../ltl2tgba -ECVWY90 -f "$1" run 0 ../ltl2tgba -ECVWY90 -f "$1"
run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' "$1" run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -f "$1" run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -ESE05 "$1" run 0 ../ltl2tgba -ESE05 -l "$1"
run 0 ../ltl2tgba -ESE05 -f "$1" run 0 ../ltl2tgba -ESE05 -f "$1"
run 0 ../ltl2tgba -E'SE05(bsh=10M)' "$1" run 0 ../ltl2tgba -E'SE05(bsh=10M)' -l "$1"
run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1" run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -ETau03_opt -f "$1" run 0 ../ltl2tgba -ETau03_opt -f "$1"
run 0 ../ltl2tgba -EGV04 -f "$1" run 0 ../ltl2tgba -EGV04 -f "$1"

6
src/tgbatest/spotlbtt.test
View file

@ -32,7 +32,7 @@ Algorithm
{ {
Name = "Spot (Couvreur -- LaCIM)" Name = "Spot (Couvreur -- LaCIM)"
Path = "${LBTT_TRANSLATE}" Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -t'" Parameters = "--spot '../ltl2tgba -F -l -t'"
Enabled = yes Enabled = yes
} }
@ -40,7 +40,7 @@ Algorithm
{ {
Name = "Spot (Couvreur -- LaCIM), reduction of formula" Name = "Spot (Couvreur -- LaCIM), reduction of formula"
Path = "${LBTT_TRANSLATE}" Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -r4 -F -t'" Parameters = "--spot '../ltl2tgba -r4 -l -F -t'"
Enabled = yes Enabled = yes
} }
@ -48,7 +48,7 @@ Algorithm
{ {
Name = "Spot (Couvreur -- LaCIM), degeneralized" Name = "Spot (Couvreur -- LaCIM), degeneralized"
Path = "${LBTT_TRANSLATE}" Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -t -D'" Parameters = "--spot '../ltl2tgba -l -F -t -D'"
Enabled = yes Enabled = yes
} }