uni/fmi/fmi23block4/ex3.d.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, 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
  );