Светофор в НуСМВ

Причина того, что свойство F nsGreen = TRUE является ложным, заключается в том, что существует бесконечное выполнение, при котором nsGreen никогда не бывает истинным. Это контрпример, который генерирует NuSMV (я вырезал обратный отсчет таймера). Обратите внимание, что печатаются только обновления переменных.

-- specification  F nsGreen = TRUE  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  nsRed = TRUE
  nsYellow = FALSE
  nsGreen = FALSE
  time = 60
  ewRed = FALSE
  ewYellow = FALSE
  ewGreen = TRUE
-> State: 1.2 <-
  time = 59
  ...
-> State: 1.61 <-
  time = 0
-> State: 1.62 <-
  nsRed = FALSE
  time = 60
  ewYellow = TRUE
  ewGreen = FALSE
-> State: 1.63 <-
  time = 59
  ...
-> State: 1.122 <-
  time = 0
-> State: 1.123 <-
  time = 60
  ewYellow = FALSE
-> State: 1.124 <-
  time = 59
  ...
-> State: 1.182 <-
  time = 1
-- Loop starts here
-> State: 1.183 <-
  time = 0
-> State: 1.184 <-

Трассировка показывает, что nsRed уже имеет значение false, когда таймер достигает 0 в первый раз. Кроме того, ewYellow становится ложным, но ewRed не устанавливается в значение true.

Я бы предложил вам использовать переменную перечисления для светофоров вместо трех логических значений, например:

MODULE main
VAR
    ns : {RED, YELLOW, GREEN};
    ew : {RED, YELLOW, GREEN};

Как насчет определения двух разных состояний, указывающих на светофоры для северной и западной сторон улицы? Я написал пример кода, надеюсь, вы найдете его полезным...

MODULE main
VAR
    nsLight : {RED, YELLOW, GREEN};
    ewLight : {RED, YELLOW, GREEN};

    timeMove    : 0..10;
    timeYellow  : 0..5;

ASSIGN
init(nsLight)   := RED;
init(ewLight)   := GREEN;
init(timeMove)  := 10;
init(timeYellow):= 5;

--  NS:                                 |   EW:

--  R (10 sec) -> R ->   G (10 sec)     |   G (10 sec) -> Y (5 sec) ->   R (10 sec)
-- / \                   |              |   |                            |
--  |                   \ /             |   |                           \ /
--  |------------------- Y (5 sec)      |   |--------------------------- R


next(nsLight) := case
                    (nsLight = RED & ewLight = GREEN & timeMove = 0)        : RED;
                    (nsLight = RED & ewLight = YELLOW & timeYellow = 0)     : GREEN;
                    (nsLight = GREEN & ewLight = RED & timeMove = 0)        : YELLOW;
                    (nsLight = YELLOW & ewLight = RED & timeYellow = 0)     : RED;
                    TRUE                                                    : nsLight;
                esac;

next(ewLight) := case
                    (ewLight = GREEN & nsLight = RED & timeMove = 0)        : YELLOW;
                    (ewLight = YELLOW & nsLight = RED & timeYellow = 0)     : RED;
                    (ewLight = RED & nsLight = GREEN & timeMove = 0)        : RED;
                    (ewLight = RED & nsLight = YELLOW & timeYellow = 0)     : GREEN;
                    TRUE                                                    : ewLight;
                esac;

next(timeMove) := case
                    timeMove > 0 & ewLight != YELLOW & nsLight != YELLOW        : timeMove - 1;
                    timeMove = 0                                                : 10;
                    TRUE                                                        : timeMove;
                    esac;

next(timeYellow) := case
                    timeYellow > 0  & (ewLight = YELLOW | nsLight = YELLOW)     : timeYellow - 1;
                    timeYellow = 0                                              : 5;
                    TRUE                                                        : timeYellow;
                    esac;

Идея состоит в том, чтобы иметь движущийся счетчик из 10 -> 0, когда мы находимся в состояниях GREEN или RED, и еще один счетчик 5 -> 0, я назвал его timeYellow, чтобы переход от GREEN к YELLOW был плавным и менее опасным!