From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 7 Oct 2015 18:55:49 +0000 (+0200)
Subject: started with the report
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=0af33fc5fba83cf7bb5ad1167e78fe1a0124019d;p=master.git

started with the report
---

diff --git a/ar/assignments/1.tex b/ar/assignments/1.tex
new file mode 100644
index 0000000..56b444d
--- /dev/null
+++ b/ar/assignments/1.tex
@@ -0,0 +1,24 @@
+\paragraph{Problem 1}
+
+{\em
+Six trucks have to deliver pallets of obscure building blocks to a magic
+factory. Every ruck has a capacity of 7800 kg and can carry at most
+eight pallets. In total, the following has to be delivered:\\
+\begin{itemize}
+	\item Four pallets of nuzzles, each of weight 700 kg.
+	\item A number of pallets of prittles, each of weight 800 kg.
+	\item Eight pallets of skipples, each of weight 1000 kg.
+	\item Ten pallets of crottles, each of weight 1500 kg.
+	\item Five pallets of dupples, each of weight 100 kg.
+\end{itemize}
+Prittles and crottles are an explosive combination: they are not allowed to be
+put in the same truck.\\
+Skipples need to be cooled; only two of the six trucks have facility for
+cooling skipples. Dupples are very valuable; to distribute the risk of loss no
+two pallets of dupples may be in the same truck.\\
+Investigate what is the maximum number of pallets of prittles that can be
+delivered, and show how for that number all pallets may be divided over the six
+trucks.
+}
+
+
diff --git a/ar/assignments/2.tex b/ar/assignments/2.tex
new file mode 100644
index 0000000..e69de29
diff --git a/ar/assignments/3.tex b/ar/assignments/3.tex
new file mode 100644
index 0000000..e69de29
diff --git a/ar/assignments/4.smv b/ar/assignments/4.smv
deleted file mode 100644
index 67d257b..0000000
--- a/ar/assignments/4.smv
+++ /dev/null
@@ -1,24 +0,0 @@
-MODULE main
-VAR
-a2 : 2..100;
-a3 : 3..100;
-a4 : 4..100;
-a5 : 5..100;
-a6 : 6..100;
-c : 0..30;
-INIT
-a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & c=1
-TRANS
-next(c)=c+1 & (
-	next(a2)=1+a3 |
-	next(a3)=a2+a4 |
-	next(a4)=a3+a5 |
-	next(a5)=a4+a6 |
-	next(a6)=a5+7
-)
-LTLSPEC G !(
-	(a2>=50) |
-	(a3>=50) |
-	(a4>=50) |
-	(a5>=50)
-)
diff --git a/ar/assignments/4.tex b/ar/assignments/4.tex
new file mode 100644
index 0000000..e0f3ac0
--- /dev/null
+++ b/ar/assignments/4.tex
@@ -0,0 +1,54 @@
+\paragraph{Problem 4}
+
+{\em
+Seven integer variables $a_1; a_2; a_3; a_4; a_5; a_6; a_7$ are given, for
+which the initial value of $a_i$ is $i$ for $i=1,\ldots,7$. The following steps
+are defined: choose $i$ with $1<i<7$ and execute
+$$a_i:=a_{i-1}+a_{i+1}$$
+that is, $a_i$ gets the sum of the values of its neighbors and all other
+values remain unchanged. Show how it is possible that after a number of steps
+a number of steps a number $\ge 50$ occurs at least twice in $a_1; a_2; a_3;
+a_4; a_5; a_6; a_7$.
+}
+
+\paragraph{Solution}
+Say we have $I$ $a$'s denoted as $a_i$ and we have $N$ iterations.
+For every $a_i$ in every iteration we make a variable $i_na_i$ where $n$ is the
+number of the iteration. For $a_0$ and $a_7$ we can make an exception since
+they do not change over iterations. For documenting purposes we also keep a counter
+variable $c_n$ for every $n$th iteration. This leads in the initial state
+expressed by:
+
+$$
+\left(c_0=0\right)\wedge
+\left(a_1=1\right)\wedge
+\left(a_I=I\right)\wedge
+\bigwedge_{k=2}^{I-1} \left(i_0a_i = i\right)
+$$
+
+Every next iteration we only increment one $i$ from $2,\ldots,6$.
+
+Say we want to check if the state is reachable in $N$ iterations. Then we can
+specifiy postconditions. For every $i$ we specify this:
+$$\bigvee_{k=2}^{I-1}\left(
+	\left(i_Na_k >= 50\right)\wedge\left(
+		\bigvee_{j=2}^{I-1}\left(i_Na_k=i_Na_j\right)\wedge
+		\left(k\neq j\right)
+	\right)
+\right)$$
+
+$\begin{array}{c|c|ccccc}
+	\# & i & a_2 & a_3 & a_4 & a_5 & a_6\\
+	\hline
+	0 & - & 2 & 3 & 4 & 5 & 6\\
+	1 & 4 & 2 & 3 & \bm{8} & 5 & 6\\
+	2 & 5 & 2 & 3 & 8 & \bm{14} & 6\\
+	3 & 2 & \bm{4} & 3 & 8 & 14 & 6\\
+	4 & 4 & 4 & 3 & \bm{17} & 14 & 6\\
+	5 & 5 & 4 & 3 & 17 & \bm{23} & 6\\
+	6 & 6 & 4 & 3 & 17 & 23 & \bm{30}\\
+	7 & 5 & 4 & 3 & 17 & \bm{47} & 30\\
+	8 & 4 & 4 & 3 & \bm{50} & 47 & 30\\
+	9 & 3 & 4 & \bm{54} & 50 & 47 & 30\\
+	10 & 6 & 4 & 54 & 50 & 47 & \bm{54}\\
+\end{array}$
diff --git a/ar/assignments/4a.smv b/ar/assignments/4a.smv
deleted file mode 100644
index b88f231..0000000
--- a/ar/assignments/4a.smv
+++ /dev/null
@@ -1,24 +0,0 @@
-MODULE main
-VAR
-a2 : 2..65;
-a3 : 3..65;
-a4 : 4..65;
-a5 : 5..65;
-a6 : 6..65;
-c : 0..15;
-INIT
-a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & c = 0
-TRANS
-next(c)=c+1 & (
-	next(a2)=1+a3 |
-	next(a3)=a2+a4 |
-	next(a4)=a3+a5 |
-	next(a5)=a4+a6 |
-	next(a6)=a5+7
-)
-LTLSPEC G !(
-	(a2>=50 & (a2=a3 | a2=a4 | a2=a5 | a2=a6)) |
-	(a3>=50 & (a3=a4 | a3=a5 | a3=a6)) |
-	(a4>=50 & (a4=a5 | a4=a6)) |
-	(a5>=50 & (a5=a6))
-)
diff --git a/ar/assignments/Makefile b/ar/assignments/Makefile
new file mode 100644
index 0000000..2055aa8
--- /dev/null
+++ b/ar/assignments/Makefile
@@ -0,0 +1,21 @@
+LATEX:=latex
+
+DOCUMENT:=ar
+SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex))
+
+.SECONDARY: $(addsuffix .fmt,$(DOCUMENT))
+
+all: $(DOCUMENT).pdf
+
+%.pdf: %.dvi
+	dvipdfm $<
+
+%.dvi: %.tex %.fmt $(SOURCES)
+	$(LATEX) $(basename $@)
+	$(LATEX) $(basename $@)
+
+%.fmt: preamble.tex
+	$(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
+
+clean:
+	$(RM) -v $(addprefix $(DOCUMENT).,fmt aux bbl blg dvi log out toc pdf)
diff --git a/ar/assignments/a11.smt b/ar/assignments/a11.smt
deleted file mode 100644
index a208034..0000000
--- a/ar/assignments/a11.smt
+++ /dev/null
@@ -1,15 +0,0 @@
-(benchmark a11.smt
-:logic QF_UFLIA
-:extrafuns (
-	(Nuzzles Int)
-	(Prittles Int)
-	(Skipples Int)
-	(Crottles Int)
-	(Duples Int))
-:formula (and
-(= Nuzzles 700)
-(= Prittles 800)
-(= Skipples 1000)
-(= Crottles 1500)
-(= Duples 100)
-)) 
diff --git a/ar/assignments/ar.tex b/ar/assignments/ar.tex
new file mode 100644
index 0000000..a85b3f2
--- /dev/null
+++ b/ar/assignments/ar.tex
@@ -0,0 +1,10 @@
+%&ar
+\begin{document}
+\maketitle
+
+\input{1.tex}
+\input{2.tex}
+\input{3.tex}
+\input{4.tex}
+
+\end{document}
diff --git a/ar/assignments/preamble.tex b/ar/assignments/preamble.tex
new file mode 100644
index 0000000..477b06f
--- /dev/null
+++ b/ar/assignments/preamble.tex
@@ -0,0 +1,10 @@
+\documentclass{article}
+
+\usepackage{a4wide}
+\usepackage{bm}
+
+\everymath{\displaystyle}
+
+\author{Mart Lubbers (s4109503)}
+\title{Automated reasoning Assignment 1} 
+\date{\today}
diff --git a/ar/assignments/src/4.model b/ar/assignments/src/4.model
new file mode 100644
index 0000000..ffccc8a
--- /dev/null
+++ b/ar/assignments/src/4.model
@@ -0,0 +1,71 @@
+sat
+
+(= i3a3 3)
+(= i6a3 3)
+(= i8a5 47)
+(= i0a3 3)
+(= i6a6 30)
+(= c6 6)
+(= i0a5 5)
+(= i8a3 3)
+(= i0a4 4)
+(= i2a6 6)
+(= i8a4 50)
+(= i1a6 6)
+(= i10a6 54)
+(= i7a2 4)
+(= i3a2 4)
+(= i10a5 47)
+(= i5a2 4)
+(= i3a4 8)
+(= i8a2 4)
+(= i7a5 47)
+(= i5a5 23)
+(= c8 4)
+(= i1a3 3)
+(= i1a5 5)
+(= i10a2 4)
+(= i2a5 5)
+(= i4a4 17)
+(= i3a6 6)
+(= c3 5)
+(= c5 5)
+(= i5a3 3)
+(= i9a4 50)
+(= i5a4 17)
+(= i9a6 30)
+(= i9a2 4)
+(= a1 1)
+(= c1 2)
+(= c7 5)
+(= c2 4)
+(= i9a3 54)
+(= i10a3 54)
+(= i3a5 14)
+(= i7a3 3)
+(= c10 6)
+(= i2a2 4)
+(= i5a6 6)
+(= c0 0)
+(= c9 3)
+(= i4a5 14)
+(= i4a6 6)
+(= i7a4 17)
+(= i6a5 23)
+(= i10a4 50)
+(= i0a2 2)
+(= i4a2 4)
+(= i4a3 3)
+(= i6a2 4)
+(= i2a3 3)
+(= i7a6 30)
+(= c4 4)
+(= i2a4 8)
+(= a7 7)
+(= i6a4 17)
+(= i8a6 30)
+(= i9a5 47)
+(= i0a6 6)
+(= i1a2 4)
+(= i1a4 4)
+
diff --git a/ar/assignments/src/4.py b/ar/assignments/src/4.py
new file mode 100644
index 0000000..e260264
--- /dev/null
+++ b/ar/assignments/src/4.py
@@ -0,0 +1,59 @@
+iterations = 11
+numa = 8
+
+##Print preamble
+print("(benchmark a4.smt")
+print(":logic QF_UFLIA")
+
+##Print variables
+print(":extrafuns (")
+print("(a{} Int)".format(1))
+print("(a{} Int)".format(numa))
+for i in range(iterations):
+    for v in range(2,numa):
+        print("(i{}a{} Int) ".format(i,v))
+    print("(c{} Int)".format(i))
+print(")")
+
+##Print preconditions
+print(":formula")
+print("(and")
+print("(= c0 0)")
+print("(= a1 1)")
+print("(= a{0} {0})".format(numa, numa))
+for i in range(2,numa):
+    print("(= i0a{0} {0})".format(i))
+
+##Print iterations
+for i in range(1, iterations):
+    print("(or")
+    for v in range(2, numa):
+        print("(and")
+        print("(= c{} {})".format(i, v))
+        for ov in [k for k in range(2, numa) if k != v]:
+            print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
+        im1 = 'a1' if v == 2 else 'i{}a{}'.format(i, v-1)
+        ip1 = 'a{}'.format(numa) if v == numa-1 else 'i{}a{}'.format(i-1, v+1)
+        print("(= i{}a{} (+ {} {}))".format(i, v, im1, ip1))
+        print(")")
+    print("(and")
+    print("(= c{} 0)".format(i))
+    for ov in range(2, numa):
+        print("(= i{0}a{1} i{2}a{1})".format(i, ov, i-1))
+    print(")")
+    print(")")
+
+
+## Post conditions
+print("(or")
+for v in range(2, numa):
+    print("(and (>= i{}a{} 50)".format(iterations-1, v))
+    print("(or")
+    for ov in [k for k in range(2, numa) if k != v]:
+        print("(= i{0}a{1} i{0}a{2})".format(iterations-1, v, ov))
+    print("))")
+
+
+print(")")
+## Close the and,benchmark parenthesis
+print("))")
diff --git a/ar/assignments/src/a1.smt b/ar/assignments/src/a1.smt
new file mode 100644
index 0000000..2bfa67e
--- /dev/null
+++ b/ar/assignments/src/a1.smt
@@ -0,0 +1,19 @@
+(benchmark a1.smt
+:logic QF_UFLIA
+:extrafuns (
+	(MaxTruck Int)
+	(NuzzleWeight Int)
+	(PrittleWeight Int)
+	(SkippleWeight Int)
+	(CrottleWeight Int)
+	(DuppleWeight Int)
+)
+:formula
+(and
+	(= NuzzleWeight 700)
+	(= PrittleWeight 800)
+	(= SkippleWeight 1000)
+	(= CrottleWeight 1500)
+	(= DuppleWeight 100)
+)
+)
diff --git a/ar/assignments/marble.smv b/ar/assignments/src/marble.smv
similarity index 100%
rename from ar/assignments/marble.smv
rename to ar/assignments/src/marble.smv