| Hello, could you please be a bit more specific what you mean by "execution errors"? Once you add a suitable module header and footer (which you appear to have done judging from the LaTeX translation included with your posting), the input is syntactically correct. There are at least two strange aspects to your spec: the second last conjunct of action Pick constrains the value of i in the state before the transition, and action Max leaves the value of j' unspecified. TLC will complain about the second issue. I also find it strange that the initial values for i and j fixed by the initial condition are discarded in the Pick action. Below is a TLA+ module that describes the algorithm that you are apparently trying to specify, in a somewhat more direct fashion. You can create a model, indicate integer values for the constant parameters lower and upper (say, -30 and 30), and check the invariants TypeOK and Correctness. (Disable the default check for deadlock checking in a sequential program such as this one.) Best regards, Stephan ------------------------------- MODULE maxof2 ------------------------------- EXTENDS Integers CONSTANTS lower, upper ASSUME lower \in Int /\ upper \in Int /\ lower <= upper Range == lower .. upper null == CHOOSE x : x \notin Range VARIABLES i, j, max Init == /\ i \in Range /\ j \in Range /\ max = null Next == /\ max = null /\ max' = IF i > j THEN i ELSE j /\ UNCHANGED << i,j >> TypeOK == /\ i \in Range /\ j \in Range /\ max \in Range \cup {null} Correctness == max # null => max \in {i,j} /\ max >= i /\ max >= j =============================================================================
|