From f3eb67d340f8e00feebef1d58acc854772783337 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Mon, 4 Jan 2016 11:37:15 +0100 Subject: [PATCH] cleaned up and finished 1-3 --- a2/1.tex | 117 ++++++++++++++++++++++++------------------------- a2/2.tex | 93 +++++++++++++++++++++------------------ a2/3.tex | 84 ++++++++++++----------------------- a2/pre.tex | 1 + a2/src/1c.bash | 16 +++---- 5 files changed, 144 insertions(+), 167 deletions(-) diff --git a/a2/1.tex b/a2/1.tex index 6de7ceb..61dc95d 100644 --- a/a2/1.tex +++ b/a2/1.tex @@ -9,45 +9,40 @@ delivering. The truck has to pick up its food packages at location $S$ containing an unbounded supply. The villages only have a limited capacity to store food packages: for $A$ and $B$ this capacity is $120$, for $C$ it is $200$. Initially, the truck is in $S$ and is fully loaded, and in $A$, $B$ and -$C$ there are $40$, $30$ and $145$ food packages, respectively.} +$C$ there are $40$, $30$ and $145$ food packages, respectively.}\\ -The problem can be described as a SAT problem that we can solve in SAT-solver. -Every movement from the truck from a city to a city is called an iteration $i$ -for $i\in I$ where $I=\{0\ldots\}$. For every iteration $i$ we make variables -$a_i, b_i, c_i, t_i, l_i, d_i$ respectively for the capacity of city $A$, -city $B$, city $C$, the truck, the trucks location and a help variable to -record how much food is dumped in the city. The distance between two cities is -described with the function $dist(x, y)$. For all cities except $S$ and the -truck a variable is defined that states the maximum capacity. We express all -the constant values in the formula called $const$. +The problem can be solved by transforming it to a SAT problem. Every movement +from the truck from a city to a city is called an iteration $i\in I$ where +$I=\{0\ldots\}$. For every iteration $i$ variables $a_i, b_i, c_i, t_i, l_i, +d_i$ are createde respectively for the stock of city $A$, city $B$, city $C$, +the truck, the trucks location and the amount of food dumped. We introduce a +function $dist(x,y)$ that returns the distance between two cities. For $A,B,C$ +and the truck a variable is declared which states the maximum capacity. All the +constants together is called $\mathcal{CON}$. $$a_{\max}=120\wedge b_{\max}=120\wedge c_{\max}=200\wedge t_{\max}=300$$ Iteration $0$ depicts the initial state and can be described with a simple -conjunction called $initial$. +conjunction called $\mathcal{INI}$. $$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$ In every iteration there are certain constraints that always have to hold. We -call them $constraints$ and they are expressed as: +call them $\mathcal{CST}(i)$ and they are expressed as: $$d_i>0\wedge d_i\leq t_{\max}\wedge t_i\geq\wedge t_i\leq t_{\max}\wedge \bigwedge_{k\in\{A,B,C\}}k_i>0$$ -We reason about the new iteration $i$ from the things we know about iteration -$i-1$. The crucial part is the location we were in iteration $i-1$ and we make -a disjunction over all possible cities and describe the result in the following -formula called $trans$. We introduce a function $conn(s)$ that returns the set -of all cities connected to city $s$. To begin with $(1)$ sets the location of -the previous iteration correct and checks whether the city will not run out of -food while travelled too. $(2)$ deals with the fact that the truck can not dump -any food in city $S$ and constraints the amount of food dumped in the city. -$(3)$ deals with the fact that the dumped food is added to the current stock of -the city. Sub formula $(4)$ deals with the fact that if the truck is in $S$ it -is replenished and otherwise the dumped load is subtracted from the trucks -load. Finally $(5)$ deals with the other cities which will have their stock -decremented with the distance traveled. - +Besides the constraints the movement of the truck should be modeled. Depending +on $l_{i-1}$ we want to reason about the consequences of the truck moving to +$l_{i}$. The formula is called $\mathcal{TRA}$. We introduce a function +$conn(s)$ that returns the set of all cities connected to city $s$. $(1)$ sets +the location of the previous iteration correct and checks whether the city is +reachable without running out of food. $(2)$ limits the amount of food dumped +according to distance traveled, the old stock and the truck stock. When the +truck is in $S$ the truck will just be filled. $(3)$ adds the dumped food to +the stock of the city. $(4)$ subtracts the dumped food stock from the truck. +Finally $(5)$ subtracts the distance traveled from the food stock. \begin{align} \bigvee_{k\in\{S\}\cup V} l_{i-1}=k\wedge @@ -59,17 +54,19 @@ decremented with the distance traveled. k''_i=k''_{i-1}-dist(k,k') \end{align} -We tie all this together in one big formula that is as follows: -$$const\wedge initial\wedge -\bigwedge_{i\in I}\left(constraints\wedge trans\right)$$ +All the formulas tied together leads to the final formula that is satisfiable +if and only if there is never a depleted city in any iteration. +$$\mathcal{CON}\wedge\mathcal{INI}\wedge +\bigwedge_{i\in I}\left(\mathcal{CST}(i)\wedge\mathcal{TRA}(i)\right)$$ +\newpage \begin{enumerate}[(a)] \item \emph{Show that it is impossible to deliver food packages in such a way that each of the villages consumes one food package per time unit forever.} Incrementally increasing the number of iterations does result in finding an unsatisfiable formula with $I=21$. Thus there is no infinite - path that keeps the cities saturated forever. + path that keeps the cities saturated. \item \emph{Show that this is possible if the capacity of the truck is increased to 320 food packages. (Note that a finite graph contains an infinite path starting in a node $v$ if and only if there is a path @@ -81,36 +78,36 @@ $$const\wedge initial\wedge $$\bigvee_{i\in I}\bigvee_{j\in \{0\ldots i-1\}}\left( t_i=t_j\wedge l_i=l_j\wedge\bigwedge_{k\in V}k_i=k_j\right) $$ - - When we incrementally increase the number of iterations we see that - when we have more then $10$ iterations we encounter a cycle. This is - shown in Table~\ref{tbl:s3b} where iteration $4$ and iteration $11$ are - equal. - \begin{table}[H] - \centering - \begin{tabular}{lrrrrcr} - \toprule - $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\ - \midrule - $0$ & $40$ & $30$ & $145$ & $320$ & $S$ & $0$\\ - $1$ & $19$ & $35$ & $124$ & $294$ & $B$ & $26$\\ - $2$ & $120$ & $18$ & $107$ & $176$ & $A$ & $118$\\ - $3$ & $103$ & $120$ & $90$ & $57$ & $B$ & $119$\\ - \textbf{4} & \textbf{82} & \textbf{99} & \textbf{69} & - \textbf{320} & \textbf{S} & \textbf{0}\\ - $5$ & $119$ & $70$ & $40$ & $254$ & $A$ & $66$\\ - $6$ & $87$ & $38$ & $194$ & $68$ & $C$ & $186$\\ - $7$ & $50$ & $67$ & $157$ & $2$ & $B$ & $66$\\ - $8$ & $29$ & $46$ & $136$ & $320$ & $S$ & $0$\\ - $9$ & $120$ & $17$ & $107$ & $200$ & $A$ & $120$\\ - $10$ & $103$ & $120$ & $90$ & $80$ & $B$ & $120$\\ - \textbf{11} & \textbf{82} & \textbf{99} & \textbf{69} & - \textbf{320} & \textbf{S} & \textbf{0}\\ - \bottomrule - \end{tabular} - \caption{Solution for problem $3b$}\label{tbl:s3b} - \end{table} + Since $(c)$ is also true the solution in Table~\ref{tbl:s3c} is also + correct for a truck with size $320$. \item \emph{Figure out whether it is possible if the capacity of the truck is set to $318$.} - + When we incrementally increase the number of iterations we see that + when we have more then $10$ iterations we encounter a cycle. Changing + $t_{\max}=318$ and keeping the rest the same as in $b$ we find also + cycle after $11$ iterations as shown in Table~\ref{tbl:s3c} \end{enumerate} +\begin{table}[h] + \centering + \begin{tabular}{lrrrrcr} + \toprule + $I$ & $A$ & $B$ & $C$ & Truck & Location & Dump\\ + \midrule + $0$ & $40$ & $30$ & $145$ & $318$ & $0$ & $0$\\ + $1$ & $19$ & $35$ & $124$ & $292$ & $2$ & $26$\\ + $2$ & $120$ & $18$ & $107$ & $174$ & $1$ & $118$\\ + $3$ & $103$ & $120$ & $90$ & $55$ & $2$ & $119$\\ + \textbf{4} & \textbf{82} & \textbf{99} & + \textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\ + $5$ & $119$ & $70$ & $40$ & $252$ & $1$ & $66$\\ + $6$ & $87$ & $38$ & $194$ & $66$ & $3$ & $186$\\ + $7$ & $50$ & $67$ & $157$ & $0$ & $2$ & $66$\\ + $8$ & $29$ & $46$ & $136$ & $318$ & $0$ & $0$\\ + $9$ & $120$ & $17$ & $107$ & $198$ & $1$ & $120$\\ + $10$ & $103$ & $120$ & $90$ & $78$ & $2$ & $120$\\ + \textbf{11} & \textbf{82} & \textbf{99} & + \textbf{69} & \textbf{318} & \textbf{0} & \textbf{0}\\ + \bottomrule + \end{tabular} + \caption{Solution for problem $3b$ and $3c$}\label{tbl:s3c} +\end{table} diff --git a/a2/2.tex b/a2/2.tex index 0c51035..56df1c9 100644 --- a/a2/2.tex +++ b/a2/2.tex @@ -11,46 +11,67 @@ times: other bottle is full. \end{itemize}} -The problem is easily solvable using a symbolic model checker since it is -clearly a problem that progresses with state transfers up to a goal. For all -bottles $b_i$ for $i\in\{1\ldots3\}$ we create a variable stating the contents -in the current state $b_i$ and a constant that describes the maximum content -$b_{i\max}$. State transitions come in three classes. With the next -function we describe the transition to the next state. If the next state is not -defined for a bottle $b_i$ we assume $\text{next}(b_i)=b_i$. +The problem can be solved by transforming it into a symbolic model. For all +bottles $b_i$ for $i\in\{1\ldots3\}$ a variable is created that states the +contents in that state. A constant variable is created per bottle that defines +the maximum content $b_{i\max}$ the bottle can hold. The initial state then +becomes. +$$b_0=3\wedge b_1=0\wedge b_2=0\wedge +b_{1\max}=144\wedge b_{2\max}=72\wedge b_{3\max}=16$$ + +When we transition to the next state we can do three actions. With a $next$ +function we describe the transition to the next state for every bottle. If the +next state is not defined for a bottle $b_i$ we assume $next(b_i)=b_i$. \begin{itemize} \item Filling a bottle $b_i$\\ If we fill a bottle $b_i$ the contents will be the maximum thus:\\ - $\text{next}(b_i)=b_{i\max}$. + $next(b_i)=b_{i\max}$. \item Emptying a bottle $b_i$\\ If we empty a bottle $b_i$ the contents will become zero thus:\\ - $\text{next}(b_i)=0$. + $next(b_i)=0$. \item Pouring a bottle $b_i$ in bottle $b_j$ for $i\neq j$\\ If we pour a bottle $b_i$ into $b_j$, the contents that fits in $b_j$ will be subtracted from $b_i$ and added to $b_j$. What exactly fits in $b_j$ can be described as $\min(b_{j\max}-b_j, b_i)$ thus the following state changes can be defined:\\ - $\text{next}(b_i)=b_i-\min(b_{j\max}-b_j, b_i)$\\ - $\text{next}(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$ + $next(b_i)=b_i-\min(b_{j\max}-b_j, b_i)$\\ + $next(b_j)=b_j+\min(b_{j\max}-b_j, b_i)$ \end{itemize} -All transitions are unconstrained and therefore we can convert this very easily -to \textsc{NuSMV} by enclosing all the transition classes in brackets and -joining them with logical or operators. +All transitions together in a disjuction would specify all possible +transitions. +\newpage \begin{enumerate}[(a)] \item \emph{Determine whether it is possible to arrive at a situation in which the first bottle contains 8 units and the second one contains 11 units. If so, give a scenario reaching this situation.} - - The solution described in \autoref{tab:sol2a} is found by - \textsc{NuSMV} within $0.29$ seconds. - \begin{table}[H] - \centering\small + With the following goal the solution in Table~\ref{tab:sol2} is + found by \textsc{NuSMV} within $0.29$ seconds. + $$\mathcal{G}\neg(b_1=8\wedge b_2=1)$$ + \item + \emph{Do the same for the variant in which the second bottle is + replaced by a bottle that can hold 80 units, and all the rest remains + the same.} + When updating variable $b_{2\max}=80$ and using the goal from $(a)$ + \textsc{NuSMV} concludes that there is no there is no counterexample + within $0.1$ seconds. + \item + \emph{Do the same for the variant in which the third bottle is replaced + by a bottle that can hold 28 units, and all the rest (including the + capacity of 72 of the second bottle) remains the same.} + When updating variable $b_{3\max}=28$ and using the goal from $(a)$ + the solution in Table~\ref{tab:sol2} is found by \textsc{NuSMV} within + $1.8$ seconds. +\end{enumerate} +\begin{table}[h] + \centering\small + \begin{tabular}{ccc} + \begin{minipage}{.5\linewidth} \begin{tabular}{rrrrl} \toprule - State & Bottle 1 & Bottle 2 & Bottle 3 & Action\\ + & Bottle 1 & Bottle 2 & Bottle 3 & Action\\ \midrule $0$ & $3$ & $0$ & $0$ &\\ $1$ & $0$ & $0$ & $3$ & Poured $1$ in $3$\\ @@ -69,27 +90,13 @@ joining them with logical or operators. $14$ & $0$ & $11$ & $8$ & Emptied $1$\\ $15$ & $8$ & $11$ & $8$ & Poured $3$ in $1$\\ \bottomrule - \end{tabular} - \caption{Solution for problem 1}\label{tab:sol2a} - \end{table} - \item - \emph{Do the same for the variant in which the second bottle is - replaced by a bottle that can hold 80 units, and all the rest remains - the same.} - - There is no solution for this configuration. - \item - \emph{Do the same for the variant in which the third bottle is replaced - by a bottle that can hold 28 units, and all the rest (including the - capacity of 72 of the second bottle) remains the same.} - - The solution described in \autoref{tab:sol2c} is found by - \textsc{NuSMV} within $1.8$ seconds. - \begin{table}[H] - \centering\small + \multicolumn{5}{c}{Solution for problem $2a$} + \end{tabular}\vspace{16.55em} + \end{minipage} & \quad & + \begin{minipage}{.5\linewidth} \begin{tabular}{rrrrl} \toprule - State & Bottle 1 & Bottle 2 & Bottle 3 & Action\\ + & Bottle 1 & Bottle 2 & Bottle 3 & Action\\ \midrule $0$ & $3$ & $0$ & $0$ &\\ $1$ & $3$ & $72$ & $0$ & Filled $2$\\ @@ -122,7 +129,9 @@ joining them with logical or operators. $28$ & $8$ & $39$ & $0$ & Emptied $3$\\ $29$ & $8$ & $11$ & $28$ & Poured $2$ in $3$\\ \bottomrule + \multicolumn{5}{c}{Solution for problem $2c$} \end{tabular} - \caption{Solution for problem 2}\label{tab:sol2c} - \end{table} -\end{enumerate} + \end{minipage} + \end{tabular} + \caption{Solutions for problems $2a$ and $2c$}\label{tab:sol2} +\end{table} diff --git a/a2/3.tex b/a2/3.tex index 20d8feb..642c4bb 100644 --- a/a2/3.tex +++ b/a2/3.tex @@ -31,17 +31,6 @@ tools rather than elaborating the questions by hand.} As found by \textsc{prover9} a proof for $inv(inv(x))=x$. \begin{lstlisting} -1 inv(inv(x)) = x. [goal]. -2 x * (y * z) = (x * y) * z.[assumption]. -3 (x * y) * z = x * (y * z).[copy(2),flip(a)]. -4 x * I = x. [assumption] -5 x * inv(x) = I. [assumption]. -6 inv(inv(c1)) != c1. [deny(1)]. -7 x * (I * y) = x * y. [para(4(a,1),3(a,1,1)),flip(a)]. -8 x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)]. -13 I * inv(inv(x)) = x. [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)]. -15 x * inv(inv(y)) = x * y. [para(13(a,1),3(a,2,2)),rewrite([4(2)])]. -16 I * x = x. [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])]. 19 x * (inv(x) * y) = y. [back_rewrite(8),rewrite([16(5)])]. 22 inv(inv(x)) = x. [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)]. 23 \$F. [resolve(22,a,6,a)]. @@ -49,25 +38,12 @@ tools rather than elaborating the questions by hand.} As found by \textsc{prover9} a proof for $x*inv(x)=I$. \begin{lstlisting} -1 inv(x) * x = I. [goal]. -2 x * (y * z) = (x * y) * z.[assumption]. -3 (x * y) * z = x * (y * z).[copy(2),flip(a)]. -4 x * I = x. [assumption]. -5 x * inv(x) = I. [assumption]. -6 inv(c1) * c1 != I. [deny(1)]. -7 x * (I * y) = x * y. [para(4(a,1),3(a,1,1)),flip(a)]. -8 x * (inv(x) * y) = I * y. [para(5(a,1),3(a,1,1)),flip(a)]. -13 I * inv(inv(x)) = x. [para(5(a,1),8(a,1,2)),rewrite([4(2)]),flip(a)]. -15 x * inv(inv(y)) = x * y. [para(13(a,1),3(a,2,2)),rewrite([4(2)])]. -16 I * x = x. [para(13(a,1),7(a,2)),rewrite([15(5),7(4)])]. -19 x * (inv(x) * y) = y. [back_rewrite(8),rewrite([16(5)])]. -22 inv(inv(x)) = x. [para(5(a,1),19(a,1,2)),rewrite([4(2)]),flip(a)]. 24 inv(x) * x = I. [para(22(a,1),5(a,1,2))]. 25 \$F. [resolve(24,a,6,a)]. \end{lstlisting} \textsc{prover9} fails to find a proof for $x*y=y*x$. - Running the same file with \textsc{mace4} gives the following + Running the same file with \textsc{mace4} gives the smallest counterexample listed in Table~\ref{tab:s3a}. \begin{table}[H] @@ -91,8 +67,9 @@ tools rather than elaborating the questions by hand.} & 5 & 5 & 3 & 4 & 1 & 2 & 0 \end{array}\right.$ \end{tabular} - \caption{Solution for problem 3a}\label{tab:s3a} + \caption{Smallest counterexample for problem 3a}\label{tab:s3a} \end{table} + \newpage \item\emph{A term rewrite system 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. @@ -104,46 +81,39 @@ tools rather than elaborating the questions by hand.} 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$.\\ + the variables $x,y,z$ are changed in order. Thus we can simplify the + rule and question to + $$x,y,z\rightarrow y,z,x\text{ and } + b,c,d,e,f,b\overset{*?}{\rightarrow}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 - disjunction and shown below: - $$\begin{array}{rl} - next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2 + Applying these changes changes the problem into a model checking + problem. For every position $i\in\{0\ldots5\}$ a variable $p_i$ of the + enumeration type $\{b,c,d,e,f\}$ is defined. To keep track of the moves + a move $m\in\{0\ldots4\}$ variable that indicates the location of the + first variable or $0$ for the initial value is defined. The initial + values of the position variables are + $$p_0=b\wedge p_1=c\wedge p_2=d\wedge p_3=e\wedge p_4=f\wedge p_5=b + \wedge m=0$$ + There are four possible transitions as shown below. + $$\begin{array}{rrl} + & (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 + & & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\ + \vee & (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 + & & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5)\\ + \vee & (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 + & & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5)\\ + \vee & (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 + & & 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 + With the following goal the solution below is + found by \textsc{NuSMV} within $0.01$ seconds. $$\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. Lined over 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\\ diff --git a/a2/pre.tex b/a2/pre.tex index 588df3a..df89a95 100644 --- a/a2/pre.tex +++ b/a2/pre.tex @@ -2,6 +2,7 @@ \usepackage{a4wide} \usepackage{amsmath} +\usepackage{array} \usepackage{booktabs} \usepackage{enumerate} \usepackage{float} diff --git a/a2/src/1c.bash b/a2/src/1c.bash index f8ba916..5b2a04e 100644 --- a/a2/src/1c.bash +++ b/a2/src/1c.bash @@ -159,17 +159,17 @@ GEN ) GEN done -# echo "(or" -# for i in $(seq 0 $ITERATIONS); do -# for j in $(seq $((i+1)) $ITERATIONS); do -# echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))" -# done -# done -# echo ")" + echo "(or" + for i in $(seq 0 $ITERATIONS); do + for j in $(seq $((i+1)) $ITERATIONS); do + echo "(and (= t$i t$j) (= l$i l$j) (= a$i a$j) (= b$i b$j) (= c$i c$j))" + done + done + echo ")" echo "))" } it=1 -while generate $it 318 | $YICES | pee sort "grep -q \"^sat\"" +while generate $it 318 | $YICES -m | pee sort "grep -q \"^unsat\"" do echo $((it++)) done -- 2.20.1