sort

  Name = struct A | B ;

act

  empty, fill, done: Name ;
  lose_all, gain_some, lose_some, gain_all, pour: Name # Name # Nat ;

map 
  sizeA, sizeB, target: Nat;

eqn 
  sizeA = 5;
  sizeB = 8;
  target = 4;

proc

  Can(N:Name,n:Nat,m:Nat) =
    ( m != target ) -> (
      %% empty, if non-empty
      (m > 0) -> ( empty(N) . Can(N,n,0) ) +
      %% fill, if not full
      (m < n) -> ( fill(N) . Can(N,n,n) ) +
      %% pour all to other if not empty
      (m > 0) -> (
        sum M:Name . (
          lose_all(N,M,m) . Can(N,n,0) ) ) +
      %% pour some to other if not empty
      (m > 0) -> (
        sum l:Nat,M:Name . ( 
          ( (0 < l) && (l <= m) ) -> (
            lose_some(N,M,l) . Can(N,n,Int2Nat(m-l)) ) ) )  +
      %% pour all from other if not full
      (m < n) -> (
        sum M:Name . (
          gain_all(M,N,Int2Nat(n-m)) . Can(N,n,n) ) ) +
      %% pour some from other if not full
      (m < n) -> (
        sum l:Nat,M:Name . ( 
          ( (0 < l) && (l <= Int2Nat(n-m)) ) -> (
            gain_some(M,N,l) . Can(N,n,m+l) ) ) )
    ) <> done(N) ; 

init

  allow( 
    { empty, fill, done, pour },
  comm(
    { lose_all|gain_some -> pour, lose_some|gain_all -> pour },
  Can(A,sizeA,0) || Can(B,sizeB,0) 
    ));