// ************************************************************************** // // // // 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: // * If both colors are white, the man knows that he must be the one that // // has been selected, since it is known that at least one of the three men// // was selected. // // * If one color is white and the other one is blue, then we make a case // // distinction on the own hat: If it would be white, then the man with the// // blue hat would state that he was selected, and therefore this man would// // not say so. If he does not do so, then the only reason for this is that// // he sees also a blue hat, and therefore this man can state that he was // // selected. // // * If both hats seen were blue, and the own hat would be white, then both // // other men would see a white and a blue hat, and therefore they would // // determine their selection by the rule above. Hence, if neither of them // // believes to be selected, it means that the own hat must be blue, and // // therefore one can state being selected. // // ************************************************************************** // macro white = false; macro blue = true; module WiseMan(event ?hat1,?hat2,?men1Selected,?men2Selected,!itsMe) { if(hat1==white & hat2==white) emit(itsMe); if(hat1!=hat2) if(!men1Selected & !men2Selected) emit(itsMe); if(hat1==blue & hat2==blue) if(!men1Selected & !men2Selected) emit(itsMe); }