---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Queens.tla
---
-------------------------------- MODULE Queens ---------------------------------
EXTENDS Naturals, Sequences
(***************************************************************************)
(* Formulation of the N-queens problem and an iterative algorithm to solve *)
(* the problem in TLA+. Since there must be exactly one queen in every row *)
(* we represent placements of queens as functions of the form *)
(* queens \in [ 1..N -> 1..N ] *)
(* where queens[i] gives the column of the queen in row i. Note that such *)
(* a function is just a sequence of length N. *)
(* We will also consider partial solutions, also represented as sequences *)
(* of length \leq N. *)
(***************************************************************************)
CONSTANT N \** number of queens and size of the board
ASSUME N \in Nat \ {0}
(* The following predicate determines if queens i and j attack each other
in a placement of queens (represented by a sequence as above). *)
Attacks(queens, i, j) ==
\/ queens[i] = queens[j] \** same column
\/ queens[i] - queens[j] = i - j \** first diagonal
\/ queens[j] - queens[i] = i - j \** second diagonal
(* A placement represents a (partial) solution if no two different queens
attack each other in it. *)
IsSolution(queens) ==
\A i \in 1..Len(queens) - 1: \A j \in i + 1..Len(queens):
~Attacks(queens, i, j)
(* Compute the set of solutions of the N-queens problem. *)
Solutions == {queens \in [1..N -> 1..N]: IsSolution(queens)}
(***************************************************************************)
(* We now describe an algorithm that iteratively computes the set of *)
(* solutions of the N-queens problem by successively placing queens. *)
(* The current state of the algorithm is given by two variables: *)
(* - todo contains a set of partial solutions, *)
(* - sols contains the set of full solutions found so far. *)
(* At every step, the algorithm picks some partial solution and computes *)
(* all possible extensions by the next queen. If N queens have been placed *)
(* these extensions are in fact full solutions, otherwise they are added *)
(* to the set todo. *)
(***************************************************************************)
VARIABLES todo, sols
Init ==
/\ todo = {<<>>} \** << >> is a partial (but not full) solution
/\ sols = {} \** no full solution found so far
PlaceQueen == \E queens \in todo:
\** extend some partial solution by placing the next queen
LET nxtQ == Len(queens) + 1 \** number of queen to place
cols == \** set of columns on which queen can be placed without any
\** conflict with some queen already placed
{c \in 1..N: ~\E i \in 1..Len(queens):
Attacks(Append(queens, c), i, nxtQ)}
exts == {Append(queens, c): c \in cols} \** possible extensions
IN IF nxtQ = N \** completed solution
THEN
/\ todo' = todo \ {queens}
/\ sols' = sols \union exts
ELSE
/\ todo' = (todo \ {queens}) \union exts
/\ sols' = sols
vars == << todo, sols >>
Spec == Init /\ [][PlaceQueen]_vars /\ WF_vars(PlaceQueen)
TypeInvariant ==
/\ todo \in SUBSET Seq(1..N) /\ \A s \in todo: Len(s) < N
/\ sols \in SUBSET Seq(1..N) /\ \A s \in sols: Len(s) = N
(* The set of sols contains only solutions, and contains all solutions
when todo is empty. *)
Invariant ==
/\ sols \subseteq Solutions
/\ todo = {} => Solutions \subseteq sols
Termination == <>(todo = {})
(* Assert that no solutions are ever computed so that TLC displays one *)
NoSolutions == sols = {}
================================================================================
\* Modification History
\* Last modified Sat Dec 11 09:58:48 CET 2010 by merz
\* Created Sat Dec 11 08:50:24 CET 2010 by merz