SPIN：無限次地訪問語句

我想知道是否有可能在程序中驗證LTL屬性，該公共約束聲明多個語句必須無限次地執行。SPIN：無限次地訪問語句

例如爲：

bool no_flip; 
bool flag; 

active[1] proctype node() 
{ 
    do 
    :: skip -> progress00: no_flip = 1 
    :: skip -> progress01: flag = 1 
    :: !no_flip -> flag = 0 
    od; 
} 

// eventually we have flag==1 forever 
ltl p0 { <> ([] (flag == 1)) }

這個程序是正確的當且僅當最終no_flip標誌變爲真和flag爲真。

但是，運行'pan -a'和'pan -a -f'（弱公平性）會產生一條通過no_flip=1聲明和接受狀態（來自LTL公式）的循環。

我認爲進度標籤會強制執行通過他們的執行無限次，但似乎並非如此。那麼，是否有可能增加這種公平性約束？

感謝，努諾

來源

2013-10-03 Nuno Lopes

就列入進度標籤本身並不能保證執行將被限制在無進度的情況。您需要在您的ltl或never索賠中的某處添加「非進度」。

作爲never聲明，您使用<>[](np_)強制執行進度（使用spin -p '<>[](np_)'生成永不聲明本身）。一個可能的ltl形式爲您的驗證是：

ltl { []<>!(np_) && <>[](flag==1) }

還要注意的是做「進步」並不意味着來訪每個進度標籤無限頻繁地;這意味着無限次地訪問任何進度標籤。因此，在執行進度時，通過代碼的可行路徑是第一個do選項 - 這不是您所期望的。

來源

2013-10-14 22:40:31 GoZoner

感謝您的回答。不幸的是，我不明白你的意思。我認爲我無法直接將LTL公式寫入從未聲稱。你能否展示如何用公平約束來擴展上面的例子？謝謝！ –

我更新了我的答案。運行您的示例仍然會導致違規行爲 - 我在'note' – GoZoner

中解釋了這一點，謝謝！那麼，是否有任何常規的技巧來解決這個問題？我假設可能會重寫程序以使其「工作」（即以某種方式限制公平調度）。 –

回答我自己的問題，對於這個簡單的例子，我可以將每個循環分支分割成單獨的進程。然後通過在弱公平模式下運行泛，我保證每個進程都將最終安排。然而，這個「解決方案」對我來說並不是很有趣，因爲我在每個過程中都有一個有數十個分支的模型。還有其他想法嗎？

bool no_flip; 
bool flag; 

active[1] proctype n1() 
{ 
    do 
    :: skip -> no_flip = 1 
    od; 
} 

active[1] proctype n2() 
{ 
    do 
    :: skip -> flag = 1 
    od; 
} 

active[1] proctype n3() 
{ 
    do 
    :: !no_flip -> flag = 0 
    od; 
} 

// eventually we have flag==1 forever 
ltl p0 { <>[] (flag == 1) }

來源

2013-10-16 13:59:02

SPIN：無限次地訪問語句

回答

相關問題