formal-verification - システムの安全要件を線形時間特性に変換する方法..?

Question

ここで問題をより明確に変更しました。送信側モデルと受信側モデルの 2 つの異なるモデルがあります。送信されたメッセージが受信者が受信したものと同じではないというプロパティを確認したい。

MODULE main()
VAR 
    state : { informationsource, getinformation, transmitter, receiver, destination, ACK }; 
    messageReceived : boolean;
    messageTransmitted : boolean;

ASSIGN
    init(state) := informationsource; 
    init(messageReceived) := FALSE;


    next(state) := case 
        state = informationsource : getinformation; 
        state = getinformation : transmitter; 
        state = transmitter : receiver; 
        state = receiver  & messageReceived = TRUE : destination;
        TRUE : {destination, ACK} ;

    esac;

LTLSPEC (G(状態=受信者 -> messageTransmited != messageReceived))