From 293eddf30010a53ab3fa3fca015b1f1c8ab1e504 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 4 Dec 2015 17:51:31 +0100
Subject: [PATCH] small update

---
 a2/src/1.bash  |  59 +++++++++++++++++++++++++
 a2/src/1.py    | 118 -------------------------------------------------
 a2/src/2c.smv  |   8 +++-
 a2/src/path.sh |   3 +-
 4 files changed, 66 insertions(+), 122 deletions(-)
 create mode 100755 a2/src/1.bash
 delete mode 100644 a2/src/1.py

diff --git a/a2/src/1.bash b/a2/src/1.bash
new file mode 100755
index 0000000..bcb1892
--- /dev/null
+++ b/a2/src/1.bash
@@ -0,0 +1,59 @@
+#!/bin/bash
+AINIT=40
+BINIT=30
+CINIT=145
+AMAX=120
+BMAX=120
+CMAX=200
+TMAX=300
+TINIT=300
+TLOC=0
+
+PLACES=s a b c
+STATES=5
+
+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)"
+	done
+	cat <<GEN
+)
+:formula
+(and
+	(and (= a0 $AINIT) (= b0 $BINIT) (= c0 $CINIT) (= t0 $TINIT) (= l0 0))
+GEN
+	for i in $(seq $STATES); do
+		j=$((i-1))
+		echo $i $j
+		echo "(or"
+
+		#Truck is in S
+		echo "(and"
+		echo "(= l$j 0)"
+		echo "(> dump
+		echo ")"
+		#Truck is in A
+		echo "(and"
+		echo "(= l$j 0)"
+		echo ")"
+		#Truck is in B
+		echo "(and"
+		echo "(= l$j 0)"
+		echo ")"
+		#Truck is in C
+		echo "(and"
+		echo "(= l$j 0)"
+		echo ")"
+
+		echo ")"
+	done	
+	echo "))"
+}
+#time generate | yices-smt -m | python3 src/a2.py > $1
+generate
diff --git a/a2/src/1.py b/a2/src/1.py
deleted file mode 100644
index 1a75628..0000000
--- a/a2/src/1.py
+++ /dev/null
@@ -1,118 +0,0 @@
-#!/usr/bin/env python3
-timebound = 1000
-names = ['s', 'a', 'b', 'c']
-nodes = range(len(names))
-connections = [
-    ('s', 'a', 29), ('s', 'b', 21),
-    ('a', 's', 29), ('a', 'b', 17), ('a', 'c', 32),
-    ('b', 's', 21), ('b', 'a', 17), ('b', 'c', 37),
-    ('c', 'a', 32), ('c', 'b', 37)]
-maxes = [120, 120, 200]
-inits = [30, 40, 145]
-truck = 300
-print("""\
-MODULE main
-DEFINE
-TIMEBOUND:={};
-VAR
-truck: 0..{};
-tstock: 0..{};
-time: 0..TIMEBOUND;""".format(timebound, len(nodes), truck))
-for stock, name in zip(maxes, names[1:]):
-    print('{}stock: 0..{};'.format(name, stock))
-print('INIT')
-for init, name in zip(inits, names[1:]):
-    print('{}stock= {} &'.format(name, init))
-print("""\
-truck=0 &
-tstock=300 &
-time=0
-TRANS
-case""")
-
-for node, name in zip(nodes, names):
-    print('FALSE & truck={} & time+50<TIMEBOUND:'.format(node))
-    orsym = False
-    for fr, to, time in connections:
-        if fr != name:
-            continue
-        if orsym:
-            print('|')
-        print('(', end='')
-        print('next(time)=time+{} &'.format(time))
-        print(')')
-        orsym = True
-    print(';')
-
-# The case where time already passed over the bound
-print('TRUE:')
-for name in names[1:]:
-    print('\tnext({0}stock)={0}stock &'.format(name))
-print("""\
-\tnext(time)=time & next(tstock)=tstock & next(truck)=truck; esac
-LTLSPEC G ({})""".format(' & '.join('{}stock>0'.format(n) for n in names[1:])))
-"""
-truck={} & time<={}: (
-    -- Truck goes to A
-    (
-        next(time)=time+29 & next(truck)=1 &
-        case
-            tstock=0 & astock-0<=120:
-                next(astock)=astock+0 &
-                next(bstock)=bstock &
-                next(cstock)=cstock &
-                next(tstock)=tstock-0;
-            tstock=1 & astock-1<=120:
-                next(astock)=astock+1 &
-                next(bstock)=bstock &
-                next(cstock)=cstock &
-                next(tstock)=tstock-1;
-            ...
-            tstock=120 & astock-1<=120:
-                next(astock)=astock+1 &
-                next(bstock)=bstock &
-                next(cstock)=cstock &
-                next(tstock)=tstock-1;
-
-        esac
-    ) |
-    -- Truck goes to B
-    (next(time)=time+21 & next(truck)=2 &
-
-    )
-);
--- Truck is in A
-truck=1 & time<=TIMEBOUND:(
-    -- Truck goes to S
-    (next(time)=time+21 & next(truck)=0) |
-    -- Truck goes to B
-    (next(time)=time+17 & next(truck)=2) |
-    -- Truck goes to C
-    (next(time)=time+32 & next(truck)=3)
-);
--- Truck is in B
-truck=2 & time<=TIMEBOUND:(
-    -- Truck goes to S
-    (next(time)=time+21 & next(truck)=0) |
-    -- Truck goes to A
-    (next(time)=time+17 & next(truck)=1) |
-    -- Truck goes to C
-    (next(time)=time+32 & next(truck)=3)
-);
--- Truck is in C
-truck=3 & time<=TIMEBOUND:(
-    -- Truck goes to A
-    (next(time)=time+32 & next(truck)=1) |
-    -- Truck goes to B
-    (next(time)=time+37 & next(truck)=2)
-);
--- Time bound has passed...
-TRUE: (
-    next(time)=time &
-    next(truck)=truck &
-    next(astock)=astock &
-    next(bstock)=bstock &
-    next(cstock)=cstock &
-    next(tstock)=tstock
-);
-"""
diff --git a/a2/src/2c.smv b/a2/src/2c.smv
index a735f05..a9e12d2 100644
--- a/a2/src/2c.smv
+++ b/a2/src/2c.smv
@@ -1,8 +1,12 @@
 MODULE main
 DEFINE
-max1:=144; max2:=72; max3:=28;
+max1:=144;
+max2:=72;
+max3:=28;
 VAR
-b1: 0..max1; b2: 0..max2; b3: 0..max3;
+b1: 0..max1;
+b2: 0..max2;
+b3: 0..max3;
 INIT
 b1=3 & b2=0 & b3=0
 TRANS
diff --git a/a2/src/path.sh b/a2/src/path.sh
index d7dfea0..8d1a61c 100644
--- a/a2/src/path.sh
+++ b/a2/src/path.sh
@@ -1,2 +1 @@
-export PATH=$PATH:/home/mart/downloads/NuSMV-2.5.4/nusmv
-export PATH=$PATH:/home/mart/projects/NuSMV-2.6.0-Linux/bin
+export PATH=$PATH:/home/mart/downloads/NuSMV-2.6.0-Linux/bin
-- 
2.20.1