8c33f959a3
* doc/spot.bib (perez.19.hoa): New entry. * spot/parseaut/public.hh: Mention it. * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Learn to parse the controllable-AP header. * spot/twaalgos/hoa.cc: Print it. * tests/core/ltlsynt.test, tests/core/parseaut.test, tests/core/readsave.test, tests/python/_synthesis.ipynb, tests/python/except.py, tests/python/games.ipynb, tests/python/mealy.py, tests/python/synthesis.py: Adjust or augment test cases.
826 lines
22 KiB
Bash
826 lines
22 KiB
Bash
#! /bin/sh
|
|
# -*- coding: utf-8 -*-
|
|
# Copyright (C) 2017, 2019-2022 Laboratoire de Recherche et
|
|
# Développement de l'Epita (LRDE).
|
|
#
|
|
# This file is part of Spot, a model checking library.
|
|
#
|
|
# Spot is free software; you can redistribute it and/or modify it
|
|
# under the terms of the GNU General Public License as published by
|
|
# the Free Software Foundation; either version 3 of the License, or
|
|
# (at your option) any later version.
|
|
#
|
|
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
# License for more details.
|
|
#
|
|
# You should have received a copy of the GNU General Public License
|
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
. ./defs || exit 1
|
|
|
|
set -e
|
|
|
|
cat >exp <<EOF
|
|
parity 17;
|
|
0 1 0 7,8 "INIT";
|
|
8 3 1 2;
|
|
2 1 0 11,12;
|
|
12 5 1 2,3;
|
|
3 1 0 13,14;
|
|
14 4 1 2,3;
|
|
13 4 1 1,4;
|
|
4 1 0 8,15;
|
|
15 3 1 5,6;
|
|
6 1 0 8,15;
|
|
5 1 0 16,17;
|
|
17 4 1 2;
|
|
16 4 1 5,6;
|
|
1 1 0 9,10;
|
|
10 3 1 2,3;
|
|
9 3 1 1,5;
|
|
11 5 1 1,4;
|
|
7 3 1 1,2;
|
|
parity 13;
|
|
0 1 0 1,2 "INIT";
|
|
2 1 1 3;
|
|
3 3 0 5,4;
|
|
4 2 1 12,3;
|
|
12 2 0 5,4;
|
|
5 1 1 6,7;
|
|
7 1 0 9,8;
|
|
8 3 1 12,3;
|
|
9 1 1 11,10;
|
|
10 2 0 9,8;
|
|
11 1 0 9,8;
|
|
6 1 0 13,4;
|
|
13 1 1 6,10;
|
|
1 1 1 6,3;
|
|
parity 5;
|
|
1 1 0 4,5 "INIT";
|
|
5 4 1 1,1;
|
|
4 5 1 0,1;
|
|
0 1 0 2,3;
|
|
3 5 1 1;
|
|
2 3 1 0,0;
|
|
EOF
|
|
|
|
: > out
|
|
for algo in ds sd lar; do
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --algo=$algo --print-pg >>out
|
|
done
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 1 1 0 1 0
|
|
2
|
|
2
|
|
i0 a
|
|
o0 b
|
|
EOF
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 1 1 0 1 0
|
|
2
|
|
2
|
|
i0 a
|
|
o0 b
|
|
EOF
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+dc >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 1 1 0 1 0
|
|
2
|
|
2
|
|
i0 a
|
|
o0 b
|
|
EOF
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+ud >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 1 1 0 1 0
|
|
2
|
|
2
|
|
i0 a
|
|
o0 b
|
|
EOF
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+sub1 >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 1 1 0 1 0
|
|
2
|
|
2
|
|
i0 a
|
|
o0 b
|
|
EOF
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop+sub2 >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 1 1 0 1 0
|
|
2
|
|
2
|
|
i0 a
|
|
o0 b
|
|
EOF
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=isop,isop+dc,isop+ud >out
|
|
diff out exp
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=ite >out
|
|
diff out exp
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger=ite+ud+dc >out
|
|
diff out exp
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --aiger >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 3 1 1 2 1
|
|
2
|
|
4 1
|
|
6
|
|
6
|
|
6 2 4
|
|
i0 a
|
|
o0 b
|
|
o1 c
|
|
EOF
|
|
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \
|
|
--algo=ds --simplify=no --aiger=isop >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 2 1 1 2 0
|
|
2
|
|
4 1
|
|
2
|
|
2
|
|
i0 a
|
|
o0 b
|
|
o1 c
|
|
EOF
|
|
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \
|
|
--algo=ds --simplify=no --aiger=isop+dc >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 3 1 1 2 1
|
|
2
|
|
4 1
|
|
6
|
|
6
|
|
6 4 2
|
|
i0 a
|
|
o0 b
|
|
o1 c
|
|
EOF
|
|
ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \
|
|
--algo=ds --simplify=no --aiger=ite >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for GFa <-> GFb
|
|
tanslating formula done in X seconds
|
|
direct strategy was found.
|
|
direct strat has 1 states and 0 colors
|
|
EOF
|
|
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for GFa <-> GFb
|
|
tanslating formula done in X seconds
|
|
direct strategy was found.
|
|
direct strat has 1 states and 0 colors
|
|
final strategy has 1 states and 2 edges
|
|
minimization took X seconds
|
|
EOF
|
|
ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for (Fa & Fb & Fc & Fd) <-> GFe
|
|
tanslating formula done in X seconds
|
|
direct strategy was found.
|
|
direct strat has 16 states and 0 colors
|
|
EOF
|
|
ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \
|
|
--verbose --realizability --algo=lar 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for G(Fi0 & Fi1 & Fi2) -> G(i1 <-> o0)
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 2 states and 3 colors
|
|
LAR construction done in X seconds
|
|
DPA has 4 states, 3 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 12 states
|
|
solving game with acceptance: parity max odd 5
|
|
game solved in X seconds
|
|
EOF
|
|
ltlsynt -f "G(Fi0 && Fi1 && Fi2) -> G(i1 <-> o0)" --outs="o0" --algo=lar \
|
|
--verbose --realizability 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
|
|
for r in '' '--real'; do
|
|
opts="$r --ins=a,c --outs=b -f"
|
|
ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || :
|
|
ltlsynt --algo=sd $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
|
|
ltlsynt --algo=ps $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
|
|
ltlsynt --algo=lar $opts 'FGc <-> GF(!b&XXb)' --csv='>>FILE' || :
|
|
ltlsynt --algo=lar.old $opts 'FGa <-> GF(c&a)' --csv='>>FILE' || :
|
|
test 6 = `wc -l < FILE`
|
|
# Make sure all lines in FILE have the same number of commas
|
|
sed 's/[^,]//g' < FILE |
|
|
( read first
|
|
while read l; do
|
|
test "x$first" = "x$l" || exit 1
|
|
done)
|
|
done
|
|
for a in sd ds lar lar.old; do
|
|
test 1 = `grep -c ",.$a.," FILE` || exit 1
|
|
done
|
|
|
|
# ltlsynt --algo=lar --ins=a --outs=b -f 'FGa <-> GF(c&a)' --print-pg --csv >out
|
|
# grep parity out
|
|
# grep 'FGa.*,"lar",' out
|
|
# grep formula out
|
|
|
|
|
|
F0='(G ((((req) -> (X ((grant) && (X ((grant) && (X (grant))))))) && ((grant)
|
|
-> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))'
|
|
IN0='cancel, go, req'
|
|
OUT0='grant'
|
|
EXP0='UNREALIZABLE'
|
|
F1='(G ((((req) -> (X ((grant) || (X ((grant) || (X (grant))))))) && ((grant)
|
|
-> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go))))))'
|
|
IN1='cancel, go, req'
|
|
OUT1='grant'
|
|
EXP1='UNREALIZABLE'
|
|
F2='((G ((cancel) -> (X (go)))) -> (G ((((req) -> (X ((grant) || (X ((grant) ||
|
|
(X (grant))))))) && ((grant) -> (X (! (grant))))) && ((cancel) -> (X ((!
|
|
(grant)) U (go)))))))'
|
|
IN2='cancel, go, req'
|
|
OUT2='grant'
|
|
EXP2='REALIZABLE'
|
|
F3='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((req) -> (X ((grant) ||
|
|
(X ((grant) || (X (grant))))))) && ((grant) -> (X (! (grant))))) && ((cancel)
|
|
-> (X ((! (grant)) U (go)))))))'
|
|
IN3='cancel, go, req'
|
|
OUT3='grant'
|
|
EXP3='REALIZABLE'
|
|
F4='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((req) -> (X (((grant) ||
|
|
(cancel)) || (X (((grant) || (cancel)) || (X ((grant) || (cancel)))))))) &&
|
|
((grant) -> (X (! (grant))))) && ((cancel) -> (X ((! (grant)) U (go)))))))'
|
|
IN4='cancel, go, req'
|
|
OUT4='grant'
|
|
EXP4='REALIZABLE'
|
|
F5='((G ((cancel) -> (X ((go) || (X ((go) || (X (go)))))))) -> (G ((((req) ->
|
|
(X (((grant) || (cancel)) || (X (((grant) || (cancel)) || (X ((grant) ||
|
|
(cancel)))))))) && ((grant) -> (X (! (grant))))) && ((cancel) -> (X ((!
|
|
(grant)) U (go)))))))'
|
|
IN5='cancel, go, req'
|
|
OUT5='grant'
|
|
EXP5='REALIZABLE'
|
|
F6='((G ((cancel) -> (X ((go) || (X (go)))))) -> (G ((((cancel) -> (X ((!
|
|
(grant)) U (go)))) && ((grant) -> (X (! (grant))))) && ((req) -> (((grant) ||
|
|
(cancel)) || (X (((grant) || (cancel)) || (X (((grant) || (cancel)) || (X
|
|
((grant) || (cancel))))))))))))'
|
|
IN6='cancel, go, req'
|
|
OUT6='grant'
|
|
EXP6='REALIZABLE'
|
|
F7='(! ((G ((req) -> (F (ack)))) && (G ((go) -> (F (grant))))))'
|
|
IN7='go, req'
|
|
OUT7='ack, grant'
|
|
EXP7='UNREALIZABLE'
|
|
F8='(((G ((((r1) -> (F (a1))) && ((r2) -> (F (a2)))) && (! ((a1) && (a2))))) &&
|
|
(((a1) U (r1)) || (G (a1)))) && (((a2) U (r2)) || (G (a2))))'
|
|
IN8='r1, r2'
|
|
OUT8='a1, a2'
|
|
EXP8='UNREALIZABLE'
|
|
F9='((((G (((((((r0) -> (F (a0))) && ((r1) -> (F (a1)))) && ((r2) -> (F (a2))))
|
|
&& (! ((a0) && (a1)))) && (! ((a0) && (a2)))) && (! ((a1) && (a2))))) && (((a0)
|
|
U (r0)) || (G (a0)))) && (((a1) U (r1)) || (G (a1)))) && (((a2) U (r2)) || (G
|
|
(a2))))'
|
|
IN9='r0, r1, r2'
|
|
OUT9='a0, a1, a2'
|
|
EXP9='UNREALIZABLE'
|
|
IN10='a, b, c'
|
|
OUT10='p0, p1, p2'
|
|
F10='G (p0 && ! p1 && ! p2 || (! p0 && p1 && ! p2) || (! p0 && ! p1 && p2)) &&
|
|
(F (G a) || F (G b) || G (F c) <-> (G (F p0) || (G (F p1) && ! G (F p2))))'
|
|
EXP10='REALIZABLE'
|
|
|
|
for i in 0 1 7 8 9; do
|
|
F=$(eval echo \$F$i)
|
|
IN=$(eval echo \$IN$i)
|
|
OUT=$(eval echo \$OUT$i)
|
|
EXP=$(eval echo \$EXP$i)
|
|
|
|
for algo in sd ds lar; do
|
|
test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \
|
|
--algo=$algo)
|
|
done
|
|
done
|
|
|
|
for i in 2 3 4 5 6 10; do
|
|
F=$(eval echo \$F$i)
|
|
IN=$(eval echo \$IN$i)
|
|
OUT=$(eval echo \$OUT$i)
|
|
EXP=$(eval echo \$EXP$i)
|
|
|
|
ltl2tgba -f "!($F)" > negf_aut$i
|
|
|
|
# test ltlsynt
|
|
for algo in sd ds ps lar lar.old; do
|
|
ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true
|
|
REAL=`head -1 out$i`
|
|
test $REAL = $EXP
|
|
tail -n +2 out$i > res$i
|
|
# check that the L(strategy) is included in L(F)
|
|
autfilt -q -v --intersect=negf_aut$i res$i
|
|
# check that all environment actions are possible
|
|
autfilt --remove-ap="$OUT" res$i | autfilt --dualize | autfilt --is-empty -q
|
|
done
|
|
done
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
HOA: v1
|
|
States: 3
|
|
Start: 0
|
|
AP: 1 "p0"
|
|
acc-name: all
|
|
Acceptance: 0 t
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
controllable-AP: 0
|
|
--BODY--
|
|
State: 0
|
|
[t] 1
|
|
State: 1
|
|
[t] 2
|
|
State: 2
|
|
[!0] 2
|
|
--END--
|
|
EOF
|
|
ltlsynt --outs=p0 -x tls-impl=0 --simpl=no -f '!XXF(p0 & (p0 M Gp0))' > out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 1 "p0"
|
|
acc-name: all
|
|
Acceptance: 0 t
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
controllable-AP: 0
|
|
--BODY--
|
|
State: 0
|
|
[!0] 0
|
|
--END--
|
|
EOF
|
|
ltlsynt --outs=p0 -x tls-impl=1 -f '!XXF(p0 & (p0 M Gp0))' > out
|
|
diff out exp
|
|
|
|
ltlsynt --outs=p0 -f '!XXF(p0 & (p0 M Gp0))' > out
|
|
diff out exp
|
|
|
|
f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))'
|
|
ltlsynt --verbose --algo=ps --outs p1 --ins p0 -f "$f" -x"dpa-simul=1" 2>err
|
|
grep 'DPA has 13 states' err
|
|
ltlsynt -x dpa-simul=0 --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
|
|
grep 'DPA has 29 states' err
|
|
ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
|
|
grep 'DPA has 12 states' err
|
|
|
|
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=no | grep 'States: 5'
|
|
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim | grep 'States: 5'
|
|
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa | grep 'States: 4'
|
|
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" | grep 'States: 4'
|
|
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=sat | grep 'States: 2'
|
|
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bisim-sat | grep 'States: 2'
|
|
ltlsynt --outs=p1 -f "$f" -x"dpa-simul=1" --simpl=bwoa-sat | grep 'States: 4'
|
|
|
|
# The following used to raise an exception because of a bug in
|
|
# split_2step_fast_here().
|
|
for i in 0 1 2 3 4 5; do
|
|
ltlsynt --ins=a -f 'GFa <-> GFb' --simplify=$i | grep 'States: 1'
|
|
done
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 34 4 3 2 27
|
|
2
|
|
4
|
|
6
|
|
8
|
|
10 39
|
|
12 62
|
|
14 68
|
|
25
|
|
31
|
|
16 11 13
|
|
18 14 16
|
|
20 10 12
|
|
22 15 20
|
|
24 19 23
|
|
26 11 12
|
|
28 15 26
|
|
30 19 29
|
|
32 7 9
|
|
34 16 32
|
|
36 15 32
|
|
38 35 37
|
|
40 3 32
|
|
42 2 4
|
|
44 6 42
|
|
46 8 42
|
|
48 5 32
|
|
50 10 14
|
|
52 12 14
|
|
54 41 45
|
|
56 47 49
|
|
58 51 53
|
|
60 54 56
|
|
62 58 60
|
|
64 33 51
|
|
66 42 53
|
|
68 64 66
|
|
i0 i0
|
|
i1 i1
|
|
i2 i2
|
|
i3 i3
|
|
o0 o0
|
|
o1 o1
|
|
EOF
|
|
ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
|
|
--aiger=isop --algo=lar --decompose=no --simpl=no >out
|
|
diff out exp
|
|
|
|
cat >exp <<EOF
|
|
REALIZABLE
|
|
aag 18 4 4 2 10
|
|
2
|
|
4
|
|
6
|
|
8
|
|
10 26
|
|
12 28
|
|
14 34
|
|
16 36
|
|
18
|
|
20
|
|
18 11 12
|
|
20 15 16
|
|
22 2 4
|
|
24 10 12
|
|
26 23 25
|
|
28 22 25
|
|
30 14 16
|
|
32 7 9
|
|
34 31 32
|
|
36 31 33
|
|
i0 i0
|
|
i1 i1
|
|
i2 i2
|
|
i3 i3
|
|
o0 o0
|
|
o1 o1
|
|
EOF
|
|
ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
|
|
--aiger=isop --algo=lar --decompose=yes --simpl=no >out
|
|
diff out exp
|
|
ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
|
|
--aiger=isop --algo=lar --simpl=no >out
|
|
diff out exp
|
|
|
|
# Issue #477
|
|
ltlsynt -f 'a U (b' 2>err && exit 1
|
|
test $? -eq 2
|
|
test `wc -l <err` -eq 4
|
|
|
|
|
|
cat >expected <<EOF
|
|
REALIZABLE
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 3 "a" "b" "c"
|
|
acc-name: all
|
|
Acceptance: 0 t
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
controllable-AP: 2
|
|
--BODY--
|
|
State: 0
|
|
[!0&!2 | !1&!2] 0
|
|
[0&1&2] 0
|
|
--END--
|
|
EOF
|
|
ltlsynt --ins=a,b -f 'G (a & b <=> c)' >stdout
|
|
diff stdout expected
|
|
ltlsynt --outs=c -f 'G (a & b <=> c)' >stdout
|
|
diff stdout expected
|
|
|
|
|
|
ltlsynt --ins=a,b --outs=c,a -f 'GFa | FGc | GFb' 2>stderr && :
|
|
test $? -eq 2
|
|
grep "'a' appears both" stderr
|
|
|
|
ltlsynt --ins=a --outs=c -f 'GFa | FGb | GFc' 2>stderr && :
|
|
test $? -eq 2
|
|
grep "both.*but 'b' is unlisted" stderr
|
|
ltlsynt -f 'GFa | FGb | GFc' 2>stderr && :
|
|
test $? -eq 2
|
|
grep "one of --ins or --outs" stderr
|
|
|
|
# Try to find a direct strategy for GFa <-> GFb and a direct strategy for
|
|
# Gc
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for GFa <-> GFb
|
|
tanslating formula done in X seconds
|
|
direct strategy was found.
|
|
direct strat has 1 states and 0 colors
|
|
final strategy has 1 states and 2 edges
|
|
minimization took X seconds
|
|
trying to create strategy directly for Gc
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 1 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 1 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 2 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
EOF
|
|
ltlsynt -f '(GFa <-> GFb) && (Gc)' --outs=b,c --verbose 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Try to find a direct strategy for (GFa <-> GFb) & Gc. THe order should not
|
|
# impact the result
|
|
for f in "(GFa <-> GFb) & Gc" "(GFb <-> GFa) & Gc" \
|
|
"Gc & (GFa <-> GFb)" "Gc & (GFb <-> GFa)"
|
|
do
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for $f
|
|
tanslating formula done in X seconds
|
|
direct strategy was found.
|
|
direct strat has 1 states and 0 colors
|
|
final strategy has 1 states and 2 edges
|
|
minimization took X seconds
|
|
EOF
|
|
ltlsynt -f "$f" --outs=b,c --verbose --decompose=0 --verify 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
done
|
|
|
|
# # Ltlsynt should be able to detect that G(a&c) is not input-complete so it is
|
|
# # impossible to find a strategy.
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for (GFb <-> GFa) & G(a & c)
|
|
tanslating formula done in X seconds
|
|
no strategy exists.
|
|
EOF
|
|
ltlsynt -f '(GFb <-> GFa) && G(a&c)' --outs=b,c --verbose\
|
|
--decompose=0 2> out || true
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# # Ltlsynt should be able to create a strategy when the last G
|
|
# is input-complete.
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for (GFb <-> GFa) & G((a & c) | (!a & !c))
|
|
tanslating formula done in X seconds
|
|
direct strategy was found.
|
|
direct strat has 1 states and 0 colors
|
|
final strategy has 1 states and 2 edges
|
|
minimization took X seconds
|
|
EOF
|
|
ltlsynt -f '(GFb <-> GFa) && (G((a&c)|(!a&!c)))' --outs=b,c --verbose\
|
|
--verify --decompose=0 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Direct strategy for persistence
|
|
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for Fa <-> FGb
|
|
tanslating formula done in X seconds
|
|
direct strategy was found.
|
|
direct strat has 2 states and 0 colors
|
|
final strategy has 2 states and 3 edges
|
|
minimization took X seconds
|
|
EOF
|
|
ltlsynt -f "Fa <-> FGb" --outs=b,c --verbose --decompose=0 --verify 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Test verbose aiger
|
|
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for Ga <-> Gb
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 4 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 4 states, 4 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 9 states
|
|
solving game with acceptance: parity max odd 6
|
|
game solved in X seconds
|
|
AIG circuit was created in X seconds and has 0 latches and 0 gates
|
|
EOF
|
|
ltlsynt -f "Ga <-> Gb" --outs=b --verbose --decompose=0 --verify --aiger 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for (b & (b | y)) -> y
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 2 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 2 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
trying to create strategy directly for (a | x) -> x
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 2 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 2 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
AIG circuit was created in X seconds and has 0 latches and 0 gates
|
|
EOF
|
|
ltlsynt -f '((a|x) & (b | y) & b) => (x & y)' --outs="x,y" --aiger=ite\
|
|
--verify --verbose 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Here, G!(!x | !y) should be Gx & Gy
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for Gx
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 1 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 1 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 2 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
trying to create strategy directly for Gy
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 1 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 1 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 2 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
AIG circuit was created in X seconds and has 0 latches and 0 gates
|
|
EOF
|
|
ltlsynt -f 'G!(!x | !y)' --outs="x, y" --aiger=ite --verify --verbose 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Here, !F(a | b) should be G(!a) & G(!b)
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for G!a
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 1 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 1 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
EOF
|
|
ltlsynt -f '!F(a|b)' --outs=b --decompose=yes --aiger --verbose 2> out || true
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Here, G!(a -> b) should be G(a) & G(!b)
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for Ga
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 1 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 1 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
EOF
|
|
ltlsynt -f 'G!(a -> b)' --outs=b --decompose=yes --aiger\
|
|
--verbose 2> out || true
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Here, (a & b) U (b & c) should be (a U (b & c)) & (b U (b & c))
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for (a & b) U (b & c)
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 2 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 2 states, 4 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 5 states
|
|
solving game with acceptance: parity max odd 6
|
|
game solved in X seconds
|
|
AIG circuit was created in X seconds and has 0 latches and 0 gates
|
|
EOF
|
|
ltlsynt -f '(a & b) U (b & c)' --outs=b,c --decompose=yes --aiger --verbose\
|
|
--verify 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Here, a => (b & c & d) should be
|
|
# (a => b) & (a => c) & (a => d)
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for a -> b
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 2 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 2 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
trying to create strategy directly for a -> c
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 2 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 2 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
trying to create strategy directly for a -> d
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 2 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 2 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
AIG circuit was created in X seconds and has 0 latches and 0 gates
|
|
EOF
|
|
ltlsynt -f 'a => (b & c & d)' --outs=b,c,d, --decompose=yes\
|
|
--verbose --aiger 2> out
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|
|
|
|
# Here, !(F(a | b)) should be G!a & G!b
|
|
cat >exp <<EOF
|
|
trying to create strategy directly for G!a
|
|
direct strategy might exist but was not found.
|
|
translating formula done in X seconds
|
|
automaton has 1 states and 1 colors
|
|
LAR construction done in X seconds
|
|
DPA has 1 states, 2 colors
|
|
split inputs and outputs done in X seconds
|
|
automaton has 4 states
|
|
solving game with acceptance: parity max odd 4
|
|
game solved in X seconds
|
|
EOF
|
|
ltlsynt -f '!(F(a | b))' --outs=b, --decompose=yes \
|
|
--verbose --aiger 2> out || true
|
|
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
|
|
diff outx exp
|