update 3b fixed

[ar1516.git] / a2 / src / 1.bak

diff --git a/a2/src/1.bak b/a2/src/1.bak
deleted file mode 100644 (file)
index 2966704..0000000
--- a/a2/src/1.bak
+++ /dev/null
@@ -1,126 +0,0 @@
-#!/bin/bash
-YICES=~/projects/yices-2.4.2/bin/yices-smt
-AI=40
-BI=30
-CI=145
-AMAX=120
-BMAX=120
-CMAX=200
-
-function generate {
-       ITERATIONS=$1
-       TMAX=$2
-       cat<<GEN
-(benchmark a1.smt
-:logic QF_UFLIA
-:extrafuns (
-$(     for i in $(seq 0 $ITERATIONS); do
-               echo -e "\t(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) (d$i Int) (p$i Int)"
-       done)
-)
-:formula
-(and
-       ;-- PRECONDITION
-       (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TMAX) (= l0 0) (= d0 0) (= p0 0))
-GEN
-       for i in $(seq 1 $ITERATIONS); do
-               cat<<GEN
-       (> a$i 0)
-       (> b$i 0)
-       (> c$i 0)
-       (or ;-- ITERATION $i
-               (and ;-- SPECIAL CASE FOR STATE S(0)
-                       (= l$i 0)
-                       (= d$i 0)
-                       (= t$i $TMAX)
-                       (= a$i (- a$((i-1)) p$i))
-                       (= b$i (- b$((i-1)) p$i))
-                       (= c$i (- c$((i-1)) p$i))
-                       (or
-                               (and ;-- CAME FROM A
-                                       (= l$((i-1)) 1)
-                                       (= p$i 29)
-                               )
-                               (and ;-- CAME FROM B
-                                       (= l$((i-1)) 2)
-                                       (= p$i 21)
-                               )
-                       )
-               )
-               (and ;-- CASE FOR STATE A(1)
-                       (= l$i 1) 
-                       (>= d$i 0) (<= d$i t$((i-1)))
-                       (<= d$i (+ p$i (- $AMAX a$((i-1)))))
-                       (= t$i (- t$((i-1)) d$i))
-                       (= a$i (- (+ a$((i-1)) d$i) p$i))
-
-                       (= b$i (- b$((i-1)) p$i))
-                       (= c$i (- c$((i-1)) p$i))
-                       (or
-                               (and  ;-- CAME FROM S(0)
-                                       (= l$((i-1)) 0)
-                                       (= p$i 29)
-                               ) (and  ;-- CAME FROM B(2)
-                                       (= p$i 17)
-                                       (= l$((i-1)) 2)
-                               ) (and ;-- CAME FROM C(3)
-                                       (= p$i 32)
-                                       (= l$((i-1)) 3)
-                               )
-                       )
-               )
-               (and ;-- CASE FOR STATE B(2)
-                       (= l$i 3)
-                       (>= d$i 0) (<= d$i t$((i-1)))
-                       (<= d$i (+ p$i (- $BMAX b$((i-1)))))
-                       (= t$i (- t$((i-1)) d$i))
-                       (= b$i (- (+ b$((i-1)) d$i) p$i))
-
-                       (= a$i (- a$((i-1)) p$i))
-                       (= c$i (- c$((i-1)) p$i))
-
-                       (or
-                               (and  ;-- CAME FROM S(0)
-                                       (= l$((i-1)) 0)
-                                       (= p$i 21)
-                               ) (and  ;-- CAME FROM A(1)
-                                       (= l$((i-1)) 1)
-                                       (= p$i 17)
-                               ) (and ;-- CAME FROM C(3)
-                                       (= l$((i-1)) 3)
-                                       (= p$i 37)
-                               )
-                       )
-               )
-               (and ;-- CASE FOR STATE C(3)
-                       (= l$i 3)
-                       (>= d$i 0) (<= d$i t$((i-1)))
-                       (<= d$i (+ p$i (- $CMAX c$((i-1)))))
-                       (= t$i (- t$((i-1)) d$i))
-                       (= c$i (- (+ c$((i-1)) d$i) p$i))
-                       (= a$i (- a$((i-1)) p$i))
-                       (= b$i (- b$((i-1)) p$i))
-                       (or
-                               (and  ;-- CAME FROM A(1)
-                                       (= l$((i-1)) 1)
-                                       (= p$i 32)
-                               ) (and ;-- CAME FROM B(2)
-                                       (= l$((i-1)) 2)
-                                       (= p$i 37)
-                               )
-                       )
-               )
-       )
-GEN
-       done
-       cat<<GEN
-))
-GEN
-}
-it=1
-until generate $it 300 | $YICES | grep "unsat"
-do
-       echo $((it++))
-done
-generate 9 300 | $YICES -m | sort
-echo $it