Generated SMV - 2

MODULE server(input)

VAR

out : {0,val,inval};

belief : {none, valid,invalid};

valid-file : boolean;

ASSIGN

valid-file := {0,1};

init(belief) := none;

next(belief) :=

case

(belief = none) & (input = fetch) : valid;

(belief = none) & (input = validate) & valid-file : valid;

(belief = none) & (input= validate) & !valid-file : invalid;

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

1 : belief;

esac;

init(out) := 0;

next(out):=

case

(belief = none) & (input = fetch) : val;

(belief = none) & (input = validate) & valid-file : val;

(belief = none) & (input = validate) & !valid-file : inval;

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

1 : 0;

esac;

Previous slide

Next slide

Back to first slide

View graphic version