123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123 |
- MODULE passenger(on_boat)
- VAR
- crossed : boolean;
- ASSIGN
- init(crossed) := FALSE;
- next(crossed) := on_boat ? !crossed : crossed;
- MODULE main
- VAR
- selected_passenger_1 : {h1, w1, h2, w2, h3, w3, h4, w4};
- selected_passenger_2 : {h1, w1, h2, w2, h3, w3, h4, w4, none};
- boat_crossed : boolean;
- husband1 : passenger(
- h1 in {selected_passenger_1, selected_passenger_2}
- );
- wife1 : passenger(
- w1 in {selected_passenger_1, selected_passenger_2}
- );
- husband2 : passenger(
- h2 in {selected_passenger_1, selected_passenger_2}
- );
- wife2 : passenger(
- w2 in {selected_passenger_1, selected_passenger_2}
- );
- husband3 : passenger(
- h3 in {selected_passenger_1, selected_passenger_2}
- );
- wife3 : passenger(
- w3 in {selected_passenger_1, selected_passenger_2}
- );
- husband4 : passenger(
- h4 in {selected_passenger_1, selected_passenger_2}
- );
- wife4 : passenger(
- w4 in {selected_passenger_1, selected_passenger_2}
- );
- ASSIGN
- init(boat_crossed) := FALSE;
- next(boat_crossed) := !boat_crossed;
- -- extended by a new pairing
- next(selected_passenger_1) := {
- next(boat_crossed) = husband1.crossed ? h1 : selected_passenger_1,
- next(boat_crossed) = wife1.crossed ? w1 : selected_passenger_1,
- next(boat_crossed) = husband2.crossed ? h2 : selected_passenger_1,
- next(boat_crossed) = wife2.crossed ? w2 : selected_passenger_1,
- next(boat_crossed) = husband3.crossed ? h3 : selected_passenger_1,
- next(boat_crossed) = wife3.crossed ? w3 : selected_passenger_1,
- next(boat_crossed) = husband4.crossed ? h4 : selected_passenger_1,
- next(boat_crossed) = wife4.crossed ? w4 : selected_passenger_1
- };
- -- extended by a new pairing
- init(selected_passenger_2) := {
- selected_passenger_1 != h1 ? h1 : none,
- selected_passenger_1 != w1 ? w1 : none,
- selected_passenger_1 != h2 ? h2 : none,
- selected_passenger_1 != w2 ? w2 : none,
- selected_passenger_1 != h3 ? h3 : none,
- selected_passenger_1 != w3 ? w3 : none,
- selected_passenger_1 != h4 ? h4 : none,
- selected_passenger_1 != w4 ? w4 : none
- };
- -- extended by a new pairing
- next(selected_passenger_2) := {
- next(boat_crossed) = husband1.crossed & next(selected_passenger_1) != h1 ? h1 : selected_passenger_2,
- next(boat_crossed) = wife1.crossed & next(selected_passenger_1) != w1 ? w1 : selected_passenger_2,
- next(boat_crossed) = husband2.crossed & next(selected_passenger_1) != h2 ? h2 : selected_passenger_2,
- next(boat_crossed) = wife2.crossed & next(selected_passenger_1) != w2 ? w2 : selected_passenger_2,
- next(boat_crossed) = husband3.crossed & next(selected_passenger_1) != h3 ? h3 : selected_passenger_2,
- next(boat_crossed) = wife3.crossed & next(selected_passenger_1) != w3 ? w3 : selected_passenger_2,
- next(boat_crossed) = husband4.crossed & next(selected_passenger_1) != h4 ? h4 : selected_passenger_2,
- next(boat_crossed) = wife4.crossed & next(selected_passenger_1) != w4 ? w4 : selected_passenger_2,
- none
- };
- DEFINE
- is_jealous_h1 := (
- husband1.crossed != wife1.crossed & (
- wife1.crossed = husband2.crossed |
- wife1.crossed = husband3.crossed |
- wife1.crossed = husband4.crossed
- ));
- is_jealous_h2 := (
- husband2.crossed != wife2.crossed & (
- wife2.crossed = husband1.crossed |
- wife2.crossed = husband3.crossed |
- wife2.crossed = husband4.crossed
- ));
- is_jealous_h3 := (
- husband3.crossed != wife3.crossed & (
- wife3.crossed = husband1.crossed |
- wife3.crossed = husband2.crossed |
- wife3.crossed = husband4.crossed
- ));
- -- extended by a pairing
- is_jealous_h4 := (
- husband4.crossed != wife4.crossed & (
- wife4.crossed = husband1.crossed |
- wife4.crossed = husband2.crossed |
- wife4.crossed = husband3.crossed
- ));
- -- extended by a pairing
- all_crossed := (
- husband1.crossed & wife1.crossed &
- husband2.crossed & wife2.crossed &
- husband3.crossed & wife3.crossed &
- husband4.crossed & wife4.crossed);
- -- extended by a pairing
- LTLSPEC ! (
- G !(is_jealous_h1 | is_jealous_h2 | is_jealous_h3 | is_jealous_h4) &
- F all_crossed
- );
|