1

LTL を使用して、オープン インタラクション プロトコルのルールを定義しています。次に、特定のインタラクションが仕様に従っているかどうか、またはルールに違反していないかどうかを確認したいと思います。私の当面のアプローチは NuSMV を使用することでしたが、問題は、確認したい相互作用のモデルがなく、特定の有限トレース (すべての状態のすべての変数の値) が 1 つしかないことです。

NuSMV でこれを指定する方法はありますか? 基本的に、NuSMV が反例として出力するモデルの 1 つを入力したいと思います。

-> State: 1.1 <-
a = TRUE
b = FALSE
-> State: 1.2 <-
a = FALSE
-> State: 1.3 <-
a = TRUE

そして、それを確認してください。それとも、NuSMV はこのための間違ったツールですか?

ありがとう！

4

1 に答える 1

1

少し考えた後、特定のトレースを NuSMV モデルにエンコードする解決策を見つけました。それは非常に簡単です。秘訣は、トレースの各状態に対して 1 つの変数を使用することです。

たとえば、インタラクションをエンコードし、最後に発話されたメッセージのみが各状態で true になるようにしたいと考えていました。エンコードする相互作用が ['a','b','a'] の場合、NuSMV モデルは次のようになります。

MODULE main
VAR
a : boolean;
b : boolean;
state : {s0,s1,s2};

ASSIGN
init(a) := FALSE;
init(state) := s0;
next(a) := 
    case
        state = s0 : TRUE;
        state = s1 : FALSE;
        state = s2 : TRUE;
    esac;
next(b) := 
    case
        state = s0 : FALSE;
        state = s1 : TRUE;
        state = s2 : FALSE;
    esac;
next(state) := 
    case
        state = s0 : s1;
        state = s1 : s2;
        state = s2 : s2;
    esac;

多分それが誰かに役立つことを願っています!

于 2016-09-22T17:12:46.970 に答える