tests: Improve tests related to SAT-minimization
* tests/core/satmin.test: Delete check for SPOT_SATSOLVER env variable and add state numbers verification. * tests/core/satmin2.test: Delete check for SPOT_SATSOLVER env variable. * tests/python/satmin.py: Delete check for SPOT_SATSOLVER env variable.
This commit is contained in:
Alexandre GBAGUIDI AISSE
parent
32f040fa45
commit
dfd500a559
3 changed files with 592 additions and 31 deletions
|
|
@ -21,12 +21,28 @@
|
|||
. ./defs
|
||||
set -e
|
||||
|
||||
# Skip if $SATSOLVE is not installed.
|
||||
(${SATSOLVER-glucose} --help >/dev/null 2>&1) || exit 77
|
||||
|
||||
ltl2tgba=ltl2tgba
|
||||
ltlcross=ltlcross
|
||||
|
||||
# The formulas below have been removed from the list to reduce the time
|
||||
# required to complete the test. In the future, we would like to respond
|
||||
# quickly to them.
|
||||
#
|
||||
# GF(a <-> XXXb)
|
||||
# X((a M F((!c & !b) | (c & b))) W (G!c U b))
|
||||
# (Fa W b) R (Fc | !a)
|
||||
# G((G!a & ((!b & X!c) | (b & Xc))) | (Fa & ((!b & Xc) | (b & X!c))))
|
||||
# X(a R ((!b & F!c) M X!a))
|
||||
# X(Gc | XG((b & Ga) | (!b & F!a)))
|
||||
# (a U X!a) | XG(!b & XFc)
|
||||
# XXG(Fa U Xb)
|
||||
#
|
||||
# Those one where removed because they were too long in the "expected" file.
|
||||
# We can not exceed 80 characters!
|
||||
#
|
||||
# p U (q & X(r & F(s & XF(u & XF(v & XFw)))))
|
||||
# (p U q U r) || (q U r U p) || (r U p U q)
|
||||
|
||||
cat >formulas <<'EOF'
|
||||
XXa
|
||||
GF(a -> XXXb)
|
||||
|
|
@ -41,57 +57,610 @@ GFa
|
|||
a U b U c U d
|
||||
G(a -> Fb) & Gc
|
||||
(Ga -> Fb) & (G!a -> F!b)
|
||||
p U (q & X(r & F(s & XF(u & XF(v & XFw)))))
|
||||
G(a -> Fb) & G(b -> Fc)
|
||||
G(a -> Fb) & G(!a -> F!b)
|
||||
GFp && GFq && GF r && GF u
|
||||
GF(a <-> XXXb)
|
||||
G(p -> q U r)
|
||||
GF(a <-> XXb)
|
||||
G!c & G(a -> Fb) & G(b -> Fc)
|
||||
G(a -> XXXb)
|
||||
G(a -> Fb)
|
||||
G(a U b U !a U !b)
|
||||
(p U q U r) || (q U r U p) || (r U p U q)
|
||||
X((a M F((!c & !b) | (c & b))) W (G!c U b))
|
||||
X(((a & b) R (!a U !c)) R b)
|
||||
XXG(Fa U Xb)
|
||||
(!a M !b) W F!c
|
||||
(b & Fa & GFc) R a
|
||||
(a R (b W a)) W G(!a M (c | b))
|
||||
(Fa W b) R (Fc | !a)
|
||||
X(G(!a M !b) | G(a | G!a))
|
||||
Fa W Gb
|
||||
Ga | GFb
|
||||
G((G!a & ((!b & X!c) | (b & Xc))) | (Fa & ((!b & Xc) | (b & X!c))))
|
||||
a M G(F!b | X!a)
|
||||
G!a R XFb
|
||||
XF(!a | GFb)
|
||||
G(F!a U !a) U Xa
|
||||
(a | G(a M !b)) W Fc
|
||||
Fa W Xb
|
||||
X(a R ((!b & F!c) M X!a))
|
||||
XG!a R Fb
|
||||
GFc | (a & Fb)
|
||||
X(a R (Fb R F!b))
|
||||
G(Xa M Fa)
|
||||
X(Gb | GFa)
|
||||
X(Gc | XG((b & Ga) | (!b & F!a)))
|
||||
Ga R Fb
|
||||
G(a U (b | X((!c & !a) | (a & c))))
|
||||
XG((G!a & F!b) | (Fa & (a | Gb)))
|
||||
(a U X!a) | XG(!b & XFc)
|
||||
X(G!a | GFa)
|
||||
G(G!a | F!c | G!b)
|
||||
G(a | Fa)
|
||||
EOF
|
||||
|
||||
# The following tests are named from 1 to 11 in order to reduce the length of
|
||||
# each line. If a test fails during the diff, it is easily identifiable.
|
||||
$ltlcross -F formulas \
|
||||
--timeout=60 \
|
||||
"$ltl2tgba --det --lbtt %f >%T" \
|
||||
"$ltl2tgba --det --lbtt -x tba-det %f >%T" \
|
||||
"$ltl2tgba --det --lbtt -x sat-acc=1 %f >%T" \
|
||||
"$ltl2tgba --det --lbtt -x sat-acc=3 %f >%T" \
|
||||
"$ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \
|
||||
"$ltl2tgba --det --lbtt -x sat-minimize %f >%T" \
|
||||
"$ltl2tgba --det --lbtt -x sat-minimize=2 %f >%T" \
|
||||
--json=det.json
|
||||
"{1} $ltl2tgba --det --lbtt %f >%T" \
|
||||
"{2} $ltl2tgba --det --lbtt -x tba-det %f >%T" \
|
||||
"{3} $ltl2tgba --det --lbtt -x sat-acc=1 %f >%T" \
|
||||
"{4} $ltl2tgba --det --lbtt -x sat-acc=3 %f >%T" \
|
||||
"{5} $ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \
|
||||
"{6} $ltl2tgba --det --lbtt -x sat-minimize %f >%T" \
|
||||
"{7} $ltl2tgba --det --lbtt -x sat-minimize=2 %f >%T" \
|
||||
--csv=det.csv
|
||||
|
||||
grep -v ',\"5\",' det.csv | cut -d ',' -f '1,2,6' > extracted
|
||||
|
||||
cat >expected <<'EOF'
|
||||
"formula","tool","states"
|
||||
"X(X(p0))","1",4
|
||||
"X(X(p0))","2",4
|
||||
"X(X(p0))","3",4
|
||||
"X(X(p0))","4",4
|
||||
"X(X(p0))","6",4
|
||||
"X(X(p0))","7",4
|
||||
"!(X(X(p0)))","1",4
|
||||
"!(X(X(p0)))","2",4
|
||||
"!(X(X(p0)))","3",4
|
||||
"!(X(X(p0)))","4",4
|
||||
"!(X(X(p0)))","6",4
|
||||
"!(X(X(p0)))","7",4
|
||||
"G(F((p0) -> (X(X(X(p1))))))","1",1
|
||||
"G(F((p0) -> (X(X(X(p1))))))","2",1
|
||||
"G(F((p0) -> (X(X(X(p1))))))","3",1
|
||||
"G(F((p0) -> (X(X(X(p1))))))","4",1
|
||||
"G(F((p0) -> (X(X(X(p1))))))","6",1
|
||||
"G(F((p0) -> (X(X(X(p1))))))","7",1
|
||||
"!(G(F((p0) -> (X(X(X(p1)))))))","1",2
|
||||
"!(G(F((p0) -> (X(X(X(p1)))))))","2",2
|
||||
"!(G(F((p0) -> (X(X(X(p1)))))))","3",2
|
||||
"!(G(F((p0) -> (X(X(X(p1)))))))","4",2
|
||||
"!(G(F((p0) -> (X(X(X(p1)))))))","6",2
|
||||
"!(G(F((p0) -> (X(X(X(p1)))))))","7",2
|
||||
"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","1",5
|
||||
"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","2",5
|
||||
"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","3",5
|
||||
"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","4",5
|
||||
"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","6",5
|
||||
"F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3))))))))))","7",5
|
||||
"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","1",4
|
||||
"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","2",4
|
||||
"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","3",4
|
||||
"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","4",4
|
||||
"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","6",4
|
||||
"!(F((p0) & (X(F((p1) & (X(F((p2) & (X(F(p3)))))))))))","7",4
|
||||
"F((p0) & (X((p1) U (p2))))","1",3
|
||||
"F((p0) & (X((p1) U (p2))))","2",3
|
||||
"F((p0) & (X((p1) U (p2))))","3",3
|
||||
"F((p0) & (X((p1) U (p2))))","4",3
|
||||
"F((p0) & (X((p1) U (p2))))","6",3
|
||||
"F((p0) & (X((p1) U (p2))))","7",3
|
||||
"!(F((p0) & (X((p1) U (p2)))))","1",2
|
||||
"!(F((p0) & (X((p1) U (p2)))))","2",2
|
||||
"!(F((p0) & (X((p1) U (p2)))))","3",2
|
||||
"!(F((p0) & (X((p1) U (p2)))))","4",2
|
||||
"!(F((p0) & (X((p1) U (p2)))))","6",2
|
||||
"!(F((p0) & (X((p1) U (p2)))))","7",2
|
||||
"F((p0) & (X((p1) & (X(F(p2))))))","1",4
|
||||
"F((p0) & (X((p1) & (X(F(p2))))))","2",4
|
||||
"F((p0) & (X((p1) & (X(F(p2))))))","3",4
|
||||
"F((p0) & (X((p1) & (X(F(p2))))))","4",4
|
||||
"F((p0) & (X((p1) & (X(F(p2))))))","6",4
|
||||
"F((p0) & (X((p1) & (X(F(p2))))))","7",4
|
||||
"!(F((p0) & (X((p1) & (X(F(p2)))))))","1",3
|
||||
"!(F((p0) & (X((p1) & (X(F(p2)))))))","2",3
|
||||
"!(F((p0) & (X((p1) & (X(F(p2)))))))","3",3
|
||||
"!(F((p0) & (X((p1) & (X(F(p2)))))))","4",3
|
||||
"!(F((p0) & (X((p1) & (X(F(p2)))))))","6",3
|
||||
"!(F((p0) & (X((p1) & (X(F(p2)))))))","7",3
|
||||
"(p0) U ((p1) & (X((p2) U (p3))))","1",4
|
||||
"(p0) U ((p1) & (X((p2) U (p3))))","2",4
|
||||
"(p0) U ((p1) & (X((p2) U (p3))))","3",4
|
||||
"(p0) U ((p1) & (X((p2) U (p3))))","4",4
|
||||
"(p0) U ((p1) & (X((p2) U (p3))))","6",4
|
||||
"(p0) U ((p1) & (X((p2) U (p3))))","7",4
|
||||
"!((p0) U ((p1) & (X((p2) U (p3)))))","1",4
|
||||
"!((p0) U ((p1) & (X((p2) U (p3)))))","2",4
|
||||
"!((p0) U ((p1) & (X((p2) U (p3)))))","3",4
|
||||
"!((p0) U ((p1) & (X((p2) U (p3)))))","4",4
|
||||
"!((p0) U ((p1) & (X((p2) U (p3)))))","6",4
|
||||
"!((p0) U ((p1) & (X((p2) U (p3)))))","7",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","1",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","2",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","3",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","4",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","6",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p2) -> (F(p3))))","7",4
|
||||
"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","1",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","2",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","3",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","4",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","6",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p2) -> (F(p3)))))","7",3
|
||||
"(G(F(p0))) & (G(F(p1)))","1",1
|
||||
"(G(F(p0))) & (G(F(p1)))","2",1
|
||||
"(G(F(p0))) & (G(F(p1)))","3",1
|
||||
"(G(F(p0))) & (G(F(p1)))","4",1
|
||||
"(G(F(p0))) & (G(F(p1)))","6",1
|
||||
"(G(F(p0))) & (G(F(p1)))","7",1
|
||||
"!((G(F(p0))) & (G(F(p1))))","1",3
|
||||
"!((G(F(p0))) & (G(F(p1))))","2",3
|
||||
"!((G(F(p0))) & (G(F(p1))))","3",3
|
||||
"!((G(F(p0))) & (G(F(p1))))","4",3
|
||||
"!((G(F(p0))) & (G(F(p1))))","6",3
|
||||
"!((G(F(p0))) & (G(F(p1))))","7",3
|
||||
"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","1",1
|
||||
"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","2",1
|
||||
"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","3",1
|
||||
"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","4",1
|
||||
"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","6",1
|
||||
"(G(F(p0))) | (G(F(p1))) | (G(F(p2)))","7",1
|
||||
"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","1",2
|
||||
"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","2",2
|
||||
"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","3",2
|
||||
"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","4",2
|
||||
"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","6",2
|
||||
"!((G(F(p0))) | (G(F(p1))) | (G(F(p2))))","7",2
|
||||
"G(F(p0))","1",1
|
||||
"G(F(p0))","2",1
|
||||
"G(F(p0))","3",1
|
||||
"G(F(p0))","4",1
|
||||
"G(F(p0))","6",1
|
||||
"G(F(p0))","7",1
|
||||
"!(G(F(p0)))","1",2
|
||||
"!(G(F(p0)))","2",2
|
||||
"!(G(F(p0)))","3",2
|
||||
"!(G(F(p0)))","4",2
|
||||
"!(G(F(p0)))","6",2
|
||||
"!(G(F(p0)))","7",2
|
||||
"(p0) U ((p1) U ((p2) U (p3)))","1",4
|
||||
"(p0) U ((p1) U ((p2) U (p3)))","2",4
|
||||
"(p0) U ((p1) U ((p2) U (p3)))","3",4
|
||||
"(p0) U ((p1) U ((p2) U (p3)))","4",4
|
||||
"(p0) U ((p1) U ((p2) U (p3)))","6",4
|
||||
"(p0) U ((p1) U ((p2) U (p3)))","7",4
|
||||
"!((p0) U ((p1) U ((p2) U (p3))))","1",4
|
||||
"!((p0) U ((p1) U ((p2) U (p3))))","2",4
|
||||
"!((p0) U ((p1) U ((p2) U (p3))))","3",4
|
||||
"!((p0) U ((p1) U ((p2) U (p3))))","4",4
|
||||
"!((p0) U ((p1) U ((p2) U (p3))))","6",4
|
||||
"!((p0) U ((p1) U ((p2) U (p3))))","7",4
|
||||
"(G((p0) -> (F(p1)))) & (G(p2))","1",2
|
||||
"(G((p0) -> (F(p1)))) & (G(p2))","2",2
|
||||
"(G((p0) -> (F(p1)))) & (G(p2))","3",2
|
||||
"(G((p0) -> (F(p1)))) & (G(p2))","4",2
|
||||
"(G((p0) -> (F(p1)))) & (G(p2))","6",2
|
||||
"(G((p0) -> (F(p1)))) & (G(p2))","7",2
|
||||
"!((G((p0) -> (F(p1)))) & (G(p2)))","1",3
|
||||
"!((G((p0) -> (F(p1)))) & (G(p2)))","2",3
|
||||
"!((G((p0) -> (F(p1)))) & (G(p2)))","3",3
|
||||
"!((G((p0) -> (F(p1)))) & (G(p2)))","4",3
|
||||
"!((G((p0) -> (F(p1)))) & (G(p2)))","6",3
|
||||
"!((G((p0) -> (F(p1)))) & (G(p2)))","7",3
|
||||
"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","1",4
|
||||
"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","2",4
|
||||
"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","3",4
|
||||
"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","4",4
|
||||
"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","6",4
|
||||
"((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1))))","7",4
|
||||
"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","1",3
|
||||
"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","2",3
|
||||
"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","3",3
|
||||
"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","4",3
|
||||
"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","6",3
|
||||
"!(((G(p0)) -> (F(p1))) & ((G(!(p0))) -> (F(!(p1)))))","7",3
|
||||
"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","1",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","2",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","3",4
|
||||
"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","4",3
|
||||
"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","6",3
|
||||
"(G((p0) -> (F(p1)))) & (G((p1) -> (F(p2))))","7",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","1",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","2",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","3",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","4",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","6",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((p1) -> (F(p2)))))","7",3
|
||||
"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","1",3
|
||||
"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","2",3
|
||||
"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","3",3
|
||||
"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","4",3
|
||||
"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","6",3
|
||||
"(G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1)))))","7",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","1",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","2",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","3",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","4",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","6",3
|
||||
"!((G((p0) -> (F(p1)))) & (G((!(p0)) -> (F(!(p1))))))","7",3
|
||||
"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","1",1
|
||||
"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","2",1
|
||||
"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","3",1
|
||||
"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","4",1
|
||||
"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","6",1
|
||||
"(G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3)))","7",1
|
||||
"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","1",5
|
||||
"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","2",5
|
||||
"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","3",5
|
||||
"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","4",5
|
||||
"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","6",5
|
||||
"!((G(F(p0))) & (G(F(p1))) & (G(F(p2))) & (G(F(p3))))","7",5
|
||||
"G((p0) -> ((p1) U (p2)))","1",2
|
||||
"G((p0) -> ((p1) U (p2)))","2",2
|
||||
"G((p0) -> ((p1) U (p2)))","3",2
|
||||
"G((p0) -> ((p1) U (p2)))","4",2
|
||||
"G((p0) -> ((p1) U (p2)))","6",2
|
||||
"G((p0) -> ((p1) U (p2)))","7",2
|
||||
"!(G((p0) -> ((p1) U (p2))))","1",3
|
||||
"!(G((p0) -> ((p1) U (p2))))","2",3
|
||||
"!(G((p0) -> ((p1) U (p2))))","3",3
|
||||
"!(G((p0) -> ((p1) U (p2))))","4",3
|
||||
"!(G((p0) -> ((p1) U (p2))))","6",3
|
||||
"!(G((p0) -> ((p1) U (p2))))","7",3
|
||||
"G(F((p0) <-> (X(X(p1)))))","1",9
|
||||
"G(F((p0) <-> (X(X(p1)))))","2",7
|
||||
"G(F((p0) <-> (X(X(p1)))))","3",4
|
||||
"G(F((p0) <-> (X(X(p1)))))","4",4
|
||||
"G(F((p0) <-> (X(X(p1)))))","6",4
|
||||
"G(F((p0) <-> (X(X(p1)))))","7",4
|
||||
"!(G(F((p0) <-> (X(X(p1))))))","1",7
|
||||
"!(G(F((p0) <-> (X(X(p1))))))","2",7
|
||||
"!(G(F((p0) <-> (X(X(p1))))))","3",7
|
||||
"!(G(F((p0) <-> (X(X(p1))))))","4",7
|
||||
"!(G(F((p0) <-> (X(X(p1))))))","6",7
|
||||
"!(G(F((p0) <-> (X(X(p1))))))","7",7
|
||||
"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","1",1
|
||||
"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","2",1
|
||||
"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","3",1
|
||||
"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","4",1
|
||||
"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","6",1
|
||||
"(G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0))))","7",1
|
||||
"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","1",2
|
||||
"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","2",2
|
||||
"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","3",2
|
||||
"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","4",2
|
||||
"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","6",2
|
||||
"!((G(!(p0))) & (G((p1) -> (F(p2)))) & (G((p2) -> (F(p0)))))","7",2
|
||||
"G((p0) -> (X(X(X(p1)))))","1",8
|
||||
"G((p0) -> (X(X(X(p1)))))","2",8
|
||||
"G((p0) -> (X(X(X(p1)))))","3",8
|
||||
"G((p0) -> (X(X(X(p1)))))","4",8
|
||||
"G((p0) -> (X(X(X(p1)))))","6",8
|
||||
"G((p0) -> (X(X(X(p1)))))","7",8
|
||||
"!(G((p0) -> (X(X(X(p1))))))","1",9
|
||||
"!(G((p0) -> (X(X(X(p1))))))","2",9
|
||||
"!(G((p0) -> (X(X(X(p1))))))","3",9
|
||||
"!(G((p0) -> (X(X(X(p1))))))","4",9
|
||||
"!(G((p0) -> (X(X(X(p1))))))","6",9
|
||||
"!(G((p0) -> (X(X(X(p1))))))","7",9
|
||||
"G((p0) -> (F(p1)))","1",2
|
||||
"G((p0) -> (F(p1)))","2",2
|
||||
"G((p0) -> (F(p1)))","3",2
|
||||
"G((p0) -> (F(p1)))","4",2
|
||||
"G((p0) -> (F(p1)))","6",2
|
||||
"G((p0) -> (F(p1)))","7",2
|
||||
"!(G((p0) -> (F(p1))))","1",2
|
||||
"!(G((p0) -> (F(p1))))","2",2
|
||||
"!(G((p0) -> (F(p1))))","3",2
|
||||
"!(G((p0) -> (F(p1))))","4",2
|
||||
"!(G((p0) -> (F(p1))))","6",2
|
||||
"!(G((p0) -> (F(p1))))","7",2
|
||||
"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","1",1
|
||||
"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","2",1
|
||||
"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","3",1
|
||||
"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","4",1
|
||||
"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","6",1
|
||||
"G((p0) U ((p1) U ((!(p0)) U (!(p1)))))","7",1
|
||||
"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","1",2
|
||||
"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","2",2
|
||||
"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","3",2
|
||||
"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","4",2
|
||||
"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","6",2
|
||||
"!(G((p0) U ((p1) U ((!(p0)) U (!(p1))))))","7",2
|
||||
"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","1",4
|
||||
"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","2",5
|
||||
"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","3",5
|
||||
"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","4",5
|
||||
"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","6",5
|
||||
"X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1))","7",5
|
||||
"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","1",6
|
||||
"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","2",6
|
||||
"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","3",6
|
||||
"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","4",6
|
||||
"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","6",6
|
||||
"!(X((((p0) & (p1)) R ((!(p0)) U (!(p2)))) R (p1)))","7",6
|
||||
"((!(p0)) M (!(p1))) W (F(!(p2)))","1",4
|
||||
"((!(p0)) M (!(p1))) W (F(!(p2)))","2",5
|
||||
"((!(p0)) M (!(p1))) W (F(!(p2)))","3",3
|
||||
"((!(p0)) M (!(p1))) W (F(!(p2)))","4",3
|
||||
"((!(p0)) M (!(p1))) W (F(!(p2)))","6",3
|
||||
"((!(p0)) M (!(p1))) W (F(!(p2)))","7",3
|
||||
"!(((!(p0)) M (!(p1))) W (F(!(p2))))","1",3
|
||||
"!(((!(p0)) M (!(p1))) W (F(!(p2))))","2",3
|
||||
"!(((!(p0)) M (!(p1))) W (F(!(p2))))","3",3
|
||||
"!(((!(p0)) M (!(p1))) W (F(!(p2))))","4",3
|
||||
"!(((!(p0)) M (!(p1))) W (F(!(p2))))","6",3
|
||||
"!(((!(p0)) M (!(p1))) W (F(!(p2))))","7",3
|
||||
"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","1",2
|
||||
"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","2",3
|
||||
"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","3",3
|
||||
"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","4",3
|
||||
"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","6",3
|
||||
"((p0) & (F(p1)) & (G(F(p2)))) R (p1)","7",3
|
||||
"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","1",5
|
||||
"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","2",5
|
||||
"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","3",5
|
||||
"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","4",5
|
||||
"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","6",5
|
||||
"!(((p0) & (F(p1)) & (G(F(p2)))) R (p1))","7",5
|
||||
"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","1",3
|
||||
"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","2",2
|
||||
"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","3",2
|
||||
"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","4",2
|
||||
"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","6",2
|
||||
"((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2))))","7",2
|
||||
"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","1",4
|
||||
"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","2",4
|
||||
"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","3",4
|
||||
"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","4",4
|
||||
"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","6",4
|
||||
"!(((p0) R ((p1) W (p0))) W (G((!(p0)) M ((p1) | (p2)))))","7",4
|
||||
"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","1",5
|
||||
"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","2",7
|
||||
"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","3",6
|
||||
"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","4",6
|
||||
"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","6",6
|
||||
"X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0))))))","7",6
|
||||
"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","1",8
|
||||
"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","2",8
|
||||
"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","3",8
|
||||
"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","4",8
|
||||
"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","6",8
|
||||
"!(X((G((!(p0)) M (!(p1)))) | (G((p0) | (G(!(p0)))))))","7",8
|
||||
"(F(p0)) W (G(p1))","1",3
|
||||
"(F(p0)) W (G(p1))","2",2
|
||||
"(F(p0)) W (G(p1))","3",2
|
||||
"(F(p0)) W (G(p1))","4",2
|
||||
"(F(p0)) W (G(p1))","6",2
|
||||
"(F(p0)) W (G(p1))","7",2
|
||||
"!((F(p0)) W (G(p1)))","1",2
|
||||
"!((F(p0)) W (G(p1)))","2",2
|
||||
"!((F(p0)) W (G(p1)))","3",2
|
||||
"!((F(p0)) W (G(p1)))","4",2
|
||||
"!((F(p0)) W (G(p1)))","6",2
|
||||
"!((F(p0)) W (G(p1)))","7",2
|
||||
"(G(F(p1))) | (G(p0))","1",3
|
||||
"(G(F(p1))) | (G(p0))","2",3
|
||||
"(G(F(p1))) | (G(p0))","3",2
|
||||
"(G(F(p1))) | (G(p0))","4",2
|
||||
"(G(F(p1))) | (G(p0))","6",2
|
||||
"(G(F(p1))) | (G(p0))","7",2
|
||||
"!((G(F(p1))) | (G(p0)))","1",3
|
||||
"!((G(F(p1))) | (G(p0)))","2",3
|
||||
"!((G(F(p1))) | (G(p0)))","3",3
|
||||
"!((G(F(p1))) | (G(p0)))","4",3
|
||||
"!((G(F(p1))) | (G(p0)))","6",3
|
||||
"!((G(F(p1))) | (G(p0)))","7",3
|
||||
"(p0) M (G((F(!(p1))) | (X(!(p0)))))","1",5
|
||||
"(p0) M (G((F(!(p1))) | (X(!(p0)))))","2",5
|
||||
"(p0) M (G((F(!(p1))) | (X(!(p0)))))","3",5
|
||||
"(p0) M (G((F(!(p1))) | (X(!(p0)))))","4",5
|
||||
"(p0) M (G((F(!(p1))) | (X(!(p0)))))","6",5
|
||||
"(p0) M (G((F(!(p1))) | (X(!(p0)))))","7",5
|
||||
"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","1",4
|
||||
"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","2",4
|
||||
"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","3",4
|
||||
"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","4",4
|
||||
"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","6",4
|
||||
"!((p0) M (G((F(!(p1))) | (X(!(p0))))))","7",4
|
||||
"(G(!(p0))) R (X(F(p1)))","1",4
|
||||
"(G(!(p0))) R (X(F(p1)))","2",4
|
||||
"(G(!(p0))) R (X(F(p1)))","3",3
|
||||
"(G(!(p0))) R (X(F(p1)))","4",3
|
||||
"(G(!(p0))) R (X(F(p1)))","6",3
|
||||
"(G(!(p0))) R (X(F(p1)))","7",3
|
||||
"!((G(!(p0))) R (X(F(p1))))","1",3
|
||||
"!((G(!(p0))) R (X(F(p1))))","2",3
|
||||
"!((G(!(p0))) R (X(F(p1))))","3",3
|
||||
"!((G(!(p0))) R (X(F(p1))))","4",3
|
||||
"!((G(!(p0))) R (X(F(p1))))","6",3
|
||||
"!((G(!(p0))) R (X(F(p1))))","7",3
|
||||
"X(F((!(p0)) | (G(F(p1)))))","1",4
|
||||
"X(F((!(p0)) | (G(F(p1)))))","2",4
|
||||
"X(F((!(p0)) | (G(F(p1)))))","3",3
|
||||
"X(F((!(p0)) | (G(F(p1)))))","4",3
|
||||
"X(F((!(p0)) | (G(F(p1)))))","6",3
|
||||
"X(F((!(p0)) | (G(F(p1)))))","7",3
|
||||
"!(X(F((!(p0)) | (G(F(p1))))))","1",3
|
||||
"!(X(F((!(p0)) | (G(F(p1))))))","2",3
|
||||
"!(X(F((!(p0)) | (G(F(p1))))))","3",3
|
||||
"!(X(F((!(p0)) | (G(F(p1))))))","4",3
|
||||
"!(X(F((!(p0)) | (G(F(p1))))))","6",3
|
||||
"!(X(F((!(p0)) | (G(F(p1))))))","7",3
|
||||
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","1",6
|
||||
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","2",6
|
||||
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","3",5
|
||||
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","4",5
|
||||
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","6",5
|
||||
"(G((F(!(p0))) U (!(p0)))) U (X(p0))","7",5
|
||||
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","1",5
|
||||
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","2",5
|
||||
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","3",5
|
||||
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","4",5
|
||||
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","6",5
|
||||
"!((G((F(!(p0))) U (!(p0)))) U (X(p0)))","7",5
|
||||
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","1",4
|
||||
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","2",5
|
||||
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","3",4
|
||||
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","4",4
|
||||
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","6",4
|
||||
"((p0) | (G((p0) M (!(p1))))) W (F(p2))","7",4
|
||||
"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","1",4
|
||||
"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","2",4
|
||||
"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","3",4
|
||||
"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","4",4
|
||||
"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","6",4
|
||||
"!(((p0) | (G((p0) M (!(p1))))) W (F(p2)))","7",4
|
||||
"(F(p0)) W (X(p1))","1",6
|
||||
"(F(p0)) W (X(p1))","2",6
|
||||
"(F(p0)) W (X(p1))","3",6
|
||||
"(F(p0)) W (X(p1))","4",6
|
||||
"(F(p0)) W (X(p1))","6",6
|
||||
"(F(p0)) W (X(p1))","7",6
|
||||
"!((F(p0)) W (X(p1)))","1",4
|
||||
"!((F(p0)) W (X(p1)))","2",4
|
||||
"!((F(p0)) W (X(p1)))","3",4
|
||||
"!((F(p0)) W (X(p1)))","4",4
|
||||
"!((F(p0)) W (X(p1)))","6",4
|
||||
"!((F(p0)) W (X(p1)))","7",4
|
||||
"(X(G(!(p0)))) R (F(p1))","1",2
|
||||
"(X(G(!(p0)))) R (F(p1))","2",2
|
||||
"(X(G(!(p0)))) R (F(p1))","3",2
|
||||
"(X(G(!(p0)))) R (F(p1))","4",2
|
||||
"(X(G(!(p0)))) R (F(p1))","6",2
|
||||
"(X(G(!(p0)))) R (F(p1))","7",2
|
||||
"!((X(G(!(p0)))) R (F(p1)))","1",3
|
||||
"!((X(G(!(p0)))) R (F(p1)))","2",3
|
||||
"!((X(G(!(p0)))) R (F(p1)))","3",3
|
||||
"!((X(G(!(p0)))) R (F(p1)))","4",3
|
||||
"!((X(G(!(p0)))) R (F(p1)))","6",3
|
||||
"!((X(G(!(p0)))) R (F(p1)))","7",3
|
||||
"(G(F(p0))) | ((p1) & (F(p2)))","1",4
|
||||
"(G(F(p0))) | ((p1) & (F(p2)))","2",4
|
||||
"(G(F(p0))) | ((p1) & (F(p2)))","3",4
|
||||
"(G(F(p0))) | ((p1) & (F(p2)))","4",4
|
||||
"(G(F(p0))) | ((p1) & (F(p2)))","6",4
|
||||
"(G(F(p0))) | ((p1) & (F(p2)))","7",4
|
||||
"!((G(F(p0))) | ((p1) & (F(p2))))","1",5
|
||||
"!((G(F(p0))) | ((p1) & (F(p2))))","2",5
|
||||
"!((G(F(p0))) | ((p1) & (F(p2))))","3",5
|
||||
"!((G(F(p0))) | ((p1) & (F(p2))))","4",5
|
||||
"!((G(F(p0))) | ((p1) & (F(p2))))","6",5
|
||||
"!((G(F(p0))) | ((p1) & (F(p2))))","7",5
|
||||
"X((p0) R ((F(p1)) R (F(!(p1)))))","1",6
|
||||
"X((p0) R ((F(p1)) R (F(!(p1)))))","2",6
|
||||
"X((p0) R ((F(p1)) R (F(!(p1)))))","3",4
|
||||
"X((p0) R ((F(p1)) R (F(!(p1)))))","4",4
|
||||
"X((p0) R ((F(p1)) R (F(!(p1)))))","6",4
|
||||
"X((p0) R ((F(p1)) R (F(!(p1)))))","7",4
|
||||
"!(X((p0) R ((F(p1)) R (F(!(p1))))))","1",3
|
||||
"!(X((p0) R ((F(p1)) R (F(!(p1))))))","2",3
|
||||
"!(X((p0) R ((F(p1)) R (F(!(p1))))))","3",3
|
||||
"!(X((p0) R ((F(p1)) R (F(!(p1))))))","4",3
|
||||
"!(X((p0) R ((F(p1)) R (F(!(p1))))))","6",3
|
||||
"!(X((p0) R ((F(p1)) R (F(!(p1))))))","7",3
|
||||
"G((X(p0)) M (F(p0)))","1",2
|
||||
"G((X(p0)) M (F(p0)))","2",2
|
||||
"G((X(p0)) M (F(p0)))","3",1
|
||||
"G((X(p0)) M (F(p0)))","4",1
|
||||
"G((X(p0)) M (F(p0)))","6",1
|
||||
"G((X(p0)) M (F(p0)))","7",1
|
||||
"!(G((X(p0)) M (F(p0))))","1",2
|
||||
"!(G((X(p0)) M (F(p0))))","2",2
|
||||
"!(G((X(p0)) M (F(p0))))","3",2
|
||||
"!(G((X(p0)) M (F(p0))))","4",2
|
||||
"!(G((X(p0)) M (F(p0))))","6",2
|
||||
"!(G((X(p0)) M (F(p0))))","7",2
|
||||
"X((G(F(p1))) | (G(p0)))","1",4
|
||||
"X((G(F(p1))) | (G(p0)))","2",4
|
||||
"X((G(F(p1))) | (G(p0)))","3",3
|
||||
"X((G(F(p1))) | (G(p0)))","4",3
|
||||
"X((G(F(p1))) | (G(p0)))","6",3
|
||||
"X((G(F(p1))) | (G(p0)))","7",3
|
||||
"!(X((G(F(p1))) | (G(p0))))","1",4
|
||||
"!(X((G(F(p1))) | (G(p0))))","2",4
|
||||
"!(X((G(F(p1))) | (G(p0))))","3",4
|
||||
"!(X((G(F(p1))) | (G(p0))))","4",4
|
||||
"!(X((G(F(p1))) | (G(p0))))","6",4
|
||||
"!(X((G(F(p1))) | (G(p0))))","7",4
|
||||
"(G(p0)) R (F(p1))","1",2
|
||||
"(G(p0)) R (F(p1))","2",2
|
||||
"(G(p0)) R (F(p1))","3",2
|
||||
"(G(p0)) R (F(p1))","4",2
|
||||
"(G(p0)) R (F(p1))","6",2
|
||||
"(G(p0)) R (F(p1))","7",2
|
||||
"!((G(p0)) R (F(p1)))","1",3
|
||||
"!((G(p0)) R (F(p1)))","2",3
|
||||
"!((G(p0)) R (F(p1)))","3",3
|
||||
"!((G(p0)) R (F(p1)))","4",3
|
||||
"!((G(p0)) R (F(p1)))","6",3
|
||||
"!((G(p0)) R (F(p1)))","7",3
|
||||
"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","1",2
|
||||
"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","2",3
|
||||
"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","3",2
|
||||
"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","4",2
|
||||
"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","6",2
|
||||
"G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2))))))","7",2
|
||||
"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","1",4
|
||||
"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","2",4
|
||||
"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","3",4
|
||||
"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","4",4
|
||||
"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","6",4
|
||||
"!(G((p0) U ((p1) | (X(((!(p0)) & (!(p2))) | ((p0) & (p2)))))))","7",4
|
||||
"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","1",4
|
||||
"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","2",5
|
||||
"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","3",5
|
||||
"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","4",5
|
||||
"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","6",5
|
||||
"X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1))))))","7",5
|
||||
"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","1",7
|
||||
"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","2",7
|
||||
"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","3",7
|
||||
"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","4",7
|
||||
"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","6",7
|
||||
"!(X(G(((G(!(p0))) & (F(!(p1)))) | ((F(p0)) & ((p0) | (G(p1)))))))","7",7
|
||||
"X((G(F(p0))) | (G(!(p0))))","1",4
|
||||
"X((G(F(p0))) | (G(!(p0))))","2",4
|
||||
"X((G(F(p0))) | (G(!(p0))))","3",3
|
||||
"X((G(F(p0))) | (G(!(p0))))","4",3
|
||||
"X((G(F(p0))) | (G(!(p0))))","6",3
|
||||
"X((G(F(p0))) | (G(!(p0))))","7",3
|
||||
"!(X((G(F(p0))) | (G(!(p0)))))","1",4
|
||||
"!(X((G(F(p0))) | (G(!(p0)))))","2",4
|
||||
"!(X((G(F(p0))) | (G(!(p0)))))","3",4
|
||||
"!(X((G(F(p0))) | (G(!(p0)))))","4",4
|
||||
"!(X((G(F(p0))) | (G(!(p0)))))","6",4
|
||||
"!(X((G(F(p0))) | (G(!(p0)))))","7",4
|
||||
"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","1",4
|
||||
"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","2",4
|
||||
"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","3",4
|
||||
"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","4",4
|
||||
"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","6",4
|
||||
"G((G(!(p0))) | (F(!(p1))) | (G(!(p2))))","7",4
|
||||
"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","1",4
|
||||
"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","2",4
|
||||
"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","3",4
|
||||
"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","4",4
|
||||
"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","6",4
|
||||
"!(G((G(!(p0))) | (F(!(p1))) | (G(!(p2)))))","7",4
|
||||
"G((p0) | (F(p0)))","1",1
|
||||
"G((p0) | (F(p0)))","2",1
|
||||
"G((p0) | (F(p0)))","3",1
|
||||
"G((p0) | (F(p0)))","4",1
|
||||
"G((p0) | (F(p0)))","6",1
|
||||
"G((p0) | (F(p0)))","7",1
|
||||
"!(G((p0) | (F(p0))))","1",2
|
||||
"!(G((p0) | (F(p0))))","2",2
|
||||
"!(G((p0) | (F(p0))))","3",2
|
||||
"!(G((p0) | (F(p0))))","4",2
|
||||
"!(G((p0) | (F(p0))))","6",2
|
||||
"!(G((p0) | (F(p0))))","7",2
|
||||
EOF
|
||||
|
||||
diff expected extracted
|
||||
|
|
|
|||
|
|
@ -21,9 +21,6 @@
|
|||
. ./defs
|
||||
set -e
|
||||
|
||||
# Skip if $SATSOLVE is not installed.
|
||||
(${SATSOLVER-glucose} --help >/dev/null 2>&1) || exit 77
|
||||
|
||||
autfilt=autfilt
|
||||
ltlfilt=ltlfilt
|
||||
|
||||
|
|
@ -152,8 +149,8 @@ properties: trans-labels explicit-labels trans-acc colored complete
|
|||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 0 {0}
|
||||
[!0] 0 {1}
|
||||
[!0] 0 {0}
|
||||
[0] 0 {1}
|
||||
--END--
|
||||
EOF
|
||||
|
||||
|
|
|
|||
|
|
@ -17,13 +17,8 @@
|
|||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
import shutil
|
||||
import sys
|
||||
import spot
|
||||
|
||||
# Ignore the test if glucose is not installed.
|
||||
if shutil.which("glucose") == None:
|
||||
sys.exit(77)
|
||||
|
||||
aut = spot.translate('GFa & GFb', 'BA')
|
||||
assert aut.num_sets() == 1
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue