INTENTION
This class extends the description class BasicRoom with the definitions concerning those objects of which in each room at least one instantiation is installed but where the concrete number of instantion can vary from room to room.
In addition to the objects introduced in description class BasicRoom each room is equipped with
FORMAL PARAMETERS
Function | numRad NAT |
---|
Intention | : | This parameter represents the number of radiators that belong to a room. |
Function | numDoorHallway NAT |
---|
Intention | : | This parameter represents the number of doors of a room to the hallway. |
BASE CLASSES
Class | BasicRoom |
---|
Intention |
: | All definitions of description class BasicRoom are also provided here. |
SIGNATURE
Object | rad : Radiator[ numRad] |
---|
Intention | : | Each object represents one radiator of a room. |
Postreferences | : | msref Room : M_R3 |
Object | hallwayDoor : Door[ numDoorHallway] |
---|
Intention | : | Each object represents one door of a room to the hallway. |
Timed Function | tempRadSet THREE_PT_ACT_RANGE |
---|
Intention | : | This function represents the current setting of the radiators in a room intended by the temperature control. |
Scope | : | mh |
Postreferences | : | msref Room : M_R2 |
msref Room : M_R3 |
Timed Function | tempRadNoMalSet : TEMP THREE_PT_ACT_RANGE |
---|
Intention | : | This function represents the current setting of the radiators in a room intended by the temperature control if the machine assumes that there is no malfunction of the sensors needed to determine this setting. This setting depends (at least) on the current desired room temperature (first argument). |
Scope | : | mh |
Postreferences | : | msref Room : M_R2 |
Timed Function | tempRadMalSet : TEMP THREE_PT_ACT_RANGE |
---|
Intention | : | This function represents the current setting of the radiators in a room intended by the temperature control if the machine assumes that there is a malfunction of the sensors needed to determine this setting. This setting depends (at least) on the current desired room temperature (first argument). Further arguments can be the current outdoor temperature and the settings of the neighbour rooms. |
Scope | : | mh |
Postreferences | : | msref Room : M_R2 |
Timed Predicate | malTemp |
---|
Intention | : | This predicate is true iff the machine assumes that the sensors, used to determine the settings of the actuators controlling the temperature, have such a serious malfunction that the settings of the actuators have to be determined using makeshift operations. |
Scope | : | mh |
Postreferences | : | msref Room : I_R1 |
msref Room : M_R1 | ||
msref Room : M_R2 | ||
msref BlindedRoom : M_BR2 |
Property | R_R1 |
---|
NonFormal | : | The desired temperature shall be reached as fast as possible during the heating up state.
This requirement is a basis for the definition of the functions tempRadNoMalSet and tempRadMalSet. |
Property | R_R2 |
---|
NonFormal | : | The currently desired temperature is maintained during the current temperature state as good as possible.
This requirement is a basis for the definition of the functions tempRadNoMalSet and tempRadMalSet. |
MACHINE SPECIFICATIONS
Property | I_R1 |
---|
Formal | : | malTemp |
NL | : | Initially the machine does not assume that the sensors, used to determine the settings of the actuators controlling the temperature, have such a serious malfunction that the settings of the actuators have to be determined using makeshift operations. |
Property | M_R1 |
---|
Formal | : | ( malTemp malfunctionAllTempSens ) |
NL | : | The machine assumes that the sensors, used to determine the settings of the actuators controlling the temperature, have such a serious malfunction that the settings of the actuators have to be determined using makeshift operations iff all temperature sensors of a room have a malfunction. |
Property | M_R2 |
---|
Formal | : | ( ( malTemp
tempRadSet = tempRadNoMalSet( RT. modes. roomDesiredTemperature) ) ( malTemp tempRadSet = tempRadMalSet( RT. modes. roomDesiredTemperature) ) ) |
NL | : | If the machine does not assume a serious malfunction of the sensors, used to determine the settings of the actuators controlling the temperature, the current setting of the radiators in a room intended by the temperature control are as determined by the function tempRadNoMalSet.
If the machine assumes a serious malfunction of the sensors, used to determine the settings of the actuators controlling the temperature, the current setting of the radiators in a room intended by the temperature control are as determined by the function tempRadMalSet. |
Property | M_R3 |
---|
Formal | : | ( n NAT ( numRad ) :
rad[n]. valveAct. noMalAct. adjustedEntity = tempRadSet ) |
NL | : | The value adjusted by the machine for the radiator valves corresponds with the value intended by the temperature control for these actuators depending on the currently desired temperature.
Note that all radiator valves in a room are always set to the same value. A specific value for a single radiator is not determined. |