Another Alloy jug puzzle
open util/ordering[State] | |
sig Jug { | |
max: Int | |
} | |
abstract sig Op {} | |
sig Pour extends Op { | |
fromj: one Jug, | |
toj: one Jug | |
} | |
sig Fill extends Op { | |
jug: one Jug | |
} | |
sig Empty extends Op { | |
jug: one Jug | |
} | |
one sig Start extends Op {} | |
sig State { | |
jugAmounts: Jug -> one Int, | |
op: lone Op | |
} | |
fact jugCapacity { | |
all s: State { | |
all j: s.jugAmounts.univ { | |
j.(s.jugAmounts) >= 0 | |
and j.(s.jugAmounts) <= j.max | |
} | |
} | |
-- jugs start empty | |
first.jugAmounts = Jug -> 0 | |
first.op = Start | |
} | |
pred fill(s, s': State){ | |
one j: Jug { | |
let f = Fill { | |
f.jug = j | |
s'.op = f | |
} | |
j.(s'.jugAmounts) = j.max | |
all r: Jug - j | r.(s'.jugAmounts) = r.(s.jugAmounts) | |
} | |
} | |
pred empty(s, s': State){ | |
one j: Jug { | |
let e = Empty { | |
s'.op = e | |
e.jug = j | |
} | |
j.(s'.jugAmounts) = 0 | |
all r: Jug - j | r.(s'.jugAmounts) = r.(s.jugAmounts) | |
} | |
} | |
pred pour(s, s': State){ | |
some x: Int { | |
some from, to: Jug { | |
let p = Pour { | |
p.fromj = from | |
p.toj = to | |
s'.op = p | |
} | |
from.(s'.jugAmounts) = 0 or to.(s'.jugAmounts) = to.max | |
from.(s'.jugAmounts) = minus[from.(s.jugAmounts), x] | |
to.(s'.jugAmounts) = plus[to.(s.jugAmounts), x] | |
all r: Jug - from - to | r.(s'.jugAmounts) = r.(s.jugAmounts) | |
} | |
} | |
} | |
fact next { | |
all s: State, s': s.next { | |
fill[s, s'] | |
or empty[s, s'] | |
or pour[s, s'] | |
} | |
} | |
fact SpecifyPuzzle{ | |
-- all s: State | #s.jugAmounts = 2 | |
#Jug = 2 | |
one j: Jug | j.max = 5 | |
one j: Jug | j.max = 3 | |
} | |
assert no4 { | |
no s: State | 4 in univ.(s.jugAmounts) | |
--4 not in Jug.(State.jugAmounts) | |
} | |
check no4 for 7 but 2 Jug |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment