nusmv

-1熱度

1回答

日食nuseen更新站點無法正常工作。

2熱度

1回答

我用這段代碼驗證了一個8位加法器。當我打印時，如果主模塊爲空，則可達狀態的數量爲1，如果包含整個主模塊，則爲2^32。報告可達狀態數量的差異是什麼？對於4位加法器，所報告的可達狀態數是2^16。如果n是位數，輸入狀態是2^n似乎是合乎邏輯的。其他所有州從哪裏來？我注意到當我添加行數a : adder (in1, in2);時，狀態會增加，但這只是通過實驗證實，這是增加狀態數量而不是加法器模塊本身。

0熱度

1回答

如何在NuSMV中定義全局常量？

我不知道如何在NuSMV聲明全局常量，在某種程度上類似於 #define n 5 在C。我如何在NuSMV中做到這一點？

1熱度

1回答

使用NuSMV進行模型檢查

確實在NuSMV中沒有像NULL，Nil，None這樣的值嗎？而且我們不應該爲過程建立模型，因爲模型應該重複電子電路？我的方案是我有一個UART連接器，一個主存儲器和一個進程，後者讀寫主內存並讀寫UART。在主存中有數據名爲K，應該保持不變。我們想證明，如果過程不寫入K' then the value of K`等於它的下一個值。我在想我的模型是否足夠精細，或者太抽象了。另外如果我使用正確的

1熱度

1回答

在NuSMV中構建UART的正式模型？

我正在學習模型檢查和NuSMV爲我的教育。我可以編輯和運行NuSMV代碼，並且對UART的功能和功能有一個公正的理解。我的任務是使用NuSMV正式模擬UART，但此時我不知道該怎麼做。我明白，UART傳輸一個字節爲八個連續的位，但我怎樣才能建模？我有一個互斥代碼爲出發點： >NuSMV.exe mutex.smv *** This is NuSMV 2.6.0 (compiled on We

1熱度

1回答

是否有選項可以提高NuSMV在規範運行期間可以使用的內存量？

在nusmv規範運行過程中，它需要幾個小時，最終導致「死亡9」的結果。如何加快執行速度？是否有選項可以提高NuSMV在規範運行期間可以使用的內存量？

2熱度

1回答

檢查SMV中的CTL規格

當我試圖檢查SM中的「EG（！s11included &！s10included）」時，它被報告爲false，並給出如下反例，我認爲相反它支持此CTL規範。我的CTL規範有什麼問題嗎？ -- specification EG (!s11included & !s10included) is false -- as demonstrated by the following execution s

0熱度

1回答

NuSMV實時CTL

我正在使用NuSMV，我試圖寫一個實時CTL屬性。我想知道是否有設置從一個狀態的步驟的方式，如： ((s.state = on) ABG (0..5 s.state = off)) 讀爲：if (s.state=on) is true，從該國和其他5個步驟物業(s.state= off) is true。我試圖寫這樣的東西，但它不起作用。你可以幫我嗎？否則，是否可以檢查從不是第一個狀態開始的

1熱度

1回答

NuSMV - 與模型

我試着寫下面的模型在NuSMV 換句話說，只有當X和Y是在狀態太糟糕ž變差。這是代碼我已經寫 MODULE singleton VAR state: {good, bad}; INIT state = good TRANS (state = good) -> next(state) = bad TRANS (state = bad) -> next(stat

0熱度

2回答

NuSMV未安裝

我無法在Windows 10 OS上安裝NuSMV-2.6.0-win64.I已成功下載該文件，但無法從已解壓縮的「bin」文件夾中安裝。