--- /dev/null
+\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.
+}
+
+
+++ /dev/null
-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)
-)
--- /dev/null
+\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}$
+++ /dev/null
-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))
-)
--- /dev/null
+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)
+++ /dev/null
-(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)
-))
--- /dev/null
+%&ar
+\begin{document}
+\maketitle
+
+\input{1.tex}
+\input{2.tex}
+\input{3.tex}
+\input{4.tex}
+
+\end{document}
--- /dev/null
+\documentclass{article}
+
+\usepackage{a4wide}
+\usepackage{bm}
+
+\everymath{\displaystyle}
+
+\author{Mart Lubbers (s4109503)}
+\title{Automated reasoning Assignment 1}
+\date{\today}
--- /dev/null
+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)
+
--- /dev/null
+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("))")
--- /dev/null
+(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)
+)
+)
repositories / master.git / commitdiff