從Spin Modelchecker瞭解錯誤路徑

我試圖使用自旋模型檢查器來模擬兩個對象（A和B）之間的遊戲。物體在板上移動，每個位置由其（x，y）座標定義。這兩個物體應該不會相撞。我有三個進程：init，A Model，B Model。我的模型檢驗的LTL性質：（活躍度屬性來檢查，如果兩個物體永遠佔據相同的位置）從Spin Modelchecker瞭解錯誤路徑

ltl prop1 { [] (!(x_a == x_b) && !(y_a == y_b)) }

錯誤線索，我得到的是：初始化 - >模型 - > B型 - >初始化

但是，我不應該根據顯示的數據得到錯誤跟蹤（反例）：x_a = 2，x_b = 1，y_a = 1，y_b = 1。

另外，第一個init會經歷init進程的所有行，但第二個只會顯示到它的最後一行。

此外，我的A模型和B模型僅包含警衛和「do」塊中的操作，如下所示。但他們更復雜，如果有對的右塊「 - >」

active proctype AModel(){ 
do 
:: someValue == 1 -> go North 
:: someValue == 2 -> go South 
:: someValue == 3 -> go East 
:: someValue == 4 -> go West 
:: else -> skip; 
od 
}

我需要把任何東西在原子塊？我要問的原因是錯誤線索顯示的行甚至沒有進入'do'塊，它只是兩個模型的第一行。編輯： LTL屬性是錯誤的。我改變了：

ltl prop1 { [] (!((x_a == x_b) && (y_a == y_b))) }

但是，我仍然得到完全相同的錯誤跟蹤。

來源

2012-04-13 Sheerberenj

您的LTL資產被錯誤地實施。基本上，SPIN發現的反例是LTL所述的真實反例。

[] (!(x_a == x_b) && !(y_z == y_b)) => 
[] (!(2 == 1) && !(1 == 1)) => 
[] (!0 && !1) => 
[] (1 && 0) => 
[] 0 => 
false

的LTL應該是：

always not (same location) => 
[] (! ((x_a == x_b) && (y_a == y_b))) => 
[] (! ((2 == 1) && (1 == 1))) => 
[] (! (0 && 1) => 
[] (! 0) => 
[] 1 => 
true

關於你的初始化和任務。啓動任務時，您需要確保在任務運行之前完成初始化。我將使用兩種方法之一：

init { ... atomic { run taskA(); run taskB() } where tasks are spawned once all initialization is complete`

或

bool init_complete = false; 
init { ...; init_complete = true } 
proctype taskA() { /* init local stuff */ ...; init-complete -> /* begin real works */ ... }

你的LTL可能會初始化過程中失敗。

根據你的問題，如果你改變x或y，你最好在原子{}中同時改變它們。

來源

2012-04-15 03:57:24 GoZoner

哦，是的，謝謝。我改變了LTL屬性，但我仍然得到完全相同的錯誤跟蹤和反例。 – Sheerberenj 2012-04-15 15:46:43

我提供的LTL是否導致計數器示例（請參閱上文，它不應該）。 – GoZoner 2012-04-15 15:59:56

是的，它的確如此。這就是我困惑的原因。我覺得把東西放在原子塊中應該有問題。因爲最初我沒有在一個原子塊中擁有我的init進程，並且計數器示例只會轉到init的第一行。但是，在將init放入原子塊後，反例將遍歷init的所有行，然後僅遍歷A Model和B Model的第一行，然後是init的最後一行。 – Sheerberenj 2012-04-15 16:15:19

從Spin Modelchecker瞭解錯誤路徑

回答

相關問題