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
```