*** Author: Markus Triska triska@gmx.at
*** Date:   Sept. 19th 2005

mod WATER-JUGS is
	protecting INT .
	sort State .
	op jug : Nat Int Int -> State [ctor] .
	op _&_ : State State -> State [ctor assoc comm] .
	vars J1 J2 F1 F2 Cap Cap1 Cap2 : Int .
	rl [spill] : jug(J1,Cap,F1) => jug(J1,Cap,0) .
	rl [fill]  : jug(J1,Cap,F1) => jug(J1,Cap,Cap) .
	crl [transfer1] : jug(J1,Cap1,F1) & jug(J2,Cap2,F2) => jug(J1,Cap1,0) & jug(J2,Cap2,F2 + F1) if F1 > 0 /\ F2 + F1 <= Cap2 .
	crl [transfer2] : jug(J1,Cap1,F1) & jug(J2,Cap2,F2) => jug(J1,Cap1,F1 - (Cap2 - F2)) & jug(J2,Cap2,Cap2) if F1 > 0 /\ F1 - (Cap2 - F2) >= 0 .
endm