123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170 |
- 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};
- selected_passenger_3 : {h1, w1, h2, w2, h3, w3, h4, w4, none};
- boat_crossed : boolean;
- husband1 : passenger(
- h1 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- wife1 : passenger(
- w1 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- husband2 : passenger(
- h2 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- wife2 : passenger(
- w2 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- husband3 : passenger(
- h3 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- wife3 : passenger(
- w3 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- husband4 : passenger(
- h4 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- wife4 : passenger(
- w4 in {selected_passenger_1, selected_passenger_2, selected_passenger_3}
- );
- ASSIGN
- init(boat_crossed) := FALSE;
- next(boat_crossed) := !boat_crossed;
- 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
- };
- 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
- };
- 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
- };
- -- new initialization constraints added
- -- in essence, same as we did in (b)
- init(selected_passenger_3) := {
- (selected_passenger_1 != h1 & selected_passenger_2 != h1) ? h1 : none,
- (selected_passenger_1 != w1 & selected_passenger_2 != w1) ? w1 : none,
- (selected_passenger_1 != h2 & selected_passenger_2 != h2) ? h2 : none,
- (selected_passenger_1 != w2 & selected_passenger_2 != w2) ? w2 : none,
- (selected_passenger_1 != h3 & selected_passenger_2 != h3) ? h3 : none,
- (selected_passenger_1 != w3 & selected_passenger_2 != w3) ? w3 : none,
- (selected_passenger_1 != h4 & selected_passenger_2 != h4) ? h4 : none,
- (selected_passenger_1 != w4 & selected_passenger_2 != w4) ? w4 : none
- };
- -- new transition added
- -- in essence, we do the same we did in (b), only this time making sure
- -- that selected_passenger_3 is unlike selected_passenger_1 and selected_passenger_2
- next(selected_passenger_3) := {
- next(boat_crossed) = husband1.crossed &
- next(selected_passenger_1) != h1 &
- next(selected_passenger_2) != h1 ?
- h1 : selected_passenger_2,
- next(boat_crossed) = wife1.crossed &
- next(selected_passenger_1) != w1 &
- next(selected_passenger_2) != w1 ?
- w1 : selected_passenger_2,
- next(boat_crossed) = husband2.crossed &
- next(selected_passenger_1) != h2 &
- next(selected_passenger_2) != h2 ?
- h2 : selected_passenger_2,
- next(boat_crossed) = wife2.crossed &
- next(selected_passenger_1) != w2 &
- next(selected_passenger_2) != w2 ?
- w2 : selected_passenger_2,
- next(boat_crossed) = husband3.crossed &
- next(selected_passenger_1) != h3 &
- next(selected_passenger_2) != h3 ?
- h3 : selected_passenger_2,
- next(boat_crossed) = wife3.crossed &
- next(selected_passenger_1) != w3 &
- next(selected_passenger_2) != w3 ?
- w3 : selected_passenger_2,
- next(boat_crossed) = husband4.crossed &
- next(selected_passenger_1) != h4 &
- next(selected_passenger_2) != h4 ?
- h4 : selected_passenger_2,
- next(boat_crossed) = wife4.crossed &
- next(selected_passenger_1) != w4 &
- next(selected_passenger_2) != 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
- ));
- is_jealous_h4 := (
- husband4.crossed != wife4.crossed & (
- wife4.crossed = husband1.crossed |
- wife4.crossed = husband2.crossed |
- wife4.crossed = husband3.crossed
- ));
- all_crossed := (
- husband1.crossed & wife1.crossed &
- husband2.crossed & wife2.crossed &
- husband3.crossed & wife3.crossed &
- husband4.crossed & wife4.crossed);
- LTLSPEC ! (
- G !(is_jealous_h1 | is_jealous_h2 | is_jealous_h3 | is_jealous_h4) &
- F all_crossed
- );
|