// ************************************************************************** //
//                                                                            //
//    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 is a typical induction puzzle that appears in different dis- //
// guises, and is often also known as the "muddy children puzzle". The variant//
// below is taken from Wikipedia:                                             //
//   In Josephine's Kingdom every woman has to pass a logic exam before being //
// allowed to marry. Every married woman knows about the fidelity of every man//
// in the Kingdom except for her own husband, and etiquette demands that no   //
// woman should tell another about the fidelity of her husband.               //
// A gunshot fired in any house in the Kingdom will be heard in any other     //
// house. Queen Josephine announced that unfaithful men had been discovered   //
// in the Kingdom, and that any woman knowing her husband to be unfaithful was//
// required to shoot him at midnight following the day after she discovered   //
// his infidelity. How did the wives manage this?                             //
//   The interesting fact is here that the problem can only be solved by using//
// time as an additional factor of information, which is only possible if all //
// threads (i.e. wives) are synchronous processes.                            //
// ************************************************************************** //

macro NoHusbands = 8;
macro Unfaithful=5;

module JosephinesProblem(event gunshot) {
    [NoHusbands]bool isUnfaithful;
    [NoHusbands]bool killed;
    for(i=0..Unfaithful-1)
        isUnfaithful[i] = true;
    for(i=0..NoHusbands-1) do ||
        let(UnfaithfulsKnown = (i<Unfaithful ? Unfaithful-1 : Unfaithful))
        Wife(UnfaithfulsKnown,gunshot,killed[i]);
}
drivenby {
    await(gunshot);
}