Skip to content

Instantly share code, notes, and snippets.

@voila voila/jugs.als
Created Jul 3, 2019

Embed
What would you like to do?
Water Jugs puzzle in Alloy
/* Impose an ordering on the State. */
open util/ordering[State]
open util/integer
/* Stores the jugs level */
sig State { small, big:Int }
/* initial state */
fact { first.small = 0 && first.big = 0 }
pred emptyBig(s, s': State) {
s'.big = 0
s'.small = s.small
}
pred emptySmall(s, s': State) {
s'.big = s.big
s'.small = 0
}
pred fillBig(s, s': State) {
s'.big = 5
s'.small = s.small
}
pred fillSmall(s, s': State) {
s'.big = s.big
s'.small = 3
}
pred smallToBig(s, s': State) {
s'.big = smaller [plus [s.big, s.small], 5]
s'.small = larger [minus [plus [s.small, s.big], 5] , 0]
}
pred bigToSmall(s, s': State) {
s'.big = larger [minus [plus [s.big, s.small], 3], 0]
s'.small = smaller [plus [s.small, s.big] , 3]
}
fact {
all s: State - last, s': s.next {
bigToSmall [s, s'] or smallToBig [s, s'] or
fillBig [s, s'] or
fillSmall [s, s'] or
emptyBig [s, s'] or emptySmall [s, s']
}
}
check { last.big != 4 } for 7 State
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.