add TLA+ version of N-Queens

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

N-Queens/queens_20.tla

+---- MODULE queens_20 ----
+
+EXTENDS Naturals, FiniteSets
+
+VARIABLE queens, n, solved
+----
+
+Init == /\ queens=[i \in 1..2 |-> 0]
+        /\ n=20
+        /\ solved = 0
+
+Solve == /\ solved=0
+         /\ queens' \in [1..n -> 1..n]
+         /\ \A i \in 1..n : (\A j \in 2..n : i<j => queens'[i] # queens'[j] /\ queens'[i]+i-j # queens'[j] /\ queens'[i]-i+j # queens'[j])
+         /\ solved'=1
+         /\ n'=n
+Spec == Init /\ [] [Solve]_<<n,queens>>
+
+VISB_JSON_FILE == "queens_20_tla.json"
+
+=======
+\* Generated at Tue Jun 22 21:06:17 CEST 2010
+\* TLC takes 2 seconds for n-6, 12 seconds to solve for n=7 
+\* and 4 minutes 9 seconds for n=8, 1h45min47sec for n=9
+\* ProB takes 0.01 seconds for n=8, both on MacBook Pro 3.06 GHz

N-Queens/queens_20_tla.json

+{
+  "svg":"queens_20.svg",
+  "definitions":[
+    { "name":"VISB_SVG_UPDATES1",
+      "value" : "ran(%i.(i:1..20|rec(`id`:\"svgQueen\"^TO_STRING(i), y:IF i:dom(queens) THEN 45*queens(i)-45 ELSE 0 END, visibility: IF i:dom(queens) THEN \"visible\" ELSE \"hidden\" END)))"
+    },
+    { "name":"VISB_SVG_UPDATES2",
+      "value" : "ran(%i.(i:1..20|rec(`id`:\"gTiles\"^TO_STRING(i), visibility: IF i<=n  THEN \"visible\" ELSE \"hidden\" END)))"
+    }
+  ],
+"events": [
+  ]
+}
+