23 lines
750 B
INI
23 lines
750 B
INI
CONSTANT defaultInitValue = defaultInitValue
|
|
\* Add statements after this line.
|
|
(**********************************************)
|
|
(* Initial predicate and next-state relation. *)
|
|
(* Alternatively, you can comment out these *)
|
|
(* and use SPECIFICATION. *)
|
|
(**********************************************)
|
|
SPECIFICATION Spec
|
|
\*INIT Init
|
|
\*NEXT Next
|
|
|
|
(**********************************************)
|
|
(* Specify the values of declared constants. *)
|
|
(**********************************************)
|
|
CONSTANT N = 1
|
|
CONSTANT defaultInitValue = 0
|
|
|
|
(**********************************************)
|
|
(* Formulas true in every reachable state. *)
|
|
(**********************************************)
|
|
INVARIANT Mutex
|
|
|
|
\* CHECK_DEADLOCK FALSE
|