檢查SMV中的CTL規格

Question

當我試圖檢查SM中的「EG（！s11included &！s10included）」時，它被報告爲false，並給出如下反例，我認爲相反它支持此CTL規範。我的CTL規範有什麼問題嗎？

-- specification EG (!s11included & !s10included) is false 
-- as demonstrated by the following execution sequence 
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
    -> State: 9.1 <- 
    s00included = TRUE 
    s01included = TRUE 
    s10included = FALSE 
    s11included = FALSE 

Answer 1

簡短的回答：

沒有，沒有什麼不對您的CTL規格：你觀察什麼是正常的，完全取決於你的型號規格。

刀具打印反例到第一狀態（包括）違反一個給定的屬性。儘管對於操作人員來說這看起來有點武斷，因爲對於財產違規而言，原因有時可能從執行軌跡本身中隱藏起來，但是從模型檢查的角度來看，這種設計選擇是非常有意義的。 重要的是要注意結果是可信的，更重要的是，通過運行模擬進行雙重檢查。

---

例：

我請你看看下面的例子。

MODULE main 
VAR a : boolean; 
VAR b : boolean; 

ASSIGN 
next(a) := case 
    a = FALSE : { TRUE }; 
    TRUE  : { TRUE, FALSE }; 
    esac; 

next(b) := case 
    b = FALSE : { TRUE }; 
    TRUE  : { TRUE, FALSE }; 
    esac; 

CTLSPEC EG (!a & !b); 

在這種模式下，每當a（RESP。b）是FALSE我們確定地將它設置爲TRUE，否則我們允許它隨意改變。

如果我們檢查CTL屬性，這是完全一樣的你，我們得到以下反例：

NuSMV > reset; read_model -i test.smv ; go; check_property 
-- specification EG (!a & !b) is false 
-- as demonstrated by the following execution sequence 
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <- 
    a = FALSE 
    b = FALSE 

正如你所看到的，反例比賽你的100％。到底是怎麼回事？

嗯，基本上NuSMV保守地打印所需的最少數量的狀態，以達到違反財產的狀態。在這種情況下，執行軌跡的初始狀態的已經違反了屬性，因爲下，確定性的，過渡導致其中或者a或b是TRUE（在此特定情況下，兩個）的狀態：

NuSMV > pick_state -s 1.1 
NuSMV > simulate -iv -k 2 
******** Simulation Starting From State 3.1 ******** 

*************** AVAILABLE STATES ************* 

================= State ================= 
0) ------------------------- 
    a = TRUE 
    b = TRUE 


There's only one available state. Press Return to Proceed. 

Chosen state is: 0 

*************** AVAILABLE STATES ************* 

================= State ================= 
0) ------------------------- 
    a = TRUE 
    b = TRUE 


================= State ================= 
1) ------------------------- 
    b = FALSE 


================= State ================= 
2) ------------------------- 
    a = FALSE 
    b = TRUE 


================= State ================= 
3) ------------------------- 
    b = FALSE 


Choose a state from the above (0-3): ^C 

我的猜測是，你模式也有類似的行爲，這就是爲什麼你得到相同的結果的原因。