Description Class Floor

INTENTION

This class is the main class. It contains and combines all the objects belonging to the considered system. These objects are

• the rooms of the floor
• the hallway sections of the floor
• the parts of the staircases belonging to the floor
• the outdoor light sensors
• the outdoor temperature sensor

SIGNATURE

Object	o415  :  Office(numRad  = 2, numDoorHallway  = 1)

Intention	:	This object represents the office with room number 415. This office is equipped with two radiators one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES

Object	o417  :  Office(numRad  = 2, numDoorHallway  = 1)

Intention	:	This object represents the office with room number 417. This office is equipped with two radiators one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES

Object	o419  :  Office(numRad  = 2, numDoorHallway  = 1)

Intention	:	This object represents the office with room number 419. This office is equipped with two radiators one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES

Object	o429  :  Office(numRad  = 2, numDoorHallway  = 1)

Intention	:	This object represents the office with room number 429. This office is equipped with two radiators one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES

Object	o425  :  OfficeNeighb(numRad  = 2, numDoorHallway  = 1, numDoorNeighbour  = 1)

Intention	:	This object represents the office with room number 425. This office is equipped with two radiators one door to the hallway one door to a neighbour room
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F3

Object	o431  :  OfficeNeighb(numRad  = 2, numDoorHallway  = 1, numDoorNeighbour  = 1)

Intention	:	This object represents the office with room number 431. This office is equipped with two radiators one door to the hallway one door to a neighbour room
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F2

Object	o435  :  OfficeNeighb(numRad  = 2, numDoorHallway  = 1, numDoorNeighbour  = 1)

Intention	:	This object represents the office with room number 435. This office is equipped with two radiators one door to the hallway one door to a neighbour room
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F1

Object	o423  :  OfficeNeighb(numRad  = 2, numDoorHallway  = 1, numDoorNeighbour  = 2)

Intention	:	This object represents the office with room number 423. This office is equipped with two radiators one door to the hallway two doors to neighbour rooms
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F3
		dkref Floor : D_F4

Object	o433  :  OfficeNeighb(numRad  = 2, numDoorHallway  = 1, numDoorNeighbour  = 2)

Intention	:	This object represents the office with room number 433. This office is equipped with two radiators one door to the hallway two doors to neighbour rooms
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F1
		dkref Floor : D_F2

Object	o421  :  OfficeNeighb(numRad  = 3, numDoorHallway  = 1, numDoorNeighbour  = 1)

Intention	:	This object represents the office with room number 421. This office is equipped with three radiators one door to the hallway one door to a neighbour room
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F4

Object	m427  :  NoOffice(numRad  = 5, numDoorHallway  = 1)

Intention	:	This object represents the meeting room with room number 427. It is equipped with five radiators one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : MEETING_ROOMS

Object	cl411  :  NoOffice(numRad  = 9, numDoorHallway  = 2)

Intention	:	This object represents the computer lab with room number 411. It is equipped with nine radiators two doors to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : COMPUTER_LABS

Object	cl426  :  BlindedNoOffice(numRad  = 3, numSunBlinds  = 3, numDoorHallway  = 1)

Intention	:	This object represents the computer lab with room number 426. It is equipped with three radiators three sun blinds one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : COMPUTER_LABS

Object	o424  :  BlindedOffice(numRad  = 2, numSunBlinds  = 2, numDoorHallway  = 1)

Intention	:	This object represents the office with room number 424. It is equipped with two radiators two sun blinds one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES

Object	cl422  :  BlindedNoOfficeNeighb(numRad  = 3, numSunBlinds  = 3, numDoorHallway  = 1, numDoorNeighbour  = 1)

Intention	:	This object represents the computer lab with room number 424. It is equipped with three radiators three sun blinds one door to the hallway one door to a neighbour room
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : COMPUTER_LABS

Object	cl418  :  BlindedNoOfficeNeighb(numRad  = 2, numSunBlinds  = 2, numDoorHallway  = 1, numDoorNeighbour  = 2)

Intention	:	This object represents the computer lab with room number 418. It is equipped with two radiators two sun blinds one door to the hallway two doors to neighbour rooms
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : COMPUTER_LABS
		dkref Floor : D_F5

Object	o416  :  BlindedOfficeNeighb(numRad  = 2, numSunBlinds  = 2, numDoorHallway  = 1, numDoorNeighbour  = 2)

Intention	:	This object represents the office with room number 416. It is equipped with two radiators two sun blinds one door to the hallway two doors to neighbour rooms
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F5
		dkref Floor : D_F6

Object	o414  :  BlindedOfficeNeighb(numRad  = 2, numSunBlinds  = 2, numDoorHallway  = 1, numDoorNeighbour  = 1)

Intention	:	This object represents the office with room number 414. It is equipped with two radiators two sun blinds one door to the hallway one door to a neighbour rooms
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES
		dkref Floor : D_F6

Object	o412  :  BlindedOffice(numRad  = 3, numSunBlinds  = 3, numDoorHallway  = 1)

Intention	:	This object represents the office with room number 412. It is equipped with three radiators three sun blinds one door to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : OFFICES

Object	cl410  :  BlindedNoOffice(numRad  = 10, numSunBlinds  = 10, numDoorHallway  = 3)

Intention	:	This object represents the computer lab with room number 410. It is equipped with ten radiators ten sun blinds three doors to the hallway
Postreferences	:	lsref Floor : ROOMS
		lsref Floor : COMPUTER_LABS

Object	h1  :  HallwaySection

Intention	:	This object represents the hallway in the east of floor 32/4.
Postreferences	:	lsref Floor : HALLWAYS

Object	h2  :  HallwaySection

Intention	:	This object represents the hallway in the middle of floor 32/4.
Postreferences	:	lsref Floor : HALLWAYS

Object	h3  :  HallwaySection

Intention	:	This object represents the hallway in the west of floor 32/4.
Postreferences	:	lsref Floor : HALLWAYS

Object	ols1  :  OutdoorLightSensor

Intention	:	This object represents the outdoor light sensor in the north-east direction.
Postreferences	:	msref Floor : M_F1

Object	ols2  :  OutdoorLightSensor

Intention	:	This object represents the outdoor light sensor in the south-west direction.
Postreferences	:	msref Floor : M_F1

Object	ols3  :  OutdoorLightSensor

Intention	:	This object represents the outdoor light sensor in the north-west direction.
Postreferences	:	msref Floor : M_F1

Object	ols4  :  OutdoorLightSensor

Intention	:	This object represents the outdoor light sensor in the south-east direction.
Postreferences	:	msref Floor : M_F1

Object	ols5  :  OutdoorLightSensor

Intention	:	This object represents the outdoor light sensor in the north direction.
Postreferences	:	msref Floor : M_F1

Object	ols6  :  OutdoorLightSensor

Intention	:	This object represents the outdoor light sensor in the south direction.
Postreferences	:	msref Floor : M_F1

Object	ots  :  OutdoorTempSensor

Intention

:

This object represents the outdoor temperature sensor.

Object	scw  :  StairCase

Intention

:

This object represents the staircase in the west of floor 32/4.

Object	sce  :  StairCase

Intention

:

This object represents the staircase in the east of floor 32/4.

Domain	ROOMS  = {  o435,  o433,  o431,  o429,  o425,  o423,  o421,  o419,  o417,  o415,  o424,  o416,  o414,  o412,  m427,  cl411,  cl426,  cl422,  cl418,  cl410 }  BasicRoom

Intention	:	This domain contains all the rooms that have to be considered.
Postreferences	:	lsref Floor : OFFICES
		lsref Floor : MEETING_ROOMS
		lsref Floor : COMPUTER_LABS
		msref Floor : M_F2
		msref Floor : M_F3
		msref Floor : M_F4
		msref Floor : M_F5
		msref Floor : M_F6

Domain	OFFICES  = {  o435,  o433,  o431,  o429,  o425,  o423,  o421,  o419,  o417,  o415,  o424,  o416,  o414,  o412 }  ROOMS

Intention	:	This domain contains all the offices that have to be considered.
Postreferences	:	msref Floor : M_F7
		msref Floor : M_F8

Domain	MEETING_ROOMS  = {  m427 }  ROOMS

Intention	:	This domain contains all the meeting rooms that have to be considered.
Postreferences	:	msref Floor : M_F9
		msref Floor : M_F10

Domain	COMPUTER_LABS  = {  cl411,  cl426,  cl422,  cl418,  cl410 }  ROOMS

Intention	:	This domain contains all the rooms that have to be considered.
Postreferences	:	msref Floor : M_F11
		msref Floor : M_F12

Domain	HALLWAYS  = {  h1,  h2,  h3 }  HallwaySection

Intention	:	This domain contains all the hallway sections that have to be considered.
Postreferences	:	rsref Floor : R_F1

Time Constant	TmalReact

Intention	:	The time delay between a malfunction of the outdoor light sensor and switching on the lights if the hallway is occupied.
Scope	:	ev
Postreferences	:	rsref Floor : R_F1

Timed Predicate	outLightSensorFaultMach

Intention	:	This predicate is true iff the machine assumes that some outdoor light sensors have a malfunction.
Scope	:	mh
Postreferences	:	msref Floor : M_F1
		msref Floor : M_F2
		rsref Floor : R_F1

DOMAIN KNOWLEDGE

Property	D_F1

Formal	:	(  o435. neighbourDoor[1] =  o433. neighbourDoor[1] )
NL	:	The two rooms with room numbers 435 and 433 are connected by a door.

Property	D_F2

Formal	:	(  o433. neighbourDoor[2] =  o431. neighbourDoor[1] )
NL	:	The two rooms with room numbers 433 and 431 are connected by a door.

Property	D_F3

Formal	:	(  o425. neighbourDoor[1] =  o423. neighbourDoor[1] )
NL	:	The two rooms with room numbers 425 and 423 are connected by a door.

Property	D_F4

Formal	:	(  o423. neighbourDoor[2] =  o421. neighbourDoor[1] )
NL	:	The two rooms with room numbers 423 and 421 are connected by a door.

Property	D_F5

Formal	:	(  cl418. neighbourDoor[2] =  o416. neighbourDoor[1] )
NL	:	The two rooms with room numbers 418 and 416 are connected by a door.

Property	D_F6

Formal	:	(  o416. neighbourDoor[1] =  o414. neighbourDoor[1] )
NL	:	The two rooms with room numbers 416 and 414 are connected by a door.

REQUIREMENT SPECIFICATIONS

Property	R_F1

Formal	:	( h  HALLWAYS:            (  outLightSensorFaultMach h. occ. occUsed                       TmalReact h. light[1]. ls. noMalSens. envEntity = 1 ) )
NL	:	Whenever some outdoor light sensors are not working correctly and the hallway is occupied for at least $T_{\mathit{malReact}}$ time units, then eventually within this time span, the light in the hallway is on and remains on at least as long as the precondition is true.

Property	R_F2

NonFormal

:

Energy consumption should be reduced as far as possible during maintaining of comfortable working conditions for all users.

Property	R_F3

NonFormal

:

If a malfunction occurs, the control system supports the facility manager by finding the reason.

Property	R_F4

NonFormal

:

The system provides reports on current and past energy consumption.

Property	R_F5

NonFormal

:

All malfunctions and unusual conditions are stored and reported on request.

Property	R_F6

NonFormal

:

All hardware connections have to be made according to DIN standards.

Property	R_F7

NonFormal

:

No hazardous condition for persons, inventory or building are allowed.

Property	R_F8

NonFormal

:

The system warns about unreasonable inputs.

Property	R_F9

NonFormal

:

If the whole control system has a serious malfunction, complete manual operation should be possible.

Property	R_F10

NonFormal

:

The control system shall be designed such that it can be easily changed and expanded.

Property	R_F11

NonFormal

:

The control system provides basic energy saving procedures automatically for control comfort. If the facility manager deviates from such settings, the system provides a report on expected results.

MACHINE SPECIFICATIONS

Property	M_F1

Formal	:	(  outLightSensorFaultMach  ols1. malSens. malDetMach                                                            ols2. malSens. malDetMach                                                            ols3. malSens. malDetMach                                                            ols4. malSens. malDetMach                                                            ols5. malSens. malDetMach                                                            ols6. malSens. malDetMach )
NL	:	The machine assumes that some outdoor light sensor has a malfunction iff one of the six outdoor light sensors has a malfunction.

Property	M_F2

Formal	:	( r  ROOMS: (  outLightSensorFaultMach                 r. RL. curStandLightScene = r. RL. faultStandLightScene ) )
NL	:	Whenever the machine assumes that some outdoor light sensors are not working correctly, then the standard light scene is the standard fault light scene, i.e. all ceiling lights are on.

Property	M_F3

Formal	:	( r  ROOMS: ( s  ROOMS:            r. RT. cp. tCPFM. heatingPeriod =                                s. RT. cp. tCPFM. heatingPeriod ) )
NL	:	The heating period is the same for all rooms.

Property	M_F4

Formal	:	( r  ROOMS: ( s  ROOMS:            r. RT. cp. tCPFM. buildingNonFreezePeriod =                                s. RT. cp. tCPFM. buildingNonFreezePeriod ) )
NL	:	The period within which the non freeze mode is set for the whole building is the same for all rooms.

Property	M_F5

Formal	:	( r  ROOMS: ( s  ROOMS:            r. RT. cp. tCPFM. nonFreezeTemperature =                                s. RT. cp. tCPFM. nonFreezeTemperature ) )
NL	:	The temperature that should be applied if the operation mode NonFreezeMode is active is the same for all rooms.

Property	M_F6

Formal	:	( r  ROOMS: ( s  ROOMS:            r. RT. cp. tCPFM. adaptive =                                s. RT. cp. tCPFM. adaptive ) )
NL	:	The modus set by the facility manager indicating whether the delay times used for determining occupancy are adaptive or not is always the same for all rooms.

Property	M_F7

Formal	:	( r  OFFICES: ( s  OFFICES:            r. RT. cp. tCPFM. standbyTemperature =                                s. RT. cp. tCPFM. standbyTemperature ) )
NL	:	The temperature that should be applied in the standbyMode is the same for all offices.

Property	M_F8

Formal	:	( r  OFFICES: ( s  OFFICES:            r. RT. cp. tCPFM. offTemperature =                                s. RT. cp. tCPFM. offTemperature ) )
NL	:	The temperature that should be applied in the OffMode is the same for all offices.

Property	M_F9

Formal	:	( r  MEETING_ROOMS: ( s  MEETING_ROOMS:            r. RT. cp. tCPFM. standbyTemperature =                                s. RT. cp. tCPFM. standbyTemperature ) )
NL	:	The temperature that should be applied in the standbyMode is the same for all meeting rooms.

Property	M_F10

Formal	:	( r  MEETING_ROOMS: ( s  MEETING_ROOMS:            r. RT. cp. tCPFM. offTemperature =                                s. RT. cp. tCPFM. offTemperature ) )
NL	:	The temperature that should be applied in the OffMode is the same for all meeting rooms.

Property	M_F11

Formal	:	( r  COMPUTER_LABS: ( s  COMPUTER_LABS:            r. RT. cp. tCPFM. standbyTemperature =                                s. RT. cp. tCPFM. standbyTemperature ) )
NL	:	The temperature that should be applied in the standbyMode is the same for all computer labs.

Property	M_F12

Formal	:	( r  COMPUTER_LABS: ( s  COMPUTER_LABS:            r. RT. cp. tCPFM. offTemperature =                                s. RT. cp. tCPFM. offTemperature ) )
NL	:	The temperature that should be applied in the OffMode is the same for all computer labs.