システムモデルをモデル検査用の遷移システムに変換する

Question

現在、システムプロトタイプを移行システムモデルに変換しようとしています。私はいくつかのLTLプロパティを持っており、モデル検査ツールNuSMVを使ってそれらのプロパティを検証したいと思います。私は、原子の性質や他の数学的な側面を定義してモデリングを始める方法に関する情報だけです。しかし、私はあなたが提供モデルはあなたに合わせて少し単純すぎることだと思う遷移システムのNuSMVで非常に単純なエンコードが

MODULE main() 
VAR 
    state : { GETINFO, ACK, SEND }; 
ASSIGN 
    init(state) := GETINFO; 
    next(state) := case 
    state = GETINFO : SEND; 
    state = SEND : ACK; 
    state = ACK  : {GETINFO, SEND}; 
    esac; 

だろう

Pictorial Representation of Model

Answer 1

問題の説明ですので、お手伝いしたいことに関する追加情報をお送りします。