INTENTION
This class is the main class. It contains and combines all the objects belonging to the considered system. These objects are
SIGNATURE
| Object | o435 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 1) |
|---|
| Intention | : | This object represents the office with room number 435, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F1 |
| lsref Floor : ROOMS | ||
| msref Floor : M_F6 |
| Object | o433 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 2) |
|---|
| Intention | : | This object represents the office with room number 433, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F1 |
| dkref Floor : D_F2 | ||
| lsref Floor : ROOMS | ||
| msref Floor : M_F7 |
| Object | o431 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 1) |
|---|
| Intention | : | This object represents the office with room number 431, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F2 |
| lsref Floor : ROOMS | ||
| msref Floor : M_F8 |
| Object | o429 : OfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the office with room number 429, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F9 |
| Object | m427 : NoOfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the meeting room with room number 427,
which is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F10 |
| Object | o425 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 1) |
|---|
| Intention | : | This object represents the office with room number 425, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F3 |
| lsref Floor : ROOMS | ||
| msref Floor : M_F11 |
| Object | o423 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 2) |
|---|
| Intention | : | This object represents the office with room number 423, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F3 |
| dkref Floor : D_F4 | ||
| lsref Floor : ROOMS | ||
| msref Floor : M_F12 |
| Object | o421 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 1) |
|---|
| Intention | : | This object represents the office with room number 421, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F4 |
| lsref Floor : ROOMS | ||
| msref Floor : M_F13 |
| Object | o419 : OfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the office with room number 419, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F14 |
| Object | o417 : OfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the office with room number 417, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F15 |
| Object | o415 : OfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the office with room number 415, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F16 |
| Object | hl411 : NoOfficeWithoutNeighbor(numDoorHallway = 2) |
|---|
| Intention | : | This object represents the hardware lab with room number 411,
which is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F17 |
| Object | cl426 : NoOfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the computer lab with room number 426,
which is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F18 |
| Object | o424 : OfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the office with room number 424, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F19 |
| Object | cl422 : NoOfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 1) |
|---|
| Intention | : | This object represents the computer lab with room number 424,
which is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F20 |
| Object | cl418 : NoOfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 2) |
|---|
| Intention | : | This object represents the computer lab with room number 418,
which is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F5 |
| lsref Floor : ROOMS | ||
| msref Floor : M_F21 |
| Object | o416 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 2) |
|---|
| Intention | : | This object represents the office with room number 416, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F5 |
| dkref Floor : D_F6 | ||
| lsref Floor : ROOMS | ||
| msref Floor : M_F22 |
| Object | o414 : OfficeNeighbor(numDoorHallway = 1, numDoorNeighbor = 1) |
|---|
| Intention | : | This object represents the office with room number 414, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | dkref Floor : D_F6 |
| lsref Floor : ROOMS | ||
| msref Floor : M_F23 |
| Object | o412 : OfficeWithoutNeighbor(numDoorHallway = 1) |
|---|
| Intention | : | This object represents the office with room number 412, which
is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F24 |
| Object | hl410 : NoOfficeWithoutNeighbor(numDoorHallway = 3) |
|---|
| Intention | : | This object represents the hardware lab with room number 410,
which is equipped with
|
| Prereferences | : | akref Figure1 |
| Postreferences | : | lsref Floor : ROOMS |
| msref Floor : M_F25 |
| Object | h1 : HallwaySection(numPB = 3) |
|---|
| NL | : | hallway 1 |
| Intention | : | This object represents the hallway in the east of floor 32/4. There are three push buttons for controlling the ceiling light group in this hallway section. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | lsref Floor : HALLWAYS |
| dkref Floor : D_F7 |
| Object | h2 : HallwaySection(numPB = 3) |
|---|
| NL | : | hallway 2 |
| Intention | : | This object represents the hallway in the middle of floor 32/4. There are three push buttons for controlling the ceiling light group in this hallway section. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | lsref Floor : HALLWAYS |
| dkref Floor : D_F7 | ||
| dkref Floor : D_F8 |
| Object | h3 : HallwaySection(numPB = 3) |
|---|
| NL | : | hallway 3 |
| Intention | : | This object represents the hallway in the west of floor 32/4. There are three push buttons for controlling the ceiling light group in this hallway section. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | lsref Floor : HALLWAYS |
| dkref Floor : D_F8 |
| Object | ols1 : OutdoorLightSensor |
|---|
| NL | : | outdoor light sensor 1 |
| Intention | : | This object represents the outdoor light sensor in the north-east direction. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F1 |
| msref Floor : M_F6 | ||
| msref Floor : M_F7 | ||
| msref Floor : M_F8 | ||
| msref Floor : M_F9 | ||
| msref Floor : M_F10 |
| Object | ols2 : OutdoorLightSensor |
|---|
| NL | : | outdoor light sensor 2 |
| Intention | : | This object represents the outdoor light sensor in the south-west direction. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F1 |
| msref Floor : M_F18 | ||
| msref Floor : M_F19 | ||
| msref Floor : M_F20 |
| Object | ols3 : OutdoorLightSensor |
|---|
| NL | : | outdoor light sensor 3 |
| Intention | : | This object represents the outdoor light sensor in the north-west direction. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F1 |
| msref Floor : M_F20 | ||
| msref Floor : M_F13 | ||
| msref Floor : M_F14 | ||
| msref Floor : M_F15 | ||
| msref Floor : M_F16 |
| Object | ols4 : OutdoorLightSensor |
|---|
| NL | : | outdoor light sensor 4 |
| Intention | : | This object represents the outdoor light sensor in the south-east direction. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F1 |
| msref Floor : M_F21 | ||
| msref Floor : M_F22 | ||
| msref Floor : M_F23 | ||
| msref Floor : M_F24 |
| Object | ols5 : OutdoorLightSensor |
|---|
| NL | : | outdoor light sensor 5 |
| Intention | : | This object represents the outdoor light sensor in the north direction. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F1 |
| msref Floor : M_F17 | ||
| msref Floor : M_F10 | ||
| msref Floor : M_F11 | ||
| msref Floor : M_F12 | ||
| msref Floor : M_F13 |
| Object | ols6 : OutdoorLightSensor |
|---|
| NL | : | outdoor light sensor 6 |
| Intention | : | This object represents the outdoor light sensor in the south direction. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F1 |
| msref Floor : M_F24 | ||
| msref Floor : M_F25 |
| Object | scw : Staircase |
|---|
| NL | : | western staircase |
| Intention | : | This object represents the staircase in the west of floor 32/4. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F4 |
| Object | sce : Staircase |
|---|
| NL | : | eastern staircase |
| Intention | : | This object represents the staircase in the east of floor 32/4. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F3 |
| Object | indicatorMalFctWestStaircase : InformSensActMalFct |
|---|
| Intention | : | This object represents the handling of a malfunction of the motion detector in the western staircase. |
| Postreferences | : | msref Floor : M_F4 |
| Object | indicatorMalFctEastStaircase : InformSensActMalFct |
|---|
| Intention | : | This object represents the handling of a malfunction of the motion detector in the eastern staircase. |
| Postreferences | : | msref Floor : M_F3 |
| Domain | ROOMS = { o435, o433, o431, o429, o425, o423, o421, o419, o417, o415, o424, o416, o414, o412, m427, hl411, cl426, cl422, cl418, hl410 }  Room |
|---|
| Intention | : | This domain contains all rooms of the specified floor. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | msref Floor : M_F2 |
| msref Floor : M_F5 |
| Domain | HALLWAYS = { h1, h2, h3 } HallwaySection(numPB = 3) |
|---|
| Intention | : | This domain contains all the hallway sections that have to be considered. |
| Prereferences | : | akref Figure1 |
| akref BD_6 | ||
| Postreferences | : | rsref Floor : R_F1 |
| msref Floor : M_F5 |
| Time Constant | TmalReact |
|---|
| Intention | : | The time delay between a malfunction of the outdoor light sensor and switching on the lights if a hallway section is occupied. |
| Scope | : | ev |
| Prereferences | : | pdref NF3 |
| Postreferences | : | rsref Floor : R_F1 |
| Timed Predicate | outLightSensorFaultMach |
|---|
| Intention | : | This predicate is true if and only if the machine assumes that some outdoor light sensors have a malfunction. |
| Scope | : | mh |
| Prereferences | : | pdref NF1 |
| pdref NF2 | ||
| pdref NF3 | ||
| Postreferences | : | msref Floor : M_F1 |
| rsref Floor : R_F1 |
| Property | D_F1 |
|---|
| Formal | : |  ( o435. neighborDoor[1] = o433. neighborDoor[1] ) |
| NL | : | The two rooms with room numbers 435 and 433 are connected by a door. |
| Prereferences | : | akref Figure1 |
| Property | D_F2 |
|---|
| Formal | : | ( o433. neighborDoor[2] = o431. neighborDoor[1] ) |
| NL | : | The two rooms with room numbers 433 and 431 are connected by a door. |
| Prereferences | : | akref Figure1 |
| Property | D_F3 |
|---|
| Formal | : | ( o425. neighborDoor[1] = o423. neighborDoor[1] ) |
| NL | : | The two rooms with room numbers 425 and 423 are connected by a door. |
| Prereferences | : | akref Figure1 |
| Property | D_F4 |
|---|
| Formal | : | ( o423. neighborDoor[2] = o421. neighborDoor[1] ) |
| NL | : | The two rooms with room numbers 423 and 421 are connected by a door. |
| Prereferences | : | akref Figure1 |
| Property | D_F5 |
|---|
| Formal | : | ( cl418. neighborDoor[2] = o416. neighborDoor[1] ) |
| NL | : | The two rooms with room numbers 418 and 416 are connected by a door. |
| Prereferences | : | akref Figure1 |
| Property | D_F6 |
|---|
| Formal | : | ( o416. neighborDoor[1] = o414. neighborDoor[1] ) |
| NL | : | The two rooms with room numbers 416 and 414 are connected by a door. |
| Prereferences | : | akref Figure1 |
| Property | D_F7 |
|---|
| Formal | : | ( h1. westDoor = h2. eastDoor ) |
| NL | : | The eastern and middle hallway section are connected by a door. |
| Prereferences | : | akref Figure1 |
| Property | D_F8 |
|---|
| Formal | : | ( h2. westDoor = h3. eastDoor ) |
| NL | : | The middle and western hallway section are connected by a door. |
| Prereferences | : | akref Figure1 |
REQUIREMENT SPECIFICATIONS
| Property | R_F1 |
|---|
| Formal | : | (  h  HALLWAYS:
( outLightSensorFaultMach  h. occFM. occUsed
  TmalReact h. light[1]. sl. noMalSens. envEntity = 1 ) ) |
| NL | : | Whenever some outdoor light sensors are not working correctly and the hallway is occupied for at least TmalReact 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 | : | If a malfunction occurs, the control system supports the facility manager by finding the reason. |
| Prereferences | : | pdref FM8 |
| Property | R_F3 |
|---|
| NonFormal | : | The system provides reports on current and past energy consumption. |
| Prereferences | : | pdref FM9 |
| Property | R_F4 |
|---|
| NonFormal | : | All malfunctions and unusual conditions are stored and reported on request. |
| Prereferences | : | pdref FM10 |
| Property | R_F5 |
|---|
| NonFormal | : | All hardware connections have to be made according to DIN standards. |
| Prereferences | : | pdref NF6 |
| Property | R_F6 |
|---|
| NonFormal | : | No hazardous condition for persons, inventory or building are allowed. |
| Prereferences | : | pdref NF7 |
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 if and only if one of the six outdoor light sensors has a malfunction. |
| Property | M_F2 |
|---|
| Formal | : | ( r ROOMS: ( r. OLSMalFct 
r. curDefaultLightScene = r. malDefaultLightScene ) ) |
| NL | : | Whenever the machine assumes that some outdoor light sensor used by a room is not working correctly, then the default light scene is the default fault light scene, i.e., all ceiling lights are on. |
| Prereferences | : | pdref NF2 |
| Property | M_F3 |
|---|
| Formal | : | ( indicatorMalFctEastStaircase. informCondMach
sce. md. malSens. malDetMach ) |
| NL | : | The situation the facility manager should be informed about concerning the motion detector in the eastern staircase is given if and only if this motion detector has a malfunction. |
| Property | M_F4 |
|---|
| Formal | : | ( indicatorMalFctWestStaircase. informCondMach
scw. md. malSens. malDetMach ) |
| NL | : | The situation the facility manager should be informed about concerning the motion detector in the western staircase is given if and only if this motion detector has a malfunction. |
| Property | M_F5 |
|---|
| Formal | : | ( r1 ROOMS: r2 ROOMS: h1 HALLWAYS: h2 HALLWAYS:
( r1. CPFM. indicatorUnreasonInp. indicator = r2. CPFM. indicatorUnreasonInp. indicator
r1. CPFM. indicatorUnreasonInp. indicator = h1. CPFM. indicatorUnreasonInp. indicator
h1. CPFM. indicatorUnreasonInp. indicator = h2. CPFM. indicatorUnreasonInp. indicator ) ) |
| NL | : | The indicator light of the facility manager control panel concerning an unreasonable input is the same for all rooms and all hallways.
Note that nevertheless the conditions for this indicator light differ from area to area. |
| Property | M_F6 |
|---|
| Formal | : | ( o435. OLSMalFct ols1. malSens. malDetMach ) |
| NL | : | Room o435 uses the following outdoor light sensors:
|
| Property | M_F7 |
|---|
| Formal | : | ( o433. OLSMalFct ols1. malSens. malDetMach ) |
| NL | : | Room o433 uses the following outdoor light sensors:
|
| Property | M_F8 |
|---|
| Formal | : | ( o431. OLSMalFct ols1. malSens. malDetMach ) |
| NL | : | Room o431 uses the following outdoor light sensors:
|
| Property | M_F9 |
|---|
| Formal | : | ( o429. OLSMalFct ols1. malSens. malDetMach ) |
| NL | : | Room o429 uses the following outdoor light sensors:
|
| Property | M_F10 |
|---|
| Formal | : | ( m427. OLSMalFct ols1. malSens. malDetMach
ols5. malSens. malDetMach ) |
| NL | : | Room m427 uses the following outdoor light sensors:
|
| Property | M_F11 |
|---|
| Formal | : | ( o425. OLSMalFct ols5. malSens. malDetMach ) |
| NL | : | Room o427 uses the following outdoor light sensors:
|
| Property | M_F12 |
|---|
| Formal | : | ( o423. OLSMalFct ols5. malSens. malDetMach ) |
| NL | : | Room o423 uses the following outdoor light sensors:
|
| Property | M_F13 |
|---|
| Formal | : | ( o421. OLSMalFct ols3. malSens. malDetMach
ols5. malSens. malDetMach ) |
| NL | : | Room o421 uses the following outdoor light sensors:
|
| Property | M_F14 |
|---|
| Formal | : | ( o419. OLSMalFct ols3. malSens. malDetMach ) |
| NL | : | Room o419 uses the following outdoor light sensors:
|
| Property | M_F15 |
|---|
| Formal | : | ( o417. OLSMalFct ols3. malSens. malDetMach ) |
| NL | : | Room o417 uses the following outdoor light sensors:
|
| Property | M_F16 |
|---|
| Formal | : | ( o415. OLSMalFct ols3. malSens. malDetMach ) |
| NL | : | Room o415 uses the following outdoor light sensors:
|
| Property | M_F17 |
|---|
| Formal | : | ( hl411. OLSMalFct ols5. malSens. malDetMach ) |
| NL | : | Room cl411 uses the following outdoor light sensors:
|
| Property | M_F18 |
|---|
| Formal | : | ( cl426. OLSMalFct ols2. malSens. malDetMach ) |
| NL | : | Room cl426 uses the following outdoor light sensors:
|
| Property | M_F19 |
|---|
| Formal | : | ( o424. OLSMalFct ols2. malSens. malDetMach ) |
| NL | : | Room o424 uses the following outdoor light sensors:
|
| Property | M_F20 |
|---|
| Formal | : | ( cl422. OLSMalFct ols2. malSens. malDetMach
ols3. malSens. malDetMach ) |
| NL | : | Room cl422 uses the following outdoor light sensors:
|
| Property | M_F21 |
|---|
| Formal | : | ( cl418. OLSMalFct ols4. malSens. malDetMach ) |
| NL | : | Room cl418 uses the following outdoor light sensors:
|
| Property | M_F22 |
|---|
| Formal | : | ( o416. OLSMalFct ols4. malSens. malDetMach ) |
| NL | : | Room o416 uses the following outdoor light sensors:
|
| Property | M_F23 |
|---|
| Formal | : | ( o414. OLSMalFct ols4. malSens. malDetMach ) |
| NL | : | Room o414 uses the following outdoor light sensors:
|
| Property | M_F24 |
|---|
| Formal | : | ( o412. OLSMalFct ols4. malSens. malDetMach
ols6. malSens. malDetMach ) |
| NL | : | Room o412 uses the following outdoor light sensors:
|
| Property | M_F25 |
|---|
| Formal | : | ( hl410. OLSMalFct ols6. malSens. malDetMach ) |
| NL | : | Room cl410 uses the following outdoor light sensors:
|