From f8ee085b0e3c66d5af59e037b69718f4c7fe52d8 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Mon, 23 Nov 2015 12:17:18 +0100 Subject: [PATCH] started with a2 --- a2/src/1.py | 116 +++++++++++++++++++++++++++++++++++++++++++++++++ a2/src/path.sh | 1 + 2 files changed, 117 insertions(+) create mode 100644 a2/src/1.py create mode 100644 a2/src/path.sh diff --git a/a2/src/1.py b/a2/src/1.py new file mode 100644 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+500'.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 index 0000000..9d9e771 --- /dev/null +++ b/a2/src/path.sh @@ -0,0 +1 @@ +export PATH=$PATH:/home/mart/downloads/NuSMV-2.5.4/nusmv -- 2.20.1