Description Class ControlledDynamicInterval

INTENTION

This class provides all definitions to describe a controlled dynamic interval. An interval is a subset of a specific domain and is given by a start (object start) and an end point (object end). The domain is given by the formal parameter INT_DOM. Furthermore, a predicate leq is provided indicating whether a value of the considered domain is less or equal to another value.
Dynamic means that the values of the start and end point of the interval can change over time. For both values the facility manager can prescribe a default value which is valid as long as a user has not entered a value. Therefore the start and end point are objects of the class ControlledInput.

FORMAL PARAMETERS

Sort	INT_DOM

Intention

:

This domain contains the values the start and end point of the interval have to belong to.

SIGNATURE

Object	start  :  ControlledInput(INPUT_DOM  =  INT_DOM)

Intention

:

This object represents the starting point of the interval. The entered value has to be an element of the domain INT_DOM.

Object	end  :  ControlledInput(INPUT_DOM  =  INT_DOM)

Intention

:

This object represents the end point of the interval. The entered value has to be an element of the domain INT_DOM.

Predicate	leq  :  INT_DOM,  INT_DOM

Intention	:	This predicate is true iff the first argument is less than or equal to the second argument.
Scope	:	mh

MACHINE SPECIFICATIONS

Property	M_CDI1

NL

:

The starting point of the interval is always less than or equal to the end point of the interval.