promela

1熱度

1回答

對於使用從未聲稱驗證（帶ispin），我得到depth reached產出比 Full statespace search for: never claim + (REQ5) assertion violations + (if within scope of claim) cycle checks - (disabled by -DSAFETY)

1熱度

1回答

使用SPIN測試多個LTL公式

我有很多LTL公式，我試圖在同一.pml文件上進行測試。我的問題是，當在任何單個公式中發現錯誤時，跟蹤文件被寫入（或覆蓋）到相同的跟蹤文件名。我一直無法找到寫入我選擇的跟蹤文件名的方法。有誰知道這個選項是否存在？如果不是，我可以使用什麼策略同時測試同一.pml文件中的多個ltl公式，而不必每次都覆蓋相同的跟蹤文件？我知道SPIN運行時-x選項，但這只是防止覆蓋的跟蹤文件。它不會生成具有不同名稱

1熱度

1回答

如何在promela中實現重複直到（條件）循環？

這將是正確的方法做： repeat{ ... } until(<condition>) 在PROMELA ？我曾嘗試： do:: //.. (condition) -> break; od 和 do :: //.. if::(condition) -> break; else fi; od

2熱度

1回答

在SPIN公式中使用（U）ntil運算符公式

我想了解如何在ltl公式中正確使用Until運算符。我發現this定義（見下文）是明確的： ù NTIL 甲û B：如果存在真實我使得：中的B是真[s i，s i + 1，s i + 2，... ] 對於所有的j，使得0≤Ĵ< I，式A是真[秒Ĵ，S J + 1，S J + 2， ...] 含義： B是在時間真我爲0和i-1之間的時間中，式A爲真仍在使用的形式化「真實在時間i」示例代碼與

-2熱度

1回答

如何使用Spin從命令行檢查Promela代碼

我在查看如何在Windows 10命令行上使用Spin分析train.pml的輸出。任何幫助，使文件給出正確的輸出將不勝感激。

-1熱度

1回答

自旋和PROMELA工作

首先，我總是達到深度的這個問題：0。我嘗試了所有可能性。其次，我想達到ltl公式中提到的那些州。那麼這個語法是否正確？

1熱度

1回答

爲什麼promela模型會超時？

我正在研究一個相當簡單的promela模型。使用兩個不同的模塊，它充當人行橫道/交通燈。第一個模塊是輸出當前信號的交通燈（綠色，紅色，黃色，待定）。該模塊還接收作爲輸入的稱爲「行人」的信號，該信號用作行人想穿過的指示器。第二個模塊充當人行橫道。它接收來自交通燈模塊的輸出信號（綠色，黃色，綠色）。它將行人信號輸出到交通燈模塊。這個模塊簡單地定義行人是否在穿越，等待或不在場。我的問題是，在Spin中運

1熱度

1回答

Promela使用Spin建模

1熱度

2回答

參考Promela LTL聲明中的以前狀態

我開始使用Promela，並且在表達一些LTL公式時遇到問題。一個示例是以下sequence值，我想斷言是單調增加。直覺上我想在下一個狀態中寫，順序是> =其前值，但是通過查看文檔，我沒有看到一種方式來表達這一點。有沒有一種方法來表達這種類型的公式？ byte sequence = 0; ltl p0 { [] sequence >= prev(sequence) } ... process

2熱度

1回答

使用SPIN進行LTL模型檢查

我正在查看SPIN軟件。我想用它來找到LTL理論的模型。所有的手冊和教程討論驗證算法的屬性，但我根本不感興趣。我只想找到LTL公式的模型（我猜想是相應的Büchi自動機），就像mace4或paradox模型檢測器可以找到FOL公式的模型。我相信SPIN應該能夠做到這一點，但我無法在文檔中找到它。有人能指出任何有用的資源嗎？