plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/data/fm_library/eml_behavior/rampdown/raw.smv

      VAR ramp_mode : { RAMPING_DOWN, RAMPING_DONE };
      ASSIGN
      init(ramp_mode) := RAMPING_DOWN;
      next(ramp_mode) := case
      is_nominal: RAMPING_DOWN;
      is_fault & varout - decr > end_value: RAMPING_DOWN;
      TRUE: RAMPING_DONE;
      esac;