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已被設置爲假。另外，ewYellow將變爲false，但ewRed未設置爲true。

我會提示你使用一個枚舉變量的交通燈，而不是三個布爾值，像這樣：

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

Answer 2

如何定義兩種不同的狀態顯示爲街頭的NS和EW兩側TRAFIC燈？ 我已經寫了代碼示例，希望你覺得它有用......

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的轉換是平穩的並且不那麼危險！