Instantly share code, notes, and snippets.

@lynaghk /jug.als
Last active Aug 25, 2018

Embed
What would you like to do?
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