モデルチェッカーを使用して特定のトレースを確認してください

Question

私はオープン相互作用プロトコルのルールを定義するためにLTLを使用しています。私は、特定の対話が仕様に従っているかどうか、または何らかのルールが壊れていないかどうかを確認したい。私の直接のアプローチはNuSMVを使うことでしたが、問題は私がチェックしたい相互作用のモデルではなく、ただ一つの特定の有限のトレース（すべての状態のすべての変数の値）です。

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

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

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

ありがとうございます！

Answer 1

いくつかの考えの後、私はNuSMVモデルで特定のトレースをエンコードするソリューションを見つけました。それは非常に簡単です、トリックは、トレースの各状態に1つの変数を使用することです。

たとえば、私は対話をエンコードしたかったので、最後に発声されたメッセージだけが各状態で真であることを望みました。エンコードの相互作用は、[「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; 

私は多分それが誰かのために便利ですね！