CristalCaveGem » LustreC

node SWITCH1 (set,reset,initial:bool) returns (level:bool);

let

  level = initial -> if set then true 

                     else if reset then false 

                     else pre(level);

tel

node SWITCH (set,reset,initial:bool) returns (level:bool);

let

  level = initial -> if set and not pre(level) then true

                     else if reset then false

                     else pre(level);

tel

--requires assert to be true

node top(set, treset, initial:bool) returns (OK:bool);

var level,level1:bool;

let

  level = SWITCH(set,treset,initial);

  level1 = SWITCH1(set,treset,initial);

  OK = if not(set and treset) then(level = level1) else true;

--  assert not(set and treset);

  --%PROPERTY OK=true;

tel