Generated SMV - 3

MODULE client(input)

VAR

out : {0,fetch,validate};

belief : {valid,invalid,suspect,nofile};

ASSIGN

init(belief) := {nofile, suspect};

next(belief) :=

case

(belief = nofile) & (input = val) : valid;

(belief = suspect) & (input = val) : valid;

(belief = suspect) & (input = inval) : invalid;

(belief = invalid) & (input = val) : valid;

1 : belief;

esac;

init(out) := 0;

next(out) :=

case

(belief = nofile) : fetch;

(belief = invalid) : fetch;

(belief = suspect) : validate;

1 : 0;

esac;

Previous slide

Next slide

Back to first slide

View graphic version