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