+#!/bin/env python
+pegs = [(x, y) for x in range(7) for y in range(7) if
+ not (
+ (x < 2 and y < 2) or # exclude topleft
+ (x > 4 and y > 4) or # exclude bottomright
+ (x > 4 and y < 2) or # exclude topright
+ (x < 2 and y > 4)) # exclude bottomleft
+ ]
+holes = [(3,3)]
+var = ' '.join('p{}: boolean;'.format(i) for i in range(len(pegs)))
+init = ' & '.join('p{}={}'.format(i,
+ 'FALSE' if pegs[i] in holes else 'TRUE') for i in range(len(pegs)))
+a1 = '({})==1)'.format('+'.join('toint(p{})'.format(i) for i in range(len(pegs))))
+trans = ''
+for i in range(len(pegs)):
+ current = pegs[i]
+ top = (current[0], current[1]-1)
+ bottom = (current[0], current[1]+1)
+ left = (current[0]-1, current[1])
+ right = (current[0]+1, current[1])
+
+print """\
+MODULE main
+VAR
+{}
+INIT
+{}
+TRANS
+case {}
+{}
+LTLSPEC G !({})
+""".format(var, init, trans, win, a1)