a2/src/1.py

   1 #!/usr/bin/env python3
   2 timebound = 1000
   3 names = ['s', 'a', 'b', 'c']
   4 nodes = range(len(names))
   5 connections = [
   6     ('s', 'a', 29), ('s', 'b', 21),
   7     ('a', 's', 29), ('a', 'b', 17), ('a', 'c', 32),
   8     ('b', 's', 21), ('b', 'a', 17), ('b', 'c', 37),
   9     ('c', 'a', 32), ('c', 'b', 37)]
  10 maxes = [120, 120, 200]
  11 inits = [30, 40, 145]
  12 truck = 300
  13 print("""\
  14 MODULE main
  15 DEFINE
  16 TIMEBOUND:={};
  17 VAR
  18 truck: 0..{};
  19 tstock: 0..{};
  20 time: 0..TIMEBOUND;""".format(timebound, len(nodes), truck))
  21 for stock, name in zip(maxes, names[1:]):
  22     print('{}stock: 0..{};'.format(name, stock))
  23 print('INIT')
  24 for init, name in zip(inits, names[1:]):
  25     print('{}stock= {} &'.format(name, init))
  26 print("""\
  27 truck=0 &
  28 tstock=300 &
  29 time=0
  30 TRANS
  31 case""")
  32
  33 for node, name in zip(nodes, names):
  34     print('FALSE & truck={} & time+50<TIMEBOUND:'.format(node))
  35     orsym = False
  36     for fr, to, time in connections:
  37         if fr != name:
  38             continue
  39         if orsym:
  40             print('|')
  41         print('next(time)=time+{}'.format(time))
  42         orsym = True
  43     print(';')
  44
  45 # The case where time already passed over the bound
  46 print('TRUE:')
  47 for name in names[1:]:
  48     print('\tnext({0}stock)={0}stock &'.format(name))
  49 print("""\
  50 \tnext(time)=time & next(tstock)=tstock & next(truck)=truck; esac
  51 LTLSPEC G ({})""".format(' & '.join('{}stock>0'.format(n) for n in names[1:])))
  52 """
  53 truck={} & time<={}: (
  54     -- Truck goes to A
  55     (
  56         next(time)=time+29 & next(truck)=1 &
  57         case
  58             tstock=0 & astock-0<=120:
  59                 next(astock)=astock+0 &
  60                 next(bstock)=bstock &
  61                 next(cstock)=cstock &
  62                 next(tstock)=tstock-0;
  63             tstock=1 & astock-1<=120:
  64                 next(astock)=astock+1 &
  65                 next(bstock)=bstock &
  66                 next(cstock)=cstock &
  67                 next(tstock)=tstock-1;
  68             ...
  69             tstock=120 & astock-1<=120:
  70                 next(astock)=astock+1 &
  71                 next(bstock)=bstock &
  72                 next(cstock)=cstock &
  73                 next(tstock)=tstock-1;
  74
  75         esac
  76     ) |
  77     -- Truck goes to B
  78     (next(time)=time+21 & next(truck)=2 &
  79
  80     )
  81 );
  82 -- Truck is in A
  83 truck=1 & time<=TIMEBOUND:(
  84     -- Truck goes to S
  85     (next(time)=time+21 & next(truck)=0) |
  86     -- Truck goes to B
  87     (next(time)=time+17 & next(truck)=2) |
  88     -- Truck goes to C
  89     (next(time)=time+32 & next(truck)=3)
  90 );
  91 -- Truck is in B
  92 truck=2 & time<=TIMEBOUND:(
  93     -- Truck goes to S
  94     (next(time)=time+21 & next(truck)=0) |
  95     -- Truck goes to A
  96     (next(time)=time+17 & next(truck)=1) |
  97     -- Truck goes to C
  98     (next(time)=time+32 & next(truck)=3)
  99 );
 100 -- Truck is in C
 101 truck=3 & time<=TIMEBOUND:(
 102     -- Truck goes to A
 103     (next(time)=time+32 & next(truck)=1) |
 104     -- Truck goes to B
 105     (next(time)=time+37 & next(truck)=2)
 106 );
 107 -- Time bound has passed...
 108 TRUE: (
 109     next(time)=time &
 110     next(truck)=truck &
 111     next(astock)=astock &
 112     next(bstock)=bstock &
 113     next(cstock)=cstock &
 114     next(tstock)=tstock
 115 );
 116 """