Another Alloy jug puzzle

jug.als

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