[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Error in spec
Sir,
Thanks for your valuable feedback, Now the spec is working. Last 3
months on wards I am learning TLA+ , simpler program is ok , but wen I
trying to specify some big programs , it will not working. I refer
TLA+ ebook also. When I listen TLA+ video course or ebook , example
programs are very less and all the key words, operators are not
showing , like some other programs ( C, C++ ) . so it is better to
learn TLA+ if it will provide keywords, operators and all other
features of TLA+
Regards
Renjith S
On Tue, Jul 24, 2018 at 3:09 PM, Stephan Merz <stepha...@xxxxxxxxx> wrote:
> I Modified the program with your suggestions , but TLC model checker
> shows 2 error ( provide value for constant lower and upper ) .
>
>
> This is normal behavior.
>
> but
> when i trying to add values for lower and upper , it will not working.
>
>
> Double-click on the constant you want to fix and enter the value in the form
> that opens, as an "ordinary assignment" (default), then click "Finish".
> Repeat for the other constant.
>
> Then click on the little "+" sign next to "Invariants" and add the formulas
> you wish to verify.
>
> Finally, click on the triangle in a green circle at the top left of the pane
> to run TLC.
>
> I believe you may want to watch some of the introductory videos [1] or
> peruse the Hyperbook [2] before writing and verifying your own
> specifications.
>
> Regards,
> Stephan
>
> [1] http://lamport.azurewebsites.net/video/videos.html
> [2] http://lamport.azurewebsites.net/tla/hyperbook.html
>
>
> 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.
>
>
> --
> 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.
>
>
> --
> 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.