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