update

diff --git a/a2/1.tex b/a2/1.tex
index 94a01cb..67a214c 100644 (file)
--- a/a2/1.tex
+++ b/a2/1.tex
@@ -24,7 +24,7 @@ Iteration $0$ depicts the initial state and can be described with a simple
 conjuction:
 $$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
 
-After that all iteration can be formalized as
+After that all iterations can be formalized as
 $$\begin{array}{lrl}
        \bigwedge_{i\in I} \Bigg(
        % Bent in S

diff --git a/a2/2.tex b/a2/2.tex
index 16530db..414669b 100644 (file)
--- a/a2/2.tex
+++ b/a2/2.tex
@@ -46,7 +46,7 @@ joining them with logical or operators.
 
                The solution described in \autoref{tab:sol2a} is found by
                \textsc{NuSMV} within $0.29$ seconds.
-               \begin{table}[h]
+               \begin{table}[ht]
                        \centering\small
                        \begin{tabular}{rrrrl}
                                \toprule
@@ -85,7 +85,7 @@ joining them with logical or operators.
        
                The solution described in \autoref{tab:sol2c} is found by
                \textsc{NuSMV} within $1.8$ seconds.
-               \begin{table}[h]
+               \begin{table}[ht]
                        \centering\small
                        \begin{tabular}{rrrrl}
                                \toprule

diff --git a/a2/4.tex b/a2/4.tex
index e69de29..15029d5 100644 (file)
--- a/a2/4.tex
+++ b/a2/4.tex
@@ -0,0 +1,2 @@
+\section{Solving solitaire}
+Solitaire

diff --git a/a2/src/1.bash b/a2/src/1.bash
index f9ed186..b1e02ff 100755 (executable)
--- a/a2/src/1.bash
+++ b/a2/src/1.bash
@@ -1,83 +1,49 @@
 #!/bin/bash
-AINIT=40
-BINIT=30
-CINIT=145
+AI=40
+BI=30
+CI=145
+TI=300
 AMAX=120
 BMAX=120
 CMAX=200
 TMAX=300
-TINIT=300
-TLOC=0
 
-PLACES=s a b c
-STATES=5
+ITERATIONS=1
 
 function generate {
-       local i j
        cat<<GEN
 (benchmark a1.smt
 :logic QF_UFLIA
 :extrafuns (
-GEN
-       for i in $(seq 0 $STATES); do
-               echo "(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) ) (d$i Int)"
-       done
-       cat <<GEN
+$(     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)"
+       done)
 )
 :formula
 (and
-       (and 
-               (= a0 $AINIT)
-               (= b0 $BINIT)
-               (= c0 $CINIT)
-               (= t0 $TINIT)
-               (= l0 0) 
-               (= d0 0)
-       )
+       -- PRECONDITION
+       (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TI) (= l0 0) (= d0 0))
 GEN
-       for i in $(seq $STATES); do
-               j=$((i-1))
-               echo "State: $i, prev: $j"
-               echo "(or"
-#
-               #Truck is in S
+       for i in $(seq 1 $ITERATIONS); do
                cat<<GEN
+       -- SPECIAL CASE FOR STATE S(0)
+       (= l$i 0) (= d$i 0) (= t$i $TMAX)
        (or
-; Truck is in S
-               (and
-                       (= l$j 0)
-                       (or
-               ; Truck can go to B
-                               (and
-                                       (= l$i 2)
-                                       (and
-                                               (> d$i 0)
-                                               (<= d$i t$j)
-                                               (<= d$i (- $AMAX a$j))
-                                       )
-                                       (= a$j (
-                                       (= b$i (- b$j 29))
-                                       (= c$i (- b$j 29))
-                               )
-               ; Truck can go to A
-                               (= l$i 1)
-                               )
-                       )
-; Truck is in A
-               (and
-                       (= l$j 1)
+               (and -- Comes from A
+                       (= l$((i-1)) 1)
+                       (= a$i (- a$((i-1)) 29)
+                       (= b$i (- b$((i-1)) 29)
+                       (= c$i (- c$((i-1)) 29)
                )
-; Truck is in B
-               (and
-                       (= l$j 2)
-               )
-; Truck is in C
-               (and
-                       (= l$j 3)
+               (and -- Comes from B
+                       (= l$((i-1)) 2)
+                       (= a$i (- a$((i-1)) 21)
+                       (= b$i (- b$((i-1)) 21)
+                       (= c$i (- c$((i-1)) 21)
                )
        )
 GEN
-       done    
+       done
        echo "))"
 }
 #time generate | yices-smt -m | python3 src/a2.py > $1

diff --git a/a2/src/4.py b/a2/src/4.py
new file mode 100644 (file)
index 0000000..b0b30f5
--- /dev/null
+++ b/a2/src/4.py
@@ -0,0 +1,32 @@
+#!/bin/env python
+pegs = [(x, y) for x in range(7) for y in range(7) if
+        not (
+        (x < 2 and y < 2) or # exclude topleft
+        (x > 4 and y > 4) or # exclude bottomright
+        (x > 4 and y < 2) or # exclude topright
+        (x < 2 and y > 4))   # exclude bottomleft
+        ]
+holes = [(3,3)]
+var = ' '.join('p{}: boolean;'.format(i) for i in range(len(pegs)))
+init = ' & '.join('p{}={}'.format(i, 
+    'FALSE' if pegs[i] in holes else 'TRUE') for i in range(len(pegs)))
+a1 = '({})==1)'.format('+'.join('toint(p{})'.format(i) for i in range(len(pegs))))
+trans = ''
+for i in range(len(pegs)):
+    current = pegs[i]
+    top = (current[0], current[1]-1)
+    bottom = (current[0], current[1]+1)
+    left = (current[0]-1, current[1])
+    right = (current[0]+1, current[1])
+
+print """\
+MODULE main
+VAR
+{}
+INIT
+{}
+TRANS
+case {}
+{}
+LTLSPEC G !({})
+""".format(var, init, trans, win, a1)

diff --git a/a2/src/4.smv b/a2/src/4.smv
new file mode 100644 (file)
index 0000000..08856c4
--- /dev/null
+++ b/a2/src/4.smv
@@ -0,0 +1,24 @@
+MODULE main
+VAR
+p1: boolean;
+p2: boolean;
+INIT
+p1=TRUE & p2=TRUE & p3=TRUE &
+p4=TRUE & p5=TRUE & p6=TRUE &
+
+p7=TRUE & p8=TRUE & 
+       p9=TRUE & p10=TRUE & p11=TRUE &
+       p12=TRUE & p13=TRUE &
+p14=TRUE & p15=TRUE &
+       p16=TRUE & p17=TRUE & p18=TRUE &
+       p19=TRUE & p20=TRUE &
+p21=TRUE & p22=TRUE & p23=TRUE &
+       p24=TRUE & p25=TRUE & p26=TRUE &
+       p27=TRUE & p28=TRUE &
+
+p29=TRUE & p30=TRUE & p31=TRUE &
+p32=TRUE & p33=TRUE & p34=TRUE
+TRANS
+next(p1)=TRUE &
+next(p2)=TRUE
+LTLSPEC G !(p1=FALSE)