Description Class ToggleActuator

INTENTION

This class provides all definitions to describe a toggle actuator. A toggle actuator is an actuator that can send a signal. This is modeled here by setting the adjusted value to 1. If there is no signal the adjusted value is 0.

Note that this class can be used to describe an actuator that already exists in the environment. Therefore, the properties $\mathit{D\_TA_1}$ and $\mathit{D\_TA_2}$ are characterized as domain knowledge. Otherwise, if the actuator does not exist, they have to be requirements/specifications.

BASE CLASSES

Class	Actuator(ENV_DOMAIN  =  BINARY, ADJUSTED_DOMAIN  =  BINARY)

Intention

:

All definitions of description class Actuator are also provided here using the values 0 and 1 as the possible values of the phenomenon existing in the real world and using the values 0 and 1 as the possible values that can be adjusted by the machine.

DOMAIN KNOWLEDGE

Property	D_TA1

Formal	:	( (  noMalAct. envEntity = 1 ) [  noMalAct. adjustedEntity = 1 ]                       noMalAct. reactionTime (  noMalAct. envEntity = 0 ) )
NL	:	If the value of the entity in the real world (envEntity) is 1 and a toggle signal arrives, i.e. the adjusted value (adjustedEntity) changes from 0 to 1, then within reactionTime milliseconds the value of the entity in the real world (envEntity) is 0.

Property	D_TA2

Formal	:	( (  noMalAct. envEntity = 0 [  noMalAct. adjustedEntity = 1 ] )                       noMalAct. reactionTime (  noMalAct. envEntity = 1 ) )
NL	:	If the value of the entity in the real world (envEntity) is 0 and a toggle signal arrives, i.e. the adjusted value (adjustedEntity) changes from 0 to 1, then within reactionTime milliseconds the value of the entity in the real world (envEntity) is 1.