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

ltlsynt: save source filename with --csv

Browse source 
* bin/ltlsynt.cc (print_csv): Make filename mandatory, and add a
"was_game" argument.
(process_formula, process_aut_file): Adjust calls.
* tests/core/ltlsynt2.test: Adjust test cases.
This commit is contained in:
Alexandre Duret-Lutz 2024-09-04 16:17:46 +02:00
parent 45cb9caa0e
commit 6e5592fe6a
3 changed files with 63 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

38
tests/core/ltlsynt2.test
View file

@ -47,7 +47,8 @@ except ImportError:
x = pandas.read_csv("out.csv")
x.to_csv('filtered.csv',
columns=('formula', 'algo', 'realizable', 'strat_num_states'),
columns=('source', 'formula', 'algo',
'realizable', 'strat_num_states'),
index=False)
EOF
@ -55,24 +56,39 @@ EOF
$PYTHON test.py
cat >expected <<EOF
formula,algo,realizable,strat_num_states
G(i1 <-> Xo1),lar,1,3
F(i1 xor i2) <-> Fo1,lar,1,2
i1 <-> F(o1 xor o2),lar,1,3
Fi1 <-> Go2,lar,0,0
o1 & F(i1 <-> o2),lar,1,2
source,formula,algo,realizable,strat_num_states
formulas.ltl:1,G(i1 <-> Xo1),lar,1,3
formulas.ltl:2,F(i1 xor i2) <-> Fo1,lar,1,2
formulas.ltl:3,i1 <-> F(o1 xor o2),lar,1,3
formulas.ltl:4,Fi1 <-> Go2,lar,0,0
,o1 & F(i1 <-> o2),lar,1,2
EOF
diff filtered.csv expected
# ltlfilt should be able to read the first columns
# ltlfilt should be able to read the second column
mv filtered.csv input.csv
ltlsynt --ins=i1,i2 -F input.csv/-1 --csv=out.csv -q && exit 2
ltlsynt --ins=i1,i2 -F input.csv/-2 --csv=out.csv -q && exit 2
test $? -eq 1
$PYTHON test.py
cat >expected <<EOF
source,formula,algo,realizable,strat_num_states
input.csv:2,G(i1 <-> Xo1),lar,1,3
input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2
input.csv:4,i1 <-> F(o1 xor o2),lar,1,3
input.csv:5,Fi1 <-> Go2,lar,0,0
input.csv:6,o1 & F(i1 <-> o2),lar,1,2
EOF
diff filtered.csv expected
grep -v 0,0 filtered.csv >input.csv
ltlsynt --ins=i1,i2 -F input.csv/-1 --csv=out.csv -q || exit 2
ltlsynt -F input.csv/-2 --csv=out.csv -q || exit 2
$PYTHON test.py
diff filtered.csv input.csv
cat >expected <<EOF
source,formula,algo,realizable,strat_num_states
input.csv:2,G(i1 <-> Xo1),lar,1,3
input.csv:3,F(i1 xor i2) <-> Fo1,lar,1,2
input.csv:4,i1 <-> F(o1 xor o2),lar,1,3
input.csv:5,o1 & F(i1 <-> o2),lar,1,2
EOF
diff filtered.csv expected