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回答

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

    1熱度

    1回答

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

    2熱度

    1回答

    我想了解如何在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回答

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

    -1熱度

    1回答

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

    1熱度

    1回答

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

    1熱度

    1回答

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

    1熱度

    2回答

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

    2熱度

    1回答

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