27 lines
967 B
INI
27 lines
967 B
INI
(**********************************************)
|
|
(* Initial predicate and next-state relation. *)
|
|
(* Alternatively, you can comment out these *)
|
|
(* and use SPECIFICATION. *)
|
|
(**********************************************)
|
|
INIT PCInit
|
|
NEXT PCNext
|
|
|
|
(**********************************************)
|
|
(* Specify the values of declared constants. *)
|
|
(**********************************************)
|
|
\* CONSTANT MyConstant = {0, 1}
|
|
CONSTANT Ballot = {0, 1}
|
|
CONSTANT Acceptor = {a1, a2, a3}
|
|
CONSTANT Majority = {{a1, a2}, {a1, a3}, {a2, a3}}
|
|
CONSTANT RM = {r1, r2}
|
|
(**********************************************)
|
|
(* Formulas true in every reachable state. *)
|
|
(**********************************************)
|
|
\* INVARIANT MyInvariant
|
|
INVARIANT PCTypeOK
|
|
INVARIANT TCConsistent
|
|
|
|
(**********************************************)
|
|
(* Disable checking deadlock. *)
|
|
(**********************************************)
|
|
\* CHECK_DEADLOCK FALSE
|