我試圖使用自旋模型檢查器來模擬兩個對象(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))) }
但是,我仍然得到完全相同的錯誤跟蹤。
哦,是的,謝謝。我改變了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