conjuction:
$$a_0=40\wedge b_0=30\wedge c_0=145\wedge t_0=300\wedge l_0=S\wedge d_0=0$$
-After that all iteration can be formalized as
+After that all iterations can be formalized as
$$\begin{array}{lrl}
\bigwedge_{i\in I} \Bigg(
% Bent in S
The solution described in \autoref{tab:sol2a} is found by
\textsc{NuSMV} within $0.29$ seconds.
- \begin{table}[h]
+ \begin{table}[ht]
\centering\small
\begin{tabular}{rrrrl}
\toprule
The solution described in \autoref{tab:sol2c} is found by
\textsc{NuSMV} within $1.8$ seconds.
- \begin{table}[h]
+ \begin{table}[ht]
\centering\small
\begin{tabular}{rrrrl}
\toprule
+\section{Solving solitaire}
+Solitaire
#!/bin/bash
-AINIT=40
-BINIT=30
-CINIT=145
+AI=40
+BI=30
+CI=145
+TI=300
AMAX=120
BMAX=120
CMAX=200
TMAX=300
-TINIT=300
-TLOC=0
-PLACES=s a b c
-STATES=5
+ITERATIONS=1
function generate {
- local i j
cat<<GEN
(benchmark a1.smt
:logic QF_UFLIA
:extrafuns (
-GEN
- for i in $(seq 0 $STATES); do
- echo "(a$i Int) (b$i Int) (c$i Int) (t$i Int) (l$i Int) ) (d$i Int)"
- done
- cat <<GEN
+$( 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)"
+ done)
)
:formula
(and
- (and
- (= a0 $AINIT)
- (= b0 $BINIT)
- (= c0 $CINIT)
- (= t0 $TINIT)
- (= l0 0)
- (= d0 0)
- )
+ -- PRECONDITION
+ (and (= a0 $AI) (= b0 $BI) (= c0 $CI) (= t0 $TI) (= l0 0) (= d0 0))
GEN
- for i in $(seq $STATES); do
- j=$((i-1))
- echo "State: $i, prev: $j"
- echo "(or"
-#
- #Truck is in S
+ for i in $(seq 1 $ITERATIONS); do
cat<<GEN
+ -- SPECIAL CASE FOR STATE S(0)
+ (= l$i 0) (= d$i 0) (= t$i $TMAX)
(or
-; Truck is in S
- (and
- (= l$j 0)
- (or
- ; Truck can go to B
- (and
- (= l$i 2)
- (and
- (> d$i 0)
- (<= d$i t$j)
- (<= d$i (- $AMAX a$j))
- )
- (= a$j (
- (= b$i (- b$j 29))
- (= c$i (- b$j 29))
- )
- ; Truck can go to A
- (= l$i 1)
- )
- )
-; Truck is in A
- (and
- (= l$j 1)
+ (and -- Comes from A
+ (= l$((i-1)) 1)
+ (= a$i (- a$((i-1)) 29)
+ (= b$i (- b$((i-1)) 29)
+ (= c$i (- c$((i-1)) 29)
)
-; Truck is in B
- (and
- (= l$j 2)
- )
-; Truck is in C
- (and
- (= l$j 3)
+ (and -- Comes from B
+ (= l$((i-1)) 2)
+ (= a$i (- a$((i-1)) 21)
+ (= b$i (- b$((i-1)) 21)
+ (= c$i (- c$((i-1)) 21)
)
)
GEN
- done
+ done
echo "))"
}
#time generate | yices-smt -m | python3 src/a2.py > $1
--- /dev/null
+#!/bin/env python
+pegs = [(x, y) for x in range(7) for y in range(7) if
+ not (
+ (x < 2 and y < 2) or # exclude topleft
+ (x > 4 and y > 4) or # exclude bottomright
+ (x > 4 and y < 2) or # exclude topright
+ (x < 2 and y > 4)) # exclude bottomleft
+ ]
+holes = [(3,3)]
+var = ' '.join('p{}: boolean;'.format(i) for i in range(len(pegs)))
+init = ' & '.join('p{}={}'.format(i,
+ 'FALSE' if pegs[i] in holes else 'TRUE') for i in range(len(pegs)))
+a1 = '({})==1)'.format('+'.join('toint(p{})'.format(i) for i in range(len(pegs))))
+trans = ''
+for i in range(len(pegs)):
+ current = pegs[i]
+ top = (current[0], current[1]-1)
+ bottom = (current[0], current[1]+1)
+ left = (current[0]-1, current[1])
+ right = (current[0]+1, current[1])
+
+print """\
+MODULE main
+VAR
+{}
+INIT
+{}
+TRANS
+case {}
+{}
+LTLSPEC G !({})
+""".format(var, init, trans, win, a1)
--- /dev/null
+MODULE main
+VAR
+p1: boolean;
+p2: boolean;
+INIT
+p1=TRUE & p2=TRUE & p3=TRUE &
+p4=TRUE & p5=TRUE & p6=TRUE &
+
+p7=TRUE & p8=TRUE &
+ p9=TRUE & p10=TRUE & p11=TRUE &
+ p12=TRUE & p13=TRUE &
+p14=TRUE & p15=TRUE &
+ p16=TRUE & p17=TRUE & p18=TRUE &
+ p19=TRUE & p20=TRUE &
+p21=TRUE & p22=TRUE & p23=TRUE &
+ p24=TRUE & p25=TRUE & p26=TRUE &
+ p27=TRUE & p28=TRUE &
+
+p29=TRUE & p30=TRUE & p31=TRUE &
+p32=TRUE & p33=TRUE & p34=TRUE
+TRANS
+next(p1)=TRUE &
+next(p2)=TRUE
+LTLSPEC G !(p1=FALSE)