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
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
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 }
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
= 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.
++ 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}
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).
There must be a bug somewhere but my experience with Electrum is limited. Hope 