\section{Problem 3}
+\emph{The goal of this problem is to exploit the power of the recom mended
+tools rather than elaborating the questions by hand.}
+\begin{enumerate}[a.]
+ \item\emph{In mathematics, a \emph{group} is defined to be a set $G$
+ with an element $I\in G$, a binary operator $∗$ and a unary
+ operator inv satisfying.
+ $$x*(y*z)=(x*y)*z, x*I=x\text{ and }x*inv(x)=I,$$
+ for all $x,y,z\in G$. Determine whether in every group each of
+ the four properties
+ $$I*x=x, inv(inv(x))=x, inv(x)*x=I\text{ and } x*y=y*x$$
+ holds for all $x,y\in G$. If a property does not hold,
+ determine the size of the smallest finite group for which it
+ does not hold.}
+ \item\emph{A term rewrite sysetm consists of the single rule
+ $$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$
+ in which $a$ is a binary symbol and $x,y,z,u$ are variables.
+ Moreover, there are constants $b,c,d,e,f,g$. Determine whether
+ $c$ and $d$ may swapped in $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ by
+ rewriting, that is, $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ rewrites
+ in a finite number of steps to
+ $a(b,a(d,a(c,a(e,a(f,a(b,g))))))$.}\\
+
+ When inspecting the rewrite rule more closely we see that the
+ entire structure of the formula stays the same and that only
+ the variables $x,y,z$ are changed in order. Because of this we
+ can simplify the rule to
+ $$x,y,z\rightarrow y,z,x$$
+ and we can simplify the question to asking whether
+ $b,c,d,e,f,b$ rewrites to $b,d,c,e,f,b$.\\
+
+ Because of this the nature of the rewritten problem becomes
+ solvable by a symbolic model checker. We define for every
+ position $i\in\{0\ldots5\}$ a variable $p_i$ of the enumeration
+ type $\{b,c,d,e,f\}$. To keep track of the moves we define a
+ move $m\in\{0\ldots4\}$ variable that indicates the location of
+ the first variable or $0$ for the initial value. The initial
+ values of the position variables is
+ $$p_0=b,p_1=c,p_2=d,p_3=e,p_4=f,p_5=b$$
+ There are four possible transitions and they are put in a
+ disjuction and shown below:
+ $$\begin{array}{rl}
+ next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
+ \wedge next(p_2)=p_0 \wedge\\
+ & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
+
+ next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
+ \wedge next(p_2)=p_3 \wedge\\
+ & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
+
+ next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
+ \wedge next(p_2)=p_3 \wedge\\
+ & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5\\
+ next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
+ \wedge next(p_2)=p_2 \wedge\\
+ & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3
+ \end{array}$$
+
+ The LTL logic goal state would then be
+ $$\mathcal{G} \neg(p_0=b\wedge p_1=d\wedge p_2=c\wedge
+ p_3=e\wedge p_4=f\wedge p_5=b)$$
+
+ The solution described below is found by
+ \textsc{NuSMV} within $0.01$ seconds. Overline triples are the
+ ones changed in the next.
+ $$\begin{array}{rl}
+ \overline{b,c,d},e,f,b
+ & \rightarrow c,d,\overline{b,e,f},b\\
+ & \rightarrow c,d,e,\overline{f,b,b}\\
+ & \rightarrow c,d,e,\overline{b,b,f}\\
+ & \rightarrow c,\overline{d,e,b},f,b\\
+ & \rightarrow c,\overline{e,b,d},f,b\\
+ & \rightarrow \overline{c,b,d},e,f,b\\
+ & \rightarrow b,\overline{d,c,e},f,b\\
+ & \rightarrow b,c,e,d,f,b\\
+ \end{array}$$
+
+
+
+\end{enumerate}
+++ /dev/null
-#!/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
repositories / ar1516.git / commitdiff