From 0dc10cdf9fd0266be5067678cb05137dee5c4683 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sun, 3 Jan 2016 14:05:36 +0100 Subject: [PATCH] update 3b fixed --- a2/3.tex | 79 +++++++++++++++++++++++++++++++ a2/Makefile | 2 +- a2/pre.tex | 2 + a2/src/1.bak | 126 -------------------------------------------------- a2/src/3b.smv | 47 +++++++++++++++++++ 5 files changed, 129 insertions(+), 127 deletions(-) delete mode 100644 a2/src/1.bak create mode 100644 a2/src/3b.smv diff --git a/a2/3.tex b/a2/3.tex index a6e47e9..d29e965 100644 --- a/a2/3.tex +++ b/a2/3.tex @@ -1 +1,80 @@ \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} diff --git a/a2/Makefile b/a2/Makefile index 5162ae9..da3087d 100644 --- a/a2/Makefile +++ b/a2/Makefile @@ -17,4 +17,4 @@ all: $(DOCUMENT).pdf $(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump" clean: - $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf) + $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf) *.xyc diff --git a/a2/pre.tex b/a2/pre.tex index b9325ec..37f6b7e 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -14,6 +14,8 @@ \lstset{keepspaces=true,captionpos=b,basicstyle=\ttfamily} +\CompileMatrices% + \author{Mart Lubbers (s4109503)} \title{Automated reasoning Assignment 2} \date{\today} diff --git a/a2/src/1.bak b/a2/src/1.bak deleted file mode 100644 index 2966704..0000000 --- a/a2/src/1.bak +++ /dev/null @@ -1,126 +0,0 @@ -#!/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< 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<