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