From: Mart Lubbers Date: Fri, 4 Dec 2015 16:51:31 +0000 (+0100) Subject: small update X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=293eddf30010a53ab3fa3fca015b1f1c8ab1e504;p=ar1516.git small update --- 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< 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+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/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