// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // The module below implements the behavior of one of the wise men. The inputs// // are the colors of the hats of the other two wise men, and the output is // // true iff the wise men deduces that he was selected. The reason for the // // given decision is explained as follows: // // * In the first step, the wise men consider the case that there is only // // one blue hat. Thus, if one of the wise men sees two white hats, then // // he knows that he is the only one having a blue hat. In all other cases,// // nothing happens in the first step, since then there are more than one // // blue hats in the game. // // * In the second step, the wise men know that more than one hat is in the // // game. Thus, any of the wise men who see just one blue hat knows that he// // also has a blue hat. // // * At the third, day, the wise men know that more than two hats are in the// // game, so all have blue hats. // // ************************************************************************** // macro N=8; macro white = false; macro blue = true; module WiseMan(nat{N} ?idx,event [N]bool ?hat,select,event ?done,!itsMe) { nat{N} step,blueHatsSeen; // count the number of blue hats seen (except for the own one) blueHatsSeen = sum(i=0..N-1) (hat[i]==blue & i!=idx ? 1 : 0); weak immediate abort { // wait for blueHatsSeen steps while(step<blueHatsSeen) { next(step) = step + 1; w: pause; } // if it's not yet over, this wise men can be sure to have a blue hat emit(itsMe); } when(done); }