[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Error in spec


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,

------------------------------- 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

On 24 Jul 2018, at 08:31, Renjith Sasidharan <renjit...@xxxxxxxxx> wrote:


I m a beginner in TLA+ and my research area is Formal method .While i
m writing a spec in TLA+ , there occurs execution errors. I couldn't
rectify those errors pls correct it. I m attaching the spec also in

EXTENDS Integers
Init == (pc="start") /\ (i=0) /\ (j=2)
Pick == \/ /\ pc="start"
           /\ i' \in 0..1000
           /\ j' \in 2..1002
           /\ i = IF i>j THEN i ELSE j
           /\ pc'="middle"

Max  ==  \/  /\ pc="middle"
           /\  i' = IF i > j THEN i ELSE j
           /\  pc'="done"
Next == Pick \/ Max

renjith S
Dept of CSE
Amrita sChool of Engg

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.