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

DieHard code implementation



Hi All,

I started learning TLA+ following the video course, I am so excited !

I am curious if somebody have already done some code implementation for the problem described in video #4, a.k.a  "DieHard".

I would like to see the code that implements such spec in different programming languages, my idea is that maybe we can submit the problem to http://www.rosettacode.org/ and analyse the implementation in different languages, in order to compare if certain kind of problem could be more easy to solve in language X rather than Y.

It seems that we could even submit a new language to rosettacode, actually there is no TLA+ at https://rosettacode.org/wiki/Category:Programming_Languages .

Well ... this is the TLA+ spec of DieHard that I have.

  ------------------------------ 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   == /\ big'   = 5
             /\ small' = small
             
EmptySmall == /\ small' = 0
              /\ big' = big
              
EmptyBig == /\ big' = 0
            /\ small' = small
            
SmallToBig == IF big + small <= 5
              THEN /\ big' = big + small
                   /\ small' = 0
              ELSE /\ big' = 0
                   /\ small' = small - (5 - big)

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

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

=============================================================================
\* Modification History
\* Last modified Sat Nov 03 16:45:21 COT 2018 by ndiaz
\* Created Sat Nov 03 10:26:29 COT 2018 by ndiaz