How can the performance of an Alloy model be improved?

Question

I've written two Alloy solutions to the "water pouring puzzle" (Given a 5 quart jug, a 3 quart jug, can you measure exactly 4 quarts?)

My first attempt (specific.als) hardcodes the two jugs as named relations:

sig State {
  threeJug: one Int, 
  fiveJug: one Int 
}

It solves the puzzle (finds a counterexample) in about 500ms.

My second attempt (generic.als) is coded to allow for an arbitrary number of jugs and different sizes:

sig State {
  jugAmounts: Jug -> one Int
}

It solves the puzzle in about 2000ms.

Is it possible for the generic code, to run as quickly as the specific code? What would need to be changed?

Specific Model

open util/ordering[State]


sig State {
  threeJug: one Int, 
  fiveJug: one Int 
}


fact {
  all s: State {
    s.threeJug >= 0
    s.threeJug <= 3
    s.fiveJug >= 0
    s.fiveJug <= 5
  }

  first.threeJug = 0
  first.fiveJug = 0
}


pred Fill(s, s': State){
  (s'.threeJug = 3 and s'.fiveJug = s.fiveJug)
  or (s'.fiveJug = 5 and s'.threeJug = s.threeJug)
}


pred Empty(s, s': State){
  (s.threeJug > 0 and s'.threeJug = 0 and s'.fiveJug = s.fiveJug)
  or (s.fiveJug > 0 and s'.fiveJug = 0 and s'.threeJug = s.threeJug)
}


pred Pour3To5(s, s': State){
  some x: Int {
    s'.fiveJug = plus[s.fiveJug, x]
    and s'.threeJug = minus[s.threeJug, x]
    and (s'.fiveJug = 5 or s'.threeJug = 0)
  }
}


pred Pour5To3(s, s': State){
  some x: Int {
    s'.threeJug = plus[s.threeJug, x]
    and s'.fiveJug = minus[s.fiveJug, x]
    and (s'.threeJug = 3 or s'.fiveJug = 0)
  }
}


fact Next {
  all s: State, s': s.next {
    Fill[s, s']
    or Pour3To5[s, s']
    or Pour5To3[s, s']
    or Empty[s, s']
  }
}


assert notOne {
  no s: State | s.fiveJug = 4
}


check notOne for 7

Generic Model

open util/ordering[State]


sig Jug {
  max: Int
}


sig State {
  jugAmounts: Jug -> one Int
}


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
}


pred fill(s, s': State){
  one j: Jug {
    j.(s'.jugAmounts) = j.max
    all r: Jug - j | r.(s'.jugAmounts) = r.(s.jugAmounts)
  }
}


pred empty(s, s': State){
  one j: Jug {
    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 {
      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
  one j: Jug | j.max = 5
  one j: Jug | j.max = 3
}


assert no4 {
  no s: State | 4 in univ.(s.jugAmounts)
}


check no4 for 7

Answer 1

By experience, better performance can be obtained by :

• Reducing the size of the search space ( by decreasing the scope, the number of sig and relations, the arity of relations,..)
• Simplifying constraints. Try to avoid using set comprehension and quantification as much as possible. As an example, your assertion, no s: State | 4 in univ.(s.jugAmounts) is logically equivalent to 4 not in univ.(State.jugAmounts). Making this tiny change alone in your model has already made the processing of clauses 200ms faster on my end.

EDIT

I came back to your problem during my free time.

Here's the model I used to reach this conclusion

module WaterJugs/AbstractSyntax/ASM
open util/ordering[State] 
open util/integer


//===== HARDCODE 2 jugs of volume 3 and 5 resp.  comment those lines for generic approach ====
one sig JugA extends Jug{}{
    volume=3
    water[first]=0
}
one sig JugB extends Jug{}{
    volume=5
    water[first]=0
}
//==================================================================

abstract sig Jug{
    volume: Int,
    water:  State  ->one Int
}{
    all s:State| water[s]<=volume and water[s]>=0
    volume >0
}

pred Fill(s1,s2:State){
    one disj j1,j2:Jug{j1.water[s1]!=j1.volume and j1.water[s2]=j1.volume and j2.water[s2]=j2.water[s1] }
}

pred Empty(s1,s2:State){
    one disj j1,j2:Jug{ j1.water[s1]!=0 and  j1.water[s2]=0 and  j2.water[s2]= j2.water[s1] }
}

pred Pour(s1,s2:State){
    one disj j1,j2: Jug{
        add[j1.water[s1],j2.water[s1]] >j1.volume implies {
            ( j1.water[s2]=j1.volume and j2.water[s2]=sub[j2.water[s1],sub[j1.volume,j1.water[s1]]])}
        else{
            ( j1.water[s2]=add[j1.water[s1],j2.water[s1]] and j2.water[s2]=0)
        }
    }
}

fact Next {
  all s: State-last{
    Fill[s, s.next]
    or Pour[s, s.next]
    or Empty[s, s.next]
  }
}

sig State{

}

assert no4 {
  4 not in Jug.water[State]
}

check no4 for 7

In bonus, here's a visualization of the counter exemple provided by Lightning