次のLTLプロパティの単純なPromelaモデルをモデルチェックしようとしています:
ltl { M[0] U M[1] }
そして、エラーが発生しました。エラートレイルのガイド付きシミュレーションでは、次の出力が得られます。
ltl ltl_0: (M[0]) U (M[1])
spin: couldn't find claim 2 (ignored)
0 :init ini M[0] = 1
Process Statement M[0] M[1]
0 :init ini M[1] = 0 1 0
Starting net with pid 2
0 :init ini run net() 1 0
spin: trail ends after 4 steps
#processes: 2
4: proc 1 (net) petri:11 (state 13)
4: proc 0 (:init:) petri:25 (state 5)
2 processes created
Exit-Status 0
ここで、「M[0] until M[1]」がどこで違反されているのかわかりません。M[0] は init プロセスで 1 に設定され、M[1] が 1 になるまでそのままです。トレースが非常に早く終了するか、「stronguntil」のセマンティクスを完全に誤解している可能性があります。私はこれが事実であると確信しています...しかし、私は何が間違っていますか? Promela ファイル内の LTL の指定は大丈夫ですか?
問題のモデルは次のとおりです (単純なペトリネット)。
#define nPlaces 2
#define nTransitions 2
#define inp1(x1) (x1>0) -> x1--
#define out1(x1) x1++
int M[nPlaces];
int T[nTransitions];
proctype net()
{
do
:: d_step{inp1(M[0])->T[0]++;out1(M[1]);skip}
:: d_step{inp1(M[1])->T[1]++;out1(M[0]);skip}
od
}
init
{
atomic
{
M[0] = 1;
M[1] = 0;
}
run net();
}
ltl { M[0] U M[1] }