// ************************************************************************** //
//                                                                            //
//    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 directory WiseMenNonCausal does not work because //
// all decisions are made at once, which leads to cyclic dependencies among   //
// micro steps. If we make decisions per macro step, where in the first macro //
// step the wise men assume that there is exactly one blue hat, all wise men  //
// know at the n-th step that there are at least n blue hats around. This is  //
// an important information given by time, which allows us to break causality //
// cycles by time.                                                            //
// ************************************************************************** //

macro N=8;
macro white = false;
macro blue  = true;

module WiseMen(event [N]bool ?hat,select,event done) {
    loop {
        done = exists(i=0..N-1) select[i];
        pause;
    }
    ||
    for(i=0..N-1) do ||
        WiseMan(i,hat,select,done,select[i]);
}
drivenby one {
    // the king uses one blue hat
    weak immediate abort
        loop {
            for(i=0..0)   hat[i] = blue;
            for(i=1..N-1) hat[i] = white;
            pause;
        }
    when(done);
}
drivenby two {
    // the king uses two blue hats
    weak immediate abort
        loop {
            for(i=0..1)   hat[i] = blue;
            for(i=2..N-1) hat[i] = white;
            pause;
        }
    when(done);
}
drivenby three {
    // the king uses three blue hats
    weak immediate abort
        loop {
            for(i=0..2)   hat[i] = blue;
            for(i=3..N-1) hat[i] = white;
            pause;
        }
    when(done);
}