Template Declaration EnteredValue

INTENTION

This class provides all definitions to describe the entering of a value using an appropriate device (in our case this device is a control panel). For a value e that is entered (expressed by the function entered) a value c (expressed by the function checked) is determined using the function nearestValue. This function is intended to check the entered value e whether it is a valid value and returns the valid value which is nearest to e. Whether an entered value is a valid one is represented by the timed predicate unreasonableInput

It is assumed that there exists up to now no possibility to enter the value. Hence, the development of such a device is part of the overall development of the machine. Thus, this device is part of the machine. In our case this device is the control panel, which still has to be developed. Therefore the timed function entered has the scope ev and the timed function checked has the scope mh. Furthermore the optative statements are machine specifications.

Postreferences	:	lsref MalfunctionSensor : manualEnteredVal
		lsref MalfunctionSensor : manualEnteredMal
		lsref MalfunctionActuator : manualEnteredMal
		lsref AreaCtrlPanelFM : lightOff
		lsref AreaCtrlPanelFM : unoccDelay
		lsref RoomCtrlPanel : chosenLightScene
		lsref RoomCtrlPanel : winCeilLightSwitch
		lsref RoomCtrlPanel : wallCeilLightSwitch
		lsref RoomCtrlPanel : winCeilLightDimmer
		lsref RoomCtrlPanel : wallCeilLightDimmer
		lsref RoomCtrlPanel : lightSceneSwitch
		lsref RoomCtrlPanel : reoccDelay
		lsref RoomCtrlPanel : defaultLightScene
		lsref MalfunctionOccupancy : manualEnteredOcc
		lsref MalfunctionOccupancy : manualEnteredMal

FORMAL PARAMETERS

Sort	VALID_INPUTS

Intention	:	This domain contains the valid values and by this the values that can be produced out of an entered value using the function nearestValue.
Postreferences	:	lsref EnteredValue : checked
		lsref EnteredValue : nearestValue

SIGNATURE

Time Constant	checkTime

NL	:	time for checking
Intention	:	This time constant represents the maximal time needed to check a value, entered by a person, using the function nearestValue.
Scope	:	ev
Prereferences	:	pdref NF9
Postreferences	:	msref EnteredValue : M_EV1
		dkref MalfunctionSensor : D_MS1
		dkref MalfunctionSensor : D_MS2

Timed Function	entered  STRING

NL	:	entered value
Intention	:	This function represents the value entered by a person. The value is represented as a string.
Scope	:	ev
Prereferences	:	pdref NF9
Postreferences	:	msref EnteredValue : M_EV1
		dkref MalfunctionSensor : D_MS1
		dkref MalfunctionSensor : D_MS2

Timed Function	checked   VALID_INPUTS

NL	:	checked value
Intention	:	This function represents the value decided by the machine to use. checked is determined out of entered using the function nearestValue.
Scope	:	mh
Prereferences	:	pdref NF9
Postreferences	:	msref MalfunctionSensor : M_MS4
		msref AreaCtrlPanelFM : I_M_ACPFM1
		msref AreaCtrlPanelFM : I_M_ACPFM2
		msref MalfunctionOccupancy : M_MO2
		msref Room : M_R3
		msref Room : M_R7
		msref EnteredValue : M_EV1
		msref MalfunctionSensor : M_MS3
		msref Room : M_R2
		msref Room : M_R5
		msref Room : M_R6
		msref RoomCtrlPanel : I_M_RCP7
		msref MalfunctionActuator : M_MA1
		msref RoomCtrlPanel : I_M_RCP1
		msref RoomCtrlPanel : I_M_RCP2
		msref RoomCtrlPanel : I_M_RCP3
		msref RoomCtrlPanel : I_M_RCP4
		msref RoomCtrlPanel : I_M_RCP5
		msref RoomCtrlPanel : I_M_RCP6
		msref RoomCtrlPanel : I_M_RCP8
		msref RoomCtrlPanel : I_M_RCP9
		msref RoomCtrlPanel : I_M_RCP10
		msref MalfunctionOccupancy : I_M_MO1
		msref Room : M_R4
		msref MalfunctionOccupancy : M_MO1
		msref MalfunctionOccupancy : I_M_MO5
		rsref Area : R_A1
		msref Area : M_A3
		msref Room : M_R8
		msref Room : M_R8b
		msref Room : M_R9

Timed Predicate	unreasonableInput

Intention	:	This predicate is true if and only if the last entered value does not belong to the sort VALID_INPUTS, i.e., if it is an unreasonable input.
Scope	:	mh
Prereferences	:	pdref NF9
Postreferences	:	msref EnteredValue : I_M_EV1
		msref AreaCtrlPanelFM : M_ACPFM1
		msref RoomCtrlPanel : M_RCP1

Function	nearestValue  : STRING   VALID_INPUTS

Intention	:	This function returns the value which is the nearest one in the domain VALID_INPUTS w.r.t. the first argument.
Scope	:	mh
Prereferences	:	pdref NF9
		pdref PD_30
Postreferences	:	msref EnteredValue : M_EV1
		msref MalfunctionSensor : M_MS1
		msref MalfunctionSensor : M_MS2

MACHINE SPECIFICATIONS

Property	I_M_EV1

Formal	:	unreasonableInput
NL	:	Initially there is no unreasonable input, i.e., initially the last entered value belongs to the sort VALID_INPUTS.

Property	M_EV1

Formal	:	( entered  checkTime nearestValue  checked)
NL	:	The checked value is always derived from the entered value using the function nearestValue. A change of the entered value is always propagated within the time checkTime.
Prereferences	:	pdref PD_30