plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/examples/fe/dynamic/generator.smv

----------------------
-- MODULE generator --
----------------------

MODULE generator(cmd)

VAR
  active: boolean;
  voltage: {high, low};

ASSIGN
  init(active):= cmd = on;
  next(active):= case
                   cmd = on: TRUE;
                   cmd = off: FALSE;
                   TRUE: active;
                 esac;

  voltage := high;


-------------------
-- MODULE device --
-------------------

MODULE device(voltage)

-- device is not alive if voltage goes to low for at least 2 time steps

VAR counter: 0..2;

ASSIGN
  init(counter):= case
                  voltage = high: 0;
                  TRUE: 1;
                esac;
  next(counter):= case
                  voltage = high: 0;
                  voltage = low & counter < 2: counter+1;
                  TRUE: 2;
                esac;

DEFINE
  alive:= (counter < 2);


-----------------
-- MODULE main --
-----------------

MODULE main

VAR
  mode: {primary_mode, spare_mode};
  primary: generator(cmd_primary);
  spare:   generator(cmd_spare);
  cmd_primary: {on, off, nop};
  cmd_spare: {on, off, nop};
  voltage: {high, low};
  dev:     device(voltage);

ASSIGN
  -- initially in primary mode
  -- goes to spare mode and stays there, if primary voltage is low

  init(mode) := primary_mode;
  next(mode) := case
                  mode = primary_mode & primary.voltage = high: primary_mode;
                  TRUE: spare_mode;
                 esac;

  voltage:= case
              mode = primary_mode: primary.voltage;
              TRUE: spare.voltage;
            esac;

  init(cmd_primary):= on;
  next(cmd_primary):= case
                        mode = primary_mode & primary.voltage = low: off;
                        TRUE: nop;
                      esac;

  init(cmd_spare):= off;
  next(cmd_spare):= case
                        mode = primary_mode & primary.voltage = low: on;
                        TRUE: nop;
                      esac;

INVARSPEC NAME alive:=  dev.alive;