update

[ar1516.git] / a2 / src / 4.py

diff --git a/a2/src/4.py b/a2/src/4.py
new file mode 100644 (file)
index 0000000..b0b30f5
--- /dev/null
+++ b/a2/src/4.py
@@ -0,0 +1,32 @@
+#!/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)