model-checking

1熱度

2回答

對於下面的代碼未得錯誤， proctype A() { byte cond1; time = time + 1; time = time + 2; t[0] = 3; a[0] = 2; do :: (a[0] == 0)->break; :: else -> a[0] = a[0] - 1; do :: (t[0] <= t[1])->break;

2熱度

1回答

如何用SPIN建模轉換系統

我是新來的自旋。我想檢查一個轉換系統是否滿足給定的LTL屬性。但我不知道如何在promela中建立一個轉換系統的模型。例如，下面顯示的轉換系統有兩個狀態，初始狀態爲s0。如何檢查是否滿足LTL屬性：<> q。有人知道如何在promela中描述這個問題嗎？順便說一下，如何在自旋中使用LTL的下一個操作員？

0熱度

1回答

在Promela中選擇語句要比等價的if語句慢得多？

所以我在我的Promela代碼中使用了以下行。 select(cycles: 26..31); 然而，這是造成狀態爆炸。我用下面的if聲明替換它，突然間州爆炸問題消失了。我上面顯示的select聲明是否應該等於下面的if聲明？這裏發生了什麼？ if :: cycles = 26; :: cycles = 27; :: cycles = 28; :: cycles = 29; :: c

1熱度

1回答

是否有可能在SPIN/PROMELA中檢查變量的最大值

在我的模型檢查代碼中，我只想找到某個變量的最大值。我現在使用的程序是有一個assert語句assert(var < MAX_VALUE)，並繼續以二進制搜索方式更改MAX_VALUE。然而，如果SPIN實際上有辦法在一次運行中給出一個變量的最大可能值，那將會好很多。我知道UPPAAL有一個sup運營商。 SPIN中是否有等價物？

1熱度

1回答

LTL公式的大小是多少？

就複雜性而言，LTL公式的大小通常表示爲| p |原子命題的數量，深度還是別的？在此先感謝！

3熱度

1回答

將'else'與I/O結合使用，看到';' 'if'

以下是導致此問題的代碼。 if :: ((fromProc[0] == MSG_SLEEP) && nempty(proc2clk[0])) -> proc2clk[0] ? fromProc[0]; // Woke up :: (!(fromProc[0] == MSG_SLEEP) && !(fromProc[0] == MSG_FIN)) ->

2熱度

1回答

UPPAAL：什麼導致時鐘停止運行

我目前正在運行我的UPPAAL模擬器。我的模擬器在某個點後停止運行代碼。這點取決於我提供的聲明。但我想知道大概什麼時候停止運行？有什麼觸發這個嗎？

4熱度

2回答

用於模型建模的LTL，CTL或TLA（內部有詳細說明）？

我目前正在寫我的碩士論文，面臨在時間邏輯中指定和驗證我的方法。我將很快解釋基本情況，但可以隨時索要詳細信息;-)基本上我想知道哪種時態邏輯最適合我的情況，並且真的很想反饋我的方法以及如何繼續。我的模型由參與者組成，它們將同時執行。對於每個參與者，都可以註冊規則。他們看起來像這樣：條件 - >動作，例如收到（a，c）^收到（b，c） - >允許（c，d）這意味着c必須從b收到一條消息，並從c收到

1熱度

1回答

在eclipse中解析smv文件

我下載了一個模型檢查器nusmv-tools（https://code.google.com/a/eclipselabs.org/p/nusmv-tools/）。我在eclipse上成功安裝了它及其依賴項（如xtext）並重新啓動了eclipse。現在，我希望eclipse能夠識別nusmv文件（哪個擴展名是'.smv'），但是它不能。我的問題是，我應該怎麼做才能在eclipse中解析nus

1熱度

1回答

用於點語言的非標準符號

我正在研究關於圖形語法建模（模型檢查）的research paper。爲了更好地理解，我開始研究人員運行exploring the experiments。他們用點符號指定圖形結構，並使用屬性，如labelangle=-35和type = "rt|re|node" 我找不到點語言互聯網上的任何很好的參考，他們沒有從一個新手的角度入手。當我搜索stackoverflow時，我覺得沒有標準的方式來指