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