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