NuSMV 中的红绿灯

Question

我正在尝试在 NuSMV 中创建交通灯系统实现。现在我有 6 个布尔值用于 NS/EW 红色、黄色、绿色。但是，当我指定它们在未来状态下始终为真时，它会返回为假。如果有人在我的代码中看到任何错误，我将不胜感激。谢谢。

MODULE main
VAR
    nsRed : boolean;
    nsYellow : boolean;
    nsGreen : boolean;

    time : 0..60;

    ewRed : boolean;
    ewYellow : boolean;
    ewGreen : boolean;
ASSIGN
    init(nsRed) := TRUE;
    init(nsYellow) := FALSE;
    init(nsGreen) := FALSE;
    init(ewRed) := FALSE;
    init(ewYellow) := FALSE;
    init(ewGreen) := TRUE;
    init(time) := 60;
next(nsRed) :=
    case
        (nsYellow = TRUE & (ewGreen = TRUE | ewYellow = TRUE) & time = 0) : TRUE;
        (nsRed = TRUE & time = 0) : FALSE;
        TRUE : nsRed;
    esac;
next(nsYellow) :=
    case
        (nsGreen = TRUE & ewRed = TRUE & time = 0) : TRUE;
        (nsYellow = TRUE & time = 0) : FALSE;
        TRUE : nsYellow;
    esac;
next(nsGreen) :=
    case
        (nsRed = TRUE & ewRed = TRUE & time = 0) : TRUE;
        (nsGreen = TRUE & time = 0) : FALSE;
        TRUE : nsGreen;
    esac;

next(ewRed) :=
    case
        (ewYellow = TRUE & (nsGreen = TRUE | nsYellow = TRUE) & time = 0) : TRUE;
        (ewRed = TRUE & time = 0) : FALSE;
        TRUE : ewRed;
    esac;
next(ewYellow) :=
    case
        (ewGreen = TRUE & nsRed = TRUE & time = 0) : TRUE;
        (ewYellow = TRUE & time = 0) : FALSE;
        TRUE : ewYellow;
    esac;
next(ewGreen) :=
    case
        (ewRed = TRUE & nsRed = TRUE & time = 0) : TRUE;
        (ewGreen = TRUE & time = 0) : FALSE;
        TRUE : ewGreen;
    esac;

next(time) :=
    case
        (time > 0) : time - 1;
        (time = 0 & nsRed = TRUE) : 60;
        (time = 0 & nsYellow = TRUE) : 60;
        (time = 0 & nsGreen = TRUE) : 3;
        (time = 0 & ewRed = TRUE) : 60;
        (time = 0 & ewYellow = TRUE) : 60;
        (time = 0 & ewGreen = TRUE) : 3;
        --(time = 0 & nsRed = TRUE & ewRed = TRUE) : 3
        TRUE : time;
    esac;

-- specification 
SPEC AG !(nsRed = TRUE & nsYellow = TRUE)
SPEC AG !(nsGreen = TRUE & nsRed = TRUE)
SPEC AG !(nsGreen = TRUE & ewGreen = TRUE)
SPEC AG !(nsYellow = TRUE & ewYellow = TRUE)
SPEC AG !(nsRed = TRUE & ewRed = TRUE)
SPEC AG (nsRed = TRUE | nsYellow = TRUE | nsGreen = TRUE | ewRed = TRUE | ewYellow = TRUE | ewGreen = TRUE)
--LTLSPEC F nsGreen = TRUE
LTLSPEC F ewGreen = TRUE

Answer 1

属性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 <-

跟踪显示，当计时器第一次达到 0 时，nsRed 已设置为 false。此外，ewYellow 变为 false，但 ewRed 未设置为 true。

我建议您对红绿灯使用枚举变量而不是三个布尔值，如下所示：

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

Answer 2

如何定义两个不同的状态来指示街道 NS 和 EW 侧的红绿灯？ 我已经写了一个示例代码，希望对你有用...

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;

我们的想法是在我们处于GREEN 或RED 的状态时从10 -> 0 移动计数器和另一个计数器5 -> 0，我称之为timeYellow，以确保从GREEN 到 YELLOW 流畅且危险性更小！