 # DieHard in Electrum

The following model is a port of Leslie Lamports example ‘DieHard’ to Electrum.
Can the model be improved? Is there a more idiomatic ways to do this in Electrum?

``````module mfc/diehard

open util/integer

one sig State {
var Small: Int,
var Big: Int
}{
gte[Small, 0]
lte[Small, 3]
gte[Big, 0]
lte[Big, 5]
}

pred init {
eq[State.Small, 0]
eq[State.Big, 0]
}

pred fillSmall {
eq[State.Small', 3]
eq[State.Big', State.Big]
}

pred emptySmall {
eq[State.Small', 0]
eq[State.Big', State.Big]
}

pred fillBig {
eq[State.Big', 5]
eq[State.Small', State.Small]
}

pred emptyBig {
eq[State.Big', 0]
eq[State.Small', State.Small]
}

pred smallToBig {
let BS = add[State.Big, State.Small] |
lte[BS, 5] implies
(eq[State.Small', 0] and eq[State.Big', BS])
else
(eq[State.Big', 5] and eq[State.Small', sub[State.Small, sub[5, State.Big]]])
}

pred bigToSmall {
let BS = add[State.Big, State.Small] |
lte[BS, 3] implies
(eq[State.Big', 0] and eq[State.Small', BS])
else
(eq[State.Small', 3] and eq[State.Big', sub[State.Small, sub[3, State.Big]]])
}

fact traces {
init
always {
fillSmall or fillBig or
emptySmall or emptyBig or
smallToBig or bigToSmall
}
}

run{} for 5 int

assert BruceWillDie {
always (not eq[State.Big, 4])
}

check BruceWillDie for 5 int, 10 steps
``````

Do you have a description of the problem, or a link?

In the 1995 movie Die Hard Bruce Willis has to fill 4 gallons of Water in a jug. To do so he has 2 jugs one is a 3 gallon jug, the other a 5 gallon jug. They both do not have measurement divisions, one can just fill them or empty them or fill their content into the other jug. Bruce Willis will be saved if he succeeds in putting exactly 4 gallons in the bigger jug. See: Die hard 3 : Jugs Problem - YouTube

Ok, this is my model but to my embarrassment I cannot get it to find a solution There must be a bug somewhere but my experience with Electrum is limited. Hope @grayswandyr will correct my model

``````-- In the 1995 movie Die Hard Bruce Willis has to fill 4 gallons of Water in a jug.

abstract sig Jug {
var gallons : Int,
capacity : Int
} {
gallons <=  capacity
}

-- To do so he has 2 jugs one is a 3 gallon jug,
-- the other a 5 gallon jug.
one sig Jug3 extends Jug {} { capacity = 3 }
one sig Jug5 extends Jug {} { capacity = 5 }

-- They both do not have measurement divisions,
-- one can just fill them
pred fill[ j : Jug ] {
j.gallons' = j.capacity
all unchanged : Jug-j | unchanged.gallons' = unchanged.gallons
}

-- or empty them
pred empty[ j : Jug ] {
j.gallons' = 0
all unchanged : Jug-j | unchanged.gallons' = unchanged.gallons
}

--  or fill their content into the other jug.
pred pour[ from, to : Jug ] {
let 	amount = max[ to.capacity.minus[to.gallons] + from.gallons ] {
from.gallons' = from.gallons.minus[amount]
to.gallons' = to.gallons.plus[amount]
}
}

-- Bruce Willis will be saved if he succeeds in putting exactly 4 gallons in the bigger jug.

run {
all j : Jug  | j.gallons = 0
always (
one j : Jug | fill[j] || empty[j] || pour[j,Jug-j]
)
eventually Jug5.gallons = 4
} for 5 but 6 int
``````

Hi,

it was `min`, not `max`., in `pour`.
Also, I added a `skip` event (not necessary to get a solution here but it’s better to have one in a lot of models) and changed the `one` in `some` in the trace formula as, in general (even if it’s not necessary here), I think it’s better if events do not coincide due to frame conditions rather than due to a strong constraint on cardinality.

``````-- In the 1995 movie Die Hard Bruce Willis has to fill 4 gallons of Water in a jug.

abstract sig Jug {
var gallons : Int,
capacity : Int
} {
gallons <=  capacity
}

-- To do so he has 2 jugs one is a 3 gallon jug,
-- the other a 5 gallon jug.
one sig Jug3 extends Jug {} { capacity = 3 }
one sig Jug5 extends Jug {} { capacity = 5 }

-- They both do not have measurement divisions,
-- one can just fill them
pred fill[ j : Jug ] {
j.gallons' = j.capacity
all unchanged : Jug-j | unchanged.gallons' = unchanged.gallons
}

-- or empty them
pred empty[ j : Jug ] {
j.gallons' = 0
all unchanged : Jug-j | unchanged.gallons' = unchanged.gallons
}

--  or fill their content into the other jug.
pred pour[ from, to : Jug ] {
let 	amount = min[ to.capacity.minus[to.gallons] + from.gallons ] {
from.gallons' = from.gallons.minus[amount]
to.gallons' = to.gallons.plus[amount]
}
}

-- or do nothing
pred skip {
gallons' = gallons
}

-- Bruce Willis will be saved if he succeeds in putting exactly 4 gallons in the bigger jug.

run {
all j : Jug  | j.gallons = 0
always (
some j : Jug | fill[j] || empty[j] || pour[j,Jug-j] || skip
)
eventually Jug5.gallons = 4
} for 5 but 6 Int
``````

EDIT: if you feel at ease with the following style for updates of relations, this is shorter and even less error-prone:

``````pred fill[ j : Jug ] { gallons' = gallons ++ j->j.capacity }
``````
1 Like

Hi Peter,

I modified my spec by eliminating the redundancy and I think it gives the correct solution.
Furthermore I treid to use the normal arithmetic operators like = instead of eq etc. but at some point that didn’t give the solution anymore. I have no idea why.

``````abstract sig Jug {
var gallons : Int,
capacity : Int
}
one sig Jug3 extends Jug {} { capacity = 3 }
one sig Jug5 extends Jug {} { capacity = 5 }

pred fill[ j : Jug ] {
eq[j.gallons', j.capacity]
all unchanged : Jug-j | eq[unchanged.gallons', unchanged.gallons]
}

pred empty[ j : Jug ] {
eq[j.gallons',  0]
all unchanged : Jug-j | eq[unchanged.gallons', unchanged.gallons]
}

pred pour[ from, to : Jug ] {
let amount = add[from.gallons, to.gallons] |
lte[amount, to.capacity] implies
(eq[from.gallons', 0] and eq[to.gallons', amount])
else
(eq[to.gallons', to.capacity] and eq[from.gallons', sub[to.gallons, sub[to.capacity, from.gallons]]])
}

pred init {
all j: Jug | eq[j.gallons, 0]
}

fact traces {
init
always {
one j: Jug | fill[j] or empty[j] or pour[j, Jug-j]
}
}

assert BruceWillDie {
always (not eq[Jug5.gallons, 4])
}

check BruceWillDie for 5 int, 10 steps

run {} for 5 int
``````
1 Like

`=` shoud work ok so perhaps you made another mistake. In case you wrote `let amount = from.gallons + to.gallons`, notice that `+` on `Int` is not addition but union of two sets of integers.

Notice also that, contrary to TLA+, you don’t need to state the dual of what you want and state it as a check command, a run (like Peter showed) will work.

Finally, if you know TLA+, the `++` operation I was advocating for above corresponds to TLA+'s `EXCEPT`, here.

1 Like

`++` isn’t quite the same thing as `EXCEPT`, as `EXCEPT` overwrites values on functions, while `++` overwrites on relations. That matters if you have a non-functional relation:

``````{A -> B, B -> C, B -> D} ++ {B -> A} = {A -> B, B -> A}
``````

Notice both B-relations are overwritten here.

Thanks David! Appreciated. I was thrown off by the UNSAT core that seems to indicate that the `gallons = 0` in the `Jug` fact was involved. Never really learned to use it.

I had not thought of this style. However, and I recall we had this discussion before, the reason I tend to avoid it is that it feels like combining multiple actions into one and thus making it more complicated to understand. The older I get, the more I tend to write code that makes every step explicit.

One thing is clear to me, we really need some support like EXCEPT. In the PlusCal experiment I detected the necessary EXCEPT parts automatically and that really simplified the step. It is probably different in plain Alloy but at least a warning for forgotten variables would be great.

Again thanks, and sorry for making such a stupid mistake.

Glad you got it to work! Sorry I did not have the time to debug mine and prayed for @grayswandyr to do my penance Any reason you broke up the `run` body in 4 different parts? Personally, I find the single body a lot easier to read and maintain. The assert/check introduces a negation that makes it harder to understand imho. Curious why you made that change?

Absolutely, this why I said it was the same here (as `gallons` is a function), sorry if this wasn’t clear. OTOH, one can argue that TLA+'s EXCEPT is a special case of `++` (except (*) perhaps on relations with arity > 3, I don’t recall if there is a difference with Alloy).

(*) no pun intended.

Well, if you read that `gallons'` is `gallons` except (a relational except) for `j`, I think it’s more clear than having two formulas: