started with a2

diff --git a/a2/src/1.py b/a2/src/1.py
new file mode 100644 (file)
index 0000000..2650336
--- /dev/null
+++ b/a2/src/1.py
@@ -0,0 +1,116 @@
+#!/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('next(time)=time+{}'.format(time))
+        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/path.sh b/a2/src/path.sh
new file mode 100644 (file)
index 0000000..9d9e771
--- /dev/null
+++ b/a2/src/path.sh
@@ -0,0 +1 @@
+export PATH=$PATH:/home/mart/downloads/NuSMV-2.5.4/nusmv