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