Re: DieHard code implementation

Hi Nestor,

here's the ECLIPSe version of the DieHard (aka bin-packing) problem: http://eclipseclp.org/wiki/Examples/BinPacking

Best regards,

Philippe

Le dimanche 4 novembre 2018 02:17:28 UTC+1, Nestor Diaz a écrit :

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