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

better coverage for ltlsynt

Browse source 
* tests/core/ltlsynt.test: here
This commit is contained in:
Maximilien Colange 2018-05-22 11:24:17 +02:00
parent d7ee23ed2f
commit 6f057941ce
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
tests/core/ltlsynt.test
View file

@ -46,6 +46,15 @@ EOF
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --print-pg > out ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --print-pg > out
diff out exp diff out exp
cat >exp <<EOF
translating formula done
split inputs and outputs done
determinization done
parity game built
EOF
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
diff out exp
F0='(G ((((req) -> (X ((grant) && (X ((grant) && (X (grant))))))) && ((grant) F0='(G ((((req) -> (X ((grant) && (X ((grant) && (X (grant))))))) && ((grant)
-> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))' -> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))'
IN0='cancel, go, req' IN0='cancel, go, req'