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

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



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, knnik...@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...@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.