CONSTANTS
  Number_Of_Boxes = 3

SPECIFICATION Spec

(* Предикат, который должен быть истинен во всех возможных мирах *)
INVARIANT TypeOK

(* Указание предиката, который должен быть проверен на истиность *)
(* Если он истинен, модель считается корректной *)
PROPERTY Victory