From 05b0d18d2bc7c8ea54c7e093089e199af8bbc8af Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 22 Dec 2015 20:34:37 +0100
Subject: [PATCH] update

---
 a2/1.tex      |  2 +-
 a2/2.tex      |  4 +--
 a2/4.tex      |  2 ++
 a2/src/1.bash | 82 +++++++++++++++------------------------------------
 a2/src/4.py   | 32 ++++++++++++++++++++
 a2/src/4.smv  | 24 +++++++++++++++
 6 files changed, 85 insertions(+), 61 deletions(-)
 create mode 100644 a2/src/4.py
 create mode 100644 a2/src/4.smv

diff --git a/a2/1.tex b/a2/1.tex
index 94a01cb..67a214c 100644
--- 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
--- 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
--- 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
--- 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
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
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)
-- 
2.20.1