Generated SMV (Syntax)

MODULE main

VAR

Client : client (Server.out);

Server : server (Client.out);

SPEC AG ((Client.belief = valid) ->

(Server.belief = valid))

SPEC AG ((Server.belief = valid) ->

(Client.belief = valid))

Previous slide

Next slide

Back to first slide

View graphic version