2012-04-13 106 views
1

我試圖使用自旋模型檢查器來模擬兩個對象(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))) } 

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

回答

1

您的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,你最好在原子{}中同時改變它們。

+0

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

+0

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

+0

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