(> a$i 0)
(> b$i 0)
(> c$i 0)
+ (>= d$i 0)
+ (<= d$i $TMAX)
+ (>= t$i 0)
+ (<= t$i $TMAX)
(or ;-- ITERATION $i
- (and ;-- SPECIAL CASE FOR STATE S(0)
- (= l$i 0)
- (= d$i 0)
- (= t$i $TMAX)
+ (and ;-- WAS IN S
+ (= l$((i-1)) 0)
(or
- (and ;-- CAME FROM A
- (= l$((i-1)) 1)
- (= a$i (- a$((i-1)) 29))
+ (and ; now in A
+ (>= a$((i-1)) 29)
+ (= l$i 1)
+ (<= d$i (+ 29 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 29) d$i))
+
(= b$i (- b$((i-1)) 29))
(= c$i (- c$((i-1)) 29))
- )
- (and ;-- CAME FROM B
- (= l$((i-1)) 2)
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (>= b$((i-1)) 21)
+ (= l$i 2)
+ (<= d$i (+ 21 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 21) d$i))
+
(= a$i (- a$((i-1)) 21))
- (= b$i (- b$((i-1)) 21))
(= c$i (- c$((i-1)) 21))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
- (and ;-- CASE FOR STATE A(1)
- (= l$i 1)
- (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $AMAX a$((i-1))))
- (= t$i (- t$((i-1)) d$i)) (= a$i (+ a$((i-1)) d$i))
-
+ (and ;-- WAS IN A
+ (= l$((i-1)) 1)
(or
- (and ;-- CAME FROM S(0)
- (= l$((i-1)) 0)
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
+ (= a$i (- a$((i-1)) 29))
(= b$i (- b$((i-1)) 29))
- (= c$i (- c$((i-1)) 29))
- ) (and ;-- CAME FROM B(2)
- (= l$((i-1)) 2)
- (= b$i (- b$((i-1)) 17))
+ (= c$i (- c$((i-1)) 29))
+
+ (= t$i $TMAX)
+ ) (and ; now in B
+ (>= b$((i-1)) 17)
+ (= l$i 2)
+ (<= d$i (+ 17 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 17) d$i))
+
+ (= a$i (- a$((i-1)) 17))
(= c$i (- c$((i-1)) 17))
- ) (and ;-- CAME FROM C(3)
- (= l$((i-1)) 3)
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (>= c$((i-1)) 32)
+ (= l$i 3)
+
+ (<= d$i (+ 32 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 32) d$i))
+
+ (= a$i (- a$((i-1)) 32))
(= b$i (- b$((i-1)) 32))
- (= c$i (- c$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
- (and ;-- CASE FOR STATE B(2)
- (= l$i 2)
- (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $BMAX b$((i-1))))
- (= t$i (- t$((i-1)) d$i)) (= b$i (+ b$((i-1)) d$i))
-
+ (and ;-- WAS IN B
+ (= l$((i-1)) 2)
(or
- (and ;-- CAME FROM S(0)
- (= l$((i-1)) 0)
+ (and ; now in S
+ (= l$i 0)
+ (= d$i 0)
+
(= a$i (- a$((i-1)) 21))
- (= c$i (- c$((i-1)) 21))
- ) (and ;-- CAME FROM A(1)
- (= l$((i-1)) 1)
- (= a$i (- a$((i-1)) 17))
+ (= b$i (- b$((i-1)) 21))
+ (= c$i (- c$((i-1)) 21))
+
+ (= t$i $TMAX)
+ ) (and ; now in A
+ (>= a$((i-1)) 17)
+ (= l$i 1)
+ (<= d$i (+ 17 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 17) d$i))
+
+ (= b$i (- b$((i-1)) 17))
(= c$i (- c$((i-1)) 17))
- ) (and ;-- CAME FROM C(3)
- (= l$((i-1)) 3)
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in C
+ (>= c$((i-1)) 37)
+ (= l$i 3)
+ (<= d$i (+ 37 (- $CMAX c$((i-1)))))
+ (= c$i (+ (- c$((i-1)) 37) d$i))
+
(= a$i (- a$((i-1)) 37))
- (= c$i (- c$((i-1)) 37))
+ (= b$i (- b$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
- (and ;-- CASE FOR STATE C(3)
- (= l$i 3)
- (>= d$i 0) (<= d$i t$((i-1))) (<= d$i (- $CMAX c$((i-1))))
- (= t$i (- t$((i-1)) d$i)) (= c$i (+ c$((i-1)) d$i))
-
+ (and ;-- WAS IN C
+ (= l$((i-1)) 3)
(or
- (and ;-- CAME FROM A(1)
- (= l$((i-1)) 1)
- (= a$i (- a$((i-1)) 32))
+ (and ; now in A
+ (>= a$((i-1)) 32)
+ (= l$i 1)
+ (<= d$i (+ 32 (- $AMAX a$((i-1)))))
+ (= a$i (+ (- a$((i-1)) 32) d$i))
+
(= b$i (- b$((i-1)) 32))
- ) (and ;-- CAME FROM B(2)
- (= l$((i-1)) 2)
+ (= c$i (- c$((i-1)) 32))
+
+ (= t$i (- t$((i-1)) d$i))
+ ) (and ; now in B
+ (>= b$((i-1)) 37)
+ (= l$i 2)
+ (<= d$i (+ 37 (- $BMAX b$((i-1)))))
+ (= b$i (+ (- b$((i-1)) 37) d$i))
+
(= a$i (- a$((i-1)) 37))
- (= b$i (- b$((i-1)) 37))
+ (= c$i (- c$((i-1)) 37))
+
+ (= t$i (- t$((i-1)) d$i))
)
)
)
done
echo ")))"
}
-
it=1
-while generate $it 320 | $YICES -m | pee sort "grep unsat"
+while generate $it 320 | $YICES -m | pee sort "grep -q unsat"
do
- it=$((it+1))
+ echo $((it++))
done
-echo $it
repositories / ar1516.git / blobdiff