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