27 lines
929 B
INI
27 lines
929 B
INI
(**********************************************)
|
|
(* Initial predicate and next-state relation. *)
|
|
(* Alternatively, you can comment out these *)
|
|
(* and use SPECIFICATION. *)
|
|
(**********************************************)
|
|
\*INIT Init
|
|
\*NEXT Next
|
|
SPECIFICATION FairSpecP
|
|
|
|
(**********************************************)
|
|
(* Specify the values of declared constants. *)
|
|
(**********************************************)
|
|
\* CONSTANT MyConstant = {0, 1}
|
|
CONSTANT Data = {"Ann", "Beatrix", "Chris"}
|
|
CONSTANT Bad = Bad
|
|
(**********************************************)
|
|
(* Formulas true in every reachable state. *)
|
|
(**********************************************)
|
|
INVARIANTS TypeOKP
|
|
|
|
(**********************************************)
|
|
(* Disable checking deadlock. *)
|
|
(**********************************************)
|
|
\* CHECK_DEADLOCK FALSE
|
|
|
|
CONSTRAINT CheckLimits
|
|
PROPERTIES ABSSpec ABSFairSpec
|