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

ltldo: rounds start at 1

Browse source 
* src/bin/ltldo.cc: Start at 1.
* src/tgbatest/ltldo.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-27 16:02:13 +01:00
parent a24a021964
commit 48d508420b
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/bin/ltldo.cc
View file

@ -317,7 +317,7 @@ namespace
f = g; f = g;
} }
static unsigned round = 0; static unsigned round = 1;
runner.round_formula(f, round); runner.round_formula(f, round);
unsigned ts = translators.size(); unsigned ts = translators.size();

12
src/tgbatest/ltldo.test
View file

@ -53,12 +53,12 @@ run 0 $ltldo "{tgba}$ltl2tgba %f -H >%H" "{ba}$ltl2tgba >%N %f -s" \
--stats="%T,%R,%f,%s,%t,%e" >output --stats="%T,%R,%f,%s,%t,%e" >output
cat output cat output
cat >expected <<EOF cat >expected <<EOF
tgba,0,GFp1,1,2,2 tgba,1,GFp1,1,2,2
ba,0,GFp1,2,4,4 ba,1,GFp1,2,4,4
tgba,1,GFp1 & GFp2,1,4,4 tgba,2,GFp1 & GFp2,1,4,4
ba,1,GFp1 & GFp2,3,12,8 ba,2,GFp1 & GFp2,3,12,8
tgba,2,GFp1 & GFp2 & GFp3,1,8,8 tgba,3,GFp1 & GFp2 & GFp3,1,8,8
ba,2,GFp1 & GFp2 & GFp3,4,32,13 ba,3,GFp1 & GFp2 & GFp3,4,32,13
EOF EOF
diff output expected diff output expected