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