// ************************************************************************** //
//                                                                            //
//    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 following contains an induction puzzle called "The King's Wise Men". It//
// is described in many different ways, e.g. also as "muddy children puzzle". //
// The following explanation was taken from Wikipedia:                        //
// The King called the three wisest men in the country to his court to decide //
// who would become his new advisor. He placed a hat on each of their heads,  //
// such that each wise man could see all of the other hats, but none of them  //
// could see their own. Each hat was either white or blue. The king gave his  //
// word to the wise men that at least one of them was wearing a blue hat - in //
// other words, there could be one, two, or three blue hats, but not zero. The//
// king also announced that the contest would be fair to all three men. The   //
// wise men were also forbidden to speak to each other. The king declared that//
// whichever man stood up first and announced the color of his own hat would  //
// become his new advisor. The wise men sat for a very long time before one   //
// stood up and correctly announced the answer. What did he say, and how did  //
// he work it out?                                                            //
// The solution offered in file  of the strategy of each of the men has //
// however, a severe flow in the cases where more than one blue hat is used.  //
// The problem is in these cases, a man would only state that he was selected //
// if the other two men would not do this. However, this leads to a cyclic    //
// dependency that cannot be constructively resolved.                         //
// ************************************************************************** //

macro white = false;
macro blue  = true;

module WiseMen(event ?hat1,?hat2,?hat3,men1Selected,men2Selected,men3Selected) {
    m1 : WiseMan(hat2,hat3,men2Selected,men3Selected,men1Selected);
    m2 : WiseMan(hat1,hat3,men1Selected,men3Selected,men2Selected);
    m3 : WiseMan(hat1,hat2,men1Selected,men2Selected,men3Selected);
}
drivenby one {
    // the king uses one blue hat
    hat1 = blue;
    hat2 = white;
    hat3 = white;
    }
drivenby two {
    // the king uses two blue hats; this is not constructive
    hat1 = blue;
    hat2 = blue;
    hat3 = white;
    }
drivenby three {
    // the king uses three blue hats; this is not constructive
    hat1 = blue;
    hat2 = blue;
    hat3 = blue;
    }