Re: [tlaplus] Not able to perform TLC Model Checking

Thanks Stephan. Now it's working :-). Previously I thought both come in that field automatically.

On Tuesday, February 27, 2018 at 7:57:14 PM UTC+5:30, Stephan Merz wrote:

Not sure I understand your question. If you are referring to the model checking pane of the Toolbox, you can either indicate Init and Next in the fields for the initial state predicate and the next-state relation, or you can enter Spec as the temporal formula defining your behavior spec. The model checker will then extract the initial state predicate and the next-state relation from the definition of Spec.

Regards,
Stephan

On 27 Feb 2018, at 15:14, knni...@xxxxxxxxx wrote:

Hi,

Am new in TLA+, am trying to solve DieHard problem and I wrote code to solve the same. But in the Initial Predicate and next state relation, My Init and Next state are not coming. The following is my code.

------------------------------ MODULE DieHard ------------------------------
EXTENDS Integers
VARIABLES small,big

TypeOK == /\ small \in 0 .. 3
/\ big \in 0 .. 5


Init == /\ big = 0
/\ small = 0


FillSmall == /\ small'=3
/\ big'= big
FillBig == /\ small'= small
/\ big' = 5
EmptySmall == /\ small'= 0
/\ big'= big
EmptyBig == /\ big' = 0
/\ small'=small

SmallToBig == IF big+small =< 5
THEN /\ big' = big + small
/\ small' = 0
ELSE /\ big' = big + (small-small')
/\ small' = big -small
BigToSmall == IF big+small =< 3
THEN /\ small' = big + small
/\ big' = 0
ELSE /\ big' = big - small
/\ small' = small + ( big - big')

Next == \/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall

Spec == Init /\ [][Next]_<<big, small>>

=============================================================================
\* Modification History
\* Last modified Tue Feb 27 19:39:03 IST 2018 by nikhila
\* Created Tue Feb 27 18:41:39 IST 2018 by nikhila

--
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...@googlegroups.com.
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.