// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// To find out which husbands are faithful, the wives determine the following //
// protocol: Each wife behaves as follows: If there are n unfaithful husbands //
// then each of their wives knows that there are n-1 unfaithful husbands and  //
// maybe the own one, too. By induction, we can prove that if there were n-1  //
// unfaithful husbands, then these were shot at the n-1 th day. Thus, if the  //
// wives will not hear a gunshot at the n-1 th day, they will shoot their own //
// husband at the n-th day.                                                   //
//                                                                            //
// Examples:                                                                  //
//  If n=1 holds, then the wife with the unfaithful husband immediately knows //
// that her husband is the only one (since she knows that all other husbands  //
// are faithful). Therefore, she immediately shoots him at day 1.             //
//  If n=2 holds, then both their wives know the other unfaithful husband, and//
// therefore expect a gunshot at day 1. As they don't hear it, they know that //
// their own husband must also be faithful, and therefore shoot him at day 2. //
// ************************************************************************** //

macro NoHusbands = 8;
macro Unfaithful=5;

module Wife(nat ?UnfaithfulsKnown, event gunshot,!killed) {
    int i;
    // wait for UnfaithfulsKnown days
    while(i<UnfaithfulsKnown) {
        next(i) = i+1;
        pause;
    }
    // if this wife does not hear a gunshot in this night, she realizes that
    // her husband is unfaithful, and will shoot him at the next day
    if(!gunshot & UnfaithfulsKnown==Unfaithful-1) {
        pause;
        emit(gunshot);
        emit(killed);
    }
}