Re: [tlaplus] Error in spec

[Renjith Sasidharan <renjit...@xxxxxxxxx>]

Sir,

thanks for your valuable suggestion. I mean execution error is TLC
model checker error. When I create the model , TLC will not go to the
next state, its hang on initial state.
 I Modified the program with your suggestions , but TLC model checker
shows 2 error ( provide value for constant lower and upper ) . but
when i trying to add values for lower and upper , it will not working.
Pls help

regards

Renjith S





On Tue, Jul 24, 2018 at 12:45 PM, Stephan Merz <stepha...@xxxxxxxxx> wrote:
> 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
> =============================================================================
>
>
> On 24 Jul 2018, at 08:31, Renjith Sasidharan <renjit...@xxxxxxxxx> wrote:
>
> Sir,
>
> 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
> PDF
>
> EXTENDS Integers
> VARIABLES i,pc,j
> 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
>
> Regards
> 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.
> <maxof2.tex>
>
>
> --
> 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.