SMV Output

-- specification AG (Client.belief = valid -> Server... is true

-- specification AG (Server.belief = valid -> Client... is false

-- as demonstrated by the following execution sequence

state 1.1:

Client.out = 0

Client.belief = nofile

Server.out = 0

Server.belief = none

Server.valid-file = 0

state 1.2:

Client.out = fetch

state 1.3:

Server.out = val

Server.belief = valid

Previous slide

Next slide

Back to first slide

View graphic version