```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  A coffee can contains some black and white beans. The following process
//  is to be repeated as long as possible: Randomly select two beans from the
//  can. If they have the same color, throw them out, but put another black
//  bean in (enough extra black beans are available to do this). If they have
//  different colors, place the white one back into the can and throw the
//  black one away. What can be said about the color of the final bean based
//  on the number of white beans and the number of black beans initially in
//  the can?
//
//  Reference:  D. Gries. The Science of Programming. Springer, 1981.
//
//  Note that the variable "black" need to have larger range than the initial
//  value "black_in", since black beans are added in some cases. To avoid
//  the overflow, we give "black" the doubled bitwidth (which is more than
//  actually necessary).
//
// **************************************************************************

macro size = 32;

module CoffeeCan(
int{size} black_in, white_in,
white, int{size*size()} black,
) {
// initialization
assume(black_in + white_in > 0);
assume(black_in > 0);
assume(white_in > 0);

black = black_in;
white = white_in;

// algorithm

while(black+white >= 2) {
if(black==0) {
// -------- two white beans have been chosen ------
next(black) = black+1;
next(white) = white-2;
} else if(white<=1)
// -------- two black beans have been chosen ------
next(black) = black-1;
else
// -------- all cases are possible ----------------
choose
next(black) = black-1;
else {
next(black) = black+1;
next(white) = white-2;
}
pause;
}

} satisfies {

InvarWhite1 : assert (white_in % 2 == 0) -> A G (white % 2 == 0);
InvarWhite2 : assert (white_in % 2 == 1) -> A G (white % 2 == 1);
Termination : assert A F ready;
LastBeanBlack : assert
(black_in + white_in > 0) & (black_in > 0) & (white_in > 0) & (white_in % 2 == 0)
-> A G (ready -> (black == 1 & white == 0));
LastBeanWhite : assert
(black_in + white_in > 0) & (black_in > 0) & (white_in > 0) & (white_in % 2 != 0)
-> A G (ready -> (black == 0 & white == 1));

}
```