uni/fmi/fmi23block4/ex3.b.smv

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};
    selected_passenger_2 : {h1, w1, h2, w2, h3, w3, 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}
    );
  ASSIGN
    init(boat_crossed) := FALSE;
    next(boat_crossed) := !boat_crossed;

    -- the next state logic of selected passenger 1 is simple, namely exactly as it was in task (a)
    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
    };

    -- this time, we prevent initialization of both passengers to the same person
    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
    };

    -- the next state of passenger 2 then depends on passenger 1
    -- to make unique choices for each selection, we additionally require that a passenger has not already been selected as selected passenger 1
    -- finally, because we need to allow the crossing of just one passenger, there is an additional none state
    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,
      none
    };

  DEFINE 

    -- the definition of the jealousness property is not too complicated, it first checks for unequivalence of the husband 1 and the wife 1, and then enumerates all equivalences of pairings of wife 1 with the other husbands
    -- equivalence in this case refers to the state where the crossing of a person is the same as that of another person
    -- so in essence we check whether the crossing value of husband 1 and wife 1 are not the same, but the crossing value of wife1 with any of the other husbands 2 or 3 is
    is_jealous_h1 := (
      husband1.crossed != wife1.crossed & (
        wife1.crossed = husband2.crossed |
        wife1.crossed = husband3.crossed
      ));

    -- this is the same as in the above explanation, but the roles of 1 and 2 are flipped
    is_jealous_h2 := (
      husband2.crossed != wife2.crossed & (
        wife2.crossed = husband1.crossed |
        wife2.crossed = husband3.crossed
      ));

    -- this is the same as in the above explanation, but the roles of 1 and 3 are flipped
    is_jealous_h3 := (
      husband3.crossed != wife3.crossed & (
        wife3.crossed = husband1.crossed |
        wife3.crossed = husband2.crossed
      ));

    -- all passengers have been crossed successfully if their crossings all evaluate to true
    all_crossed := (
      husband1.crossed & wife1.crossed &
      husband2.crossed & wife2.crossed &
      husband3.crossed & wife3.crossed);

  LTLSPEC ! (
    G !(is_jealous_h1 | is_jealous_h2 | is_jealous_h3) &
    F all_crossed
  );