formal-verification - 如何将系统的安全要求转换为线性时间属性..？

Question

我在这里更清楚地改变了我的问题。有两种不同的模型，一种是发送者模型，一种是接收者模型。我想检查发送的消息与接收者接收的消息不同的属性。

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(state=receiver -> messageTransmited != messageReceived))