// **************************************************************************
//
//    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,
    event !ready
) {
    // 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;
  }
  emit (ready);

} 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));

}