spin

0熱度

2回答

考慮這個片斷： chan sel = [0] of {int}; active proctype Selector(){ int not_me; endselector: do :: sel ? not_me; if :: 0 != not_me -> sel ! 0; :: 1 != not_me -> sel !

1熱度

1回答

自旋驗證與通道相關的屬性

我在Spin中創建了一個簡單模型，其中兩個進程S將消息發送到另一個進程R.進程R然後將響應發送到兩個進程。我想定義屬性「如果進程x發送消息，然後進程y最終接收它」，如下所示。問題是，雖然模擬工作正常，但驗證不是。我在第9行定義的屬性始終傳遞，沒有錯誤，儘管我在第17行注入了一個應該使驗證失敗的錯誤。我在這裏錯過了什麼嗎？ 1 byte r1PId; 2 byte s1PId; 3 byte s

1熱度

2回答

SPIN：解釋錯誤跟蹤

我試圖解決與農民，狼，山羊和捲心菜有關的任務。所以，我發現瞭如下因素PROMELA描述： #define fin (all_right_side == true) #define wg (g_and_w == false) #define gc (g_and_c == false) ltl ltl_0 { <> fin && [] (wg && gc) } bool all_righ

2熱度

1回答

在Promela中選擇數組元素的非確定性值是不可能的？

以下是我正在編寫的Promela代碼。 491 byte api1[5]; 492 byte api2[5]; 493 byte api3[5]; 494 byte reftask1[5] 495 byte reftask2[5]; 496 byte reftask3[5]; 497 byte rid1[5]; 498 byte rid2[5]; 499 byte

1熱度

1回答

與LTL公式

考慮找到一個變量的所有可能的執行最小值操縱共享變量N兩個過程以下Promela型號： byte N = 0; active [2] proctype P(){ byte temp, i; i = 1; do :: i < 10 -> temp = N; temp++; N = temp; i++;

2熱度

1回答

自旋驗證，驗證變量達到一定的數值

這是我在Stack Exchange上的第一個問題，所以如果有任何違規指標，請告訴我。我有一個用Promela編寫的大學OS和併發系統課程。有兩個進程正在運行，增加一個變量n。我們的任務是編寫這些流程，然後使用Spin中的驗證工具來證明n有可能獲得值4.我已經通讀了所有的命令行參數，但是沒有任何結果對我來說，「插入這個修飾符後跟一個變量名來檢查所有可能的值。」 byte n; proctyp

1熱度

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--; /*

0熱度

1回答

旋轉驗證錯誤

我在旋轉中創建了一個模型。仿真按預期運行。然而，當我嘗試驗證的LTL性質，我得到如下結果： C:/cygwin64/bin/gcc.exe -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c ./pan -m10000 -a Pid: 9372 pan:1: VECTORSZ is too small, edit pan.h (at depth 0) pa

0熱度

1回答

自旋：錯誤，生成此pan.c自旋的版本假定不同的字長（4-異8）

我使用Windows O.S和Cygwin的i型：wish -f ispin.tcl打開ispin接口。我打開一個文件其中包含： byte state = 2; proctype A() { (state == 1) -> state = 3 } proctype B() { state = state - 1 } init { run A(); run B() }

0熱度

1回答

只比較一個結構的一個屬性

當我嘗試比較我的結構的一個屬性（不是第一個屬性）時，我遇到了promela語言的問題。下面是一個例子： typedef Msg { byte header; byte content; } chan pipe = [5] of { Msg }; active proctype Receive() { Msg r; do :: ato