Description Class ControlledInput

INTENTION

This class contains all the definitions that are necessary to model the controlled input of a value by a user. This value is represented by the timed function value. Controlled means here that the facility manager prescribes an interval in which the value entered by a user has to be. Furthermore, the facility manager prescribes a default value (object default) which is valid as long as a user has not entered a value. As soon as a user has entered a value this becomes the actual value unless a user changes it by entering a new value. There is no other possibility to change the value.

FORMAL PARAMETERS

Sort	INPUT_DOM

Intention

:

This domain contains all the values that can be entered for the boundaries of the interval the facility manager can prescribe, for the default value given by the facility manager, and for the value entered by a user.

SIGNATURE

Object	allowedRange  :  DynamicInterval(INT_DOM  =  INPUT_DOM)

Intention

:

This object represents the range of possible user entries. This range is specified by the facility manager.

Object	default  :  EnteredValue(CHECKED_DOM  =  INPUT_DOM)

Intention

:

This object represents the default value given by the facility manager. Note that by this declaration it is only guaranteed that the default value is an element of the domain INPUT_DOM. It is not guaranteed that it is a value of the interval specified by the facility manager. This is expressed by the property $P\_CIN_3$ of this class.

Object	userValue  :  EnteredValue(CHECKED_DOM  =  INPUT_DOM)

Intention

:

This object represents the value entered by a user. Note that by this declaration it is only guaranteed that the entered value is an element of the domain INPUT_DOM. It is not guaranteed that it is a value of the interval specified by the facility manager. This is expressed by the property $P\_CIN_2$ of this class.

Timed Function	value   INPUT_DOM

Intention	:	This function represents the currently valid value. It depends on the inputs of the facility manager and the input of a user.
Scope	:	mh

Timed Predicate	userValueEntered

Intention	:	This predicate is true iff the user has entered a value.
Scope	:	mh

MACHINE SPECIFICATIONS

Property	I_CIN1

NL

:

Initially a value has not been entered by a user.

Property	I_CIN2

NL

:

The initially valid value is equal to the initial default value given by the facility manager.

Property	M_CIN1

NL

:

If a user has entered a value once, from this time point it will be valid that a value has been entered by a user.

Property	M_CIN2

NL

:

If a user has entered a value which is less than or equal to the lower bound of the allowed interval specified by the facility manager the currently valid value is equal to the lower bound of the interval specified by the facility manager. If a user has entered a value which is greater than the upper bound of the allowed interval specified by the facility manager the currently valid value is equal to the upper bound of the interval specified by the facility manager. Otherwise, if the entered value is within the interval specified by the facility manager, the currently valid value is equal to the value entered by a user.

Property	M_CIN3

NL

:

The default value given by the facility manager has always to be within the allowed range specified by the facility manager.