a2/src/4.py

   1 #!/bin/env python
   2 pegs = [(x, y) for x in range(7) for y in range(7) if
   3         not (
   4         (x < 2 and y < 2) or # exclude topleft
   5         (x > 4 and y > 4) or # exclude bottomright
   6         (x > 4 and y < 2) or # exclude topright
   7         (x < 2 and y > 4))   # exclude bottomleft
   8         ]
   9 holes = [(3,3)]
  10 var = ' '.join('p{}: boolean;'.format(i) for i in range(len(pegs)))
  11 init = ' & '.join('p{}={}'.format(i,
  12     'FALSE' if pegs[i] in holes else 'TRUE') for i in range(len(pegs)))
  13 a1 = '({})==1)'.format('+'.join('toint(p{})'.format(i) for i in range(len(pegs))))
  14 trans = ''
  15 for i in range(len(pegs)):
  16     current = pegs[i]
  17     top = (current[0], current[1]-1)
  18     bottom = (current[0], current[1]+1)
  19     left = (current[0]-1, current[1])
  20     right = (current[0]+1, current[1])
  21
  22 print """\
  23 MODULE main
  24 VAR
  25 {}
  26 INIT
  27 {}
  28 TRANS
  29 case {}
  30 {}
  31 LTLSPEC G !({})
  32 """.format(var, init, trans, win, a1)