process SpeedRegulator2 = { integer OFF, RUNNING, STDBY; real MSPEED, SPEED0, K; } ( ? event ONOFF_REG; event OFF_CAR; event PRESS_BRK_PED; event PRESS_ACC_PED; event REL_ACC_PED; real SPEED; event TOP; event REL_BRK_PED; ! real DELTA_TORQUE; ) (| STATE_BRK_PED ^= PRESS_BRK_PED ^+ REL_BRK_PED | STATE_BRK_PED := (true when PRESS_BRK_PED) default (false when REL_BRK_PED) default (STATE_BRK_PED$1) | STATE_ACC_PED ^= PRESS_ACC_PED ^+ REL_ACC_PED | STATE_ACC_PED := (true when PRESS_ACC_PED) default (false when REL_ACC_PED) default (STATE_ACC_PED$1) | STATE_BRK_PEDcONOFF_REG := STATE_BRK_PED cell ONOFF_REG init false | STATE_ACC_PEDcONOFF_REG := STATE_ACC_PED cell ONOFF_REG init false | SPEEDcONOFF_REG := SPEED cell ONOFF_REG init SPEED0 | ZSTATE_REG := STATE_REG$1 init OFF | STATE_REG ^= ONOFF_REG ^+ OFF_CAR ^+ PRESS_BRK_PED ^+ PRESS_ACC_PED ^+ REL_ACC_PED ^+ SPEED | STATE_REG := (OFF when (ONOFF_REG when ((ZSTATE_REG=RUNNING) or (ZSTATE_REG=STDBY)))) default (OFF when (PRESS_BRK_PED when ((ZSTATE_REG=RUNNING) or (ZSTATE_REG=STDBY)))) default (OFF when (OFF_CAR when ((ZSTATE_REG=RUNNING) or (ZSTATE_REG=STDBY)))) default (RUNNING when (ONOFF_REG when ((SPEEDcONOFF_REG>=MSPEED) when ((ZSTATE_REG=OFF) when ((not STATE_BRK_PEDcONOFF_REG) when (not STATE_ACC_PEDcONOFF_REG)))))) default (STDBY when (ONOFF_REG when ((SPEEDcONOFF_REG>=MSPEED) when ((ZSTATE_REG=OFF) when ((not STATE_BRK_PEDcONOFF_REG) when STATE_ACC_PEDcONOFF_REG))))) default (RUNNING when (REL_ACC_PED when (ZSTATE_REG=STDBY))) default (STDBY when (PRESS_ACC_PED when (ZSTATE_REG=RUNNING))) default (OFF when (((ZSTATE_REG=RUNNING) or (ZSTATE_REG=STDBY)) when (SPEED=MSPEED) when (ZSTATE_REG=RUNNING)) default ZSTATE_REG | OSPEED := SPEED cell ((when (STATE_REG=RUNNING)) when (ZSTATE_REG/=RUNNING)) init SPEED0 | STATE_REGcTOP := STATE_REG cell TOP init OFF | SPEEDcTOP := SPEED cell TOP init SPEED0 | OSPEEDcTOP := OSPEED cell TOP init SPEED0 | DELTA_TORQUE := Calculate(OSPEEDcTOP when TOP,SPEEDcTOP when TOP) when (STATE_REGcTOP=RUNNING) |) where integer STATE_REG, ZSTATE_REG, STATE_REGcTOP; boolean STATE_BRK_PED, STATE_ACC_PED, STATE_BRK_PEDcONOFF_REG, STATE_ACC_PEDcONOFF_REG; real OSPEED, OSPEEDcTOP, SPEEDcTOP, SPEEDcONOFF_REG; process Calculate = ( ? real OSPEED, SPEED; ! real DELTA_TORQUE; ) (| DELTA_TORQUE := K*(OSPEED-SPEED) |) ; end ;