1
是否有可能使用Spin獲取屬性的多個(或全部)違規痕跡?要求在Spin中有多個(或全部)違規痕跡
舉個例子,我創建了下面的PROMELA型號:
byte mutex = 0;
active proctype A() {
A1: mutex==0; /* Is free? */
A2: mutex++; /* Get mutex */
A3: /* A's critical section */
A4: mutex--; /* Release mutex */
}
active proctype B() {
B1: mutex==0; /* Is free? */
B2: mutex++; /* Get mutex */
B3: /* B's critical section */
B4: mutex--; /* Release mutex */
}
ltl {[] (mutex < 2)}
它有一個天真的互斥實現。人們可以預期流程A和B不會一起到達他們的關鍵部分,並且我寫了一個LTL表達式來檢查它。
運行
spin -run mutex_example.pml
表明財產是無效的,並運行
spin -p -t mutex_example.pml
表明違反財產語句序列。
Never claim moves to line 4 [(1)]
2: proc 1 (B:1) mutex_example.pml:11 (state 1) [((mutex==0))]
4: proc 0 (A:1) mutex_example.pml:4 (state 1) [((mutex==0))]
6: proc 1 (B:1) mutex_example.pml:12 (state 2) [mutex = (mutex+1)]
8: proc 0 (A:1) mutex_example.pml:5 (state 2) [mutex = (mutex+1)]
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!((mutex<2))))
Never claim moves to line 3 [assert(!(!((mutex<2))))]
spin: trail ends after 9 steps
#processes: 2
mutex = 2
9: proc 1 (B:1) mutex_example.pml:14 (state 3)
9: proc 0 (A:1) mutex_example.pml:7 (state 3)
9: proc - (ltl_0:1) _spin_nvr.tmp:2 (state 6)
這表明語句序列(由標籤指示)「B1」 - >「A1」 - >「B2」 - >「A2」違反屬性但也有其他的交織選擇通向該(例如'A1' - >'B1' - >'B2' - >'A2')。
我可以問Spin給我多個(或全部)痕跡嗎?
在我的例子,兩個過程(A和B)都是有限的,所以反例的數量必須是有限的。 –
這裏的要點是系統地找到一些反例。我不能保證,使用不同的搜索參數,我不會找到相同的計數器例子許多次... :( –
@BraulioHorta你是對的,我會相應地更新答案。 –