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('(', end='')
  42         print('next(time)=time+{} &'.format(time))
  43         print(')')
  44         orsym = True
  45     print(';')
  46
  47 # The case where time already passed over the bound
  48 print('TRUE:')
  49 for name in names[1:]:
  50     print('\tnext({0}stock)={0}stock &'.format(name))
  51 print("""\
  52 \tnext(time)=time & next(tstock)=tstock & next(truck)=truck; esac
  53 LTLSPEC G ({})""".format(' & '.join('{}stock>0'.format(n) for n in names[1:])))
  54 """
  55 truck={} & time<={}: (
  56     -- Truck goes to A
  57     (
  58         next(time)=time+29 & next(truck)=1 &
  59         case
  60             tstock=0 & astock-0<=120:
  61                 next(astock)=astock+0 &
  62                 next(bstock)=bstock &
  63                 next(cstock)=cstock &
  64                 next(tstock)=tstock-0;
  65             tstock=1 & astock-1<=120:
  66                 next(astock)=astock+1 &
  67                 next(bstock)=bstock &
  68                 next(cstock)=cstock &
  69                 next(tstock)=tstock-1;
  70             ...
  71             tstock=120 & astock-1<=120:
  72                 next(astock)=astock+1 &
  73                 next(bstock)=bstock &
  74                 next(cstock)=cstock &
  75                 next(tstock)=tstock-1;
  76
  77         esac
  78     ) |
  79     -- Truck goes to B
  80     (next(time)=time+21 & next(truck)=2 &
  81
  82     )
  83 );
  84 -- Truck is in A
  85 truck=1 & time<=TIMEBOUND:(
  86     -- Truck goes to S
  87     (next(time)=time+21 & next(truck)=0) |
  88     -- Truck goes to B
  89     (next(time)=time+17 & next(truck)=2) |
  90     -- Truck goes to C
  91     (next(time)=time+32 & next(truck)=3)
  92 );
  93 -- Truck is in B
  94 truck=2 & time<=TIMEBOUND:(
  95     -- Truck goes to S
  96     (next(time)=time+21 & next(truck)=0) |
  97     -- Truck goes to A
  98     (next(time)=time+17 & next(truck)=1) |
  99     -- Truck goes to C
 100     (next(time)=time+32 & next(truck)=3)
 101 );
 102 -- Truck is in C
 103 truck=3 & time<=TIMEBOUND:(
 104     -- Truck goes to A
 105     (next(time)=time+32 & next(truck)=1) |
 106     -- Truck goes to B
 107     (next(time)=time+37 & next(truck)=2)
 108 );
 109 -- Time bound has passed...
 110 TRUE: (
 111     next(time)=time &
 112     next(truck)=truck &
 113     next(astock)=astock &
 114     next(bstock)=bstock &
 115     next(cstock)=cstock &
 116     next(tstock)=tstock
 117 );
 118 """