INTENTION
This class is the main class. It contains and combines all the objects belonging to the considered system. These objects are
SIGNATURE
Object | o415 : Office(numDoorHallway = 1) |
---|
Intention | : | This object represents the office with room number 415. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | o417 : Office(numDoorHallway = 1) |
---|
Intention | : | This object represents the office with room number 417. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | o419 : Office(numDoorHallway = 1) |
---|
Intention | : | This object represents the office with room number 419. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | o429 : Office(numDoorHallway = 1) |
---|
Intention | : | This object represents the office with room number 429. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | o425 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 1) |
---|
Intention | : | This object represents the office with room number 425. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F3 |
lsref Floor : ROOMS |
Object | o431 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 1) |
---|
Intention | : | This object represents the office with room number 431. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F2 |
lsref Floor : ROOMS |
Object | o435 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 1) |
---|
Intention | : | This object represents the office with room number 435. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F1 |
lsref Floor : ROOMS |
Object | o423 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 2) |
---|
Intention | : | This object represents the office with room number 423. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F3 |
dkref Floor : D_F4 | ||
lsref Floor : ROOMS |
Object | o433 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 2) |
---|
Intention | : | This object represents the office with room number 433. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F1 |
dkref Floor : D_F2 | ||
lsref Floor : ROOMS |
Object | o421 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 1) |
---|
Intention | : | This object represents the office with room number 421. This office is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F4 |
lsref Floor : ROOMS |
Object | m427 : NoOffice(numDoorHallway = 1) |
---|
Intention | : | This object represents the meeting room with room number 427. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | cl411 : NoOffice(numDoorHallway = 2) |
---|
Intention | : | This object represents the computer lab with room number 411. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | cl426 : NoOffice(numDoorHallway = 1) |
---|
Intention | : | This object represents the computer lab with room number 426. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | o424 : Office(numDoorHallway = 1) |
---|
Intention | : | This object represents the office with room number 424. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | cl422 : NoOfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 1) |
---|
Intention | : | This object represents the computer lab with room number 424. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | cl418 : NoOfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 2) |
---|
Intention | : | This object represents the computer lab with room number 418. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F5 |
lsref Floor : ROOMS |
Object | o416 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 2) |
---|
Intention | : | This object represents the office with room number 416. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F5 |
dkref Floor : D_F6 | ||
lsref Floor : ROOMS |
Object | o414 : OfficeNeighb(numDoorHallway = 1, numDoorNeighbour = 1) |
---|
Intention | : | This object represents the office with room number 414. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | dkref Floor : D_F6 |
lsref Floor : ROOMS |
Object | o412 : Office(numDoorHallway = 1) |
---|
Intention | : | This object represents the office with room number 412. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | cl410 : NoOffice(numDoorHallway = 3) |
---|
Intention | : | This object represents the computer lab with room number 410. It is equipped with
|
Prereferences | : | akref Floorplan |
Postreferences | : | lsref Floor : ROOMS |
Object | h1 : HallwaySection |
---|
Intention | : | This object represents the hallway in the east of floor 32/4. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | lsref Floor : HALLWAYS |
dkref Floor : D_F7 |
Object | h2 : HallwaySection |
---|
Intention | : | This object represents the hallway in the middle of floor 32/4. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | lsref Floor : HALLWAYS |
dkref Floor : D_F7 | ||
dkref Floor : D_F8 |
Object | h3 : HallwaySection |
---|
Intention | : | This object represents the hallway in the west of floor 32/4. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | lsref Floor : HALLWAYS |
dkref Floor : D_F8 |
Object | ols1 : OutdoorLightSensor |
---|
Intention | : | This object represents the outdoor light sensor in the north-east direction. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | msref Floor : M_F1 |
Object | ols2 : OutdoorLightSensor |
---|
Intention | : | This object represents the outdoor light sensor in the south-west direction. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | msref Floor : M_F1 |
Object | ols3 : OutdoorLightSensor |
---|
Intention | : | This object represents the outdoor light sensor in the north-west direction. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | msref Floor : M_F1 |
Object | ols4 : OutdoorLightSensor |
---|
Intention | : | This object represents the outdoor light sensor in the south-east direction. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | msref Floor : M_F1 |
Object | ols5 : OutdoorLightSensor |
---|
Intention | : | This object represents the outdoor light sensor in the north direction. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | msref Floor : M_F1 |
Object | ols6 : OutdoorLightSensor |
---|
Intention | : | This object represents the outdoor light sensor in the south direction. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | msref Floor : M_F1 |
Object | scw : StairCase |
---|
Intention | : | This object represents the staircase in the west of floor 32/4. |
Prereferences | : | akref Floorplan |
akref BD_20 |
Object | sce : StairCase |
---|
Intention | : | This object represents the staircase in the east of floor 32/4. |
Prereferences | : | akref Floorplan |
akref BD_20 |
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. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
Postreferences | : | msref Floor : M_F2 |
Domain | HALLWAYS = { h1, h2, h3 } HallwaySection |
---|
Intention | : | This domain contains all the hallway sections that have to be considered. |
Prereferences | : | akref Floorplan |
akref BD_20 | ||
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 |
Prereferences | : | pdref NF3 |
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 |
Prereferences | : | pdref NF1 |
pdref NF2 | ||
pdref NF3 | ||
Postreferences | : | msref Floor : M_F1 |
rsref Floor : R_F1 | ||
msref Floor : M_F2 |
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. |
Prereferences | : | akref Floorplan |
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. |
Prereferences | : | akref Floorplan |
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. |
Prereferences | : | akref Floorplan |
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. |
Prereferences | : | akref Floorplan |
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. |
Prereferences | : | akref Floorplan |
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. |
Prereferences | : | akref Floorplan |
Property | D_F7 |
---|
Formal | : | ( h1. westDoor = h2. eastDoor ) |
NL | : | The eastern and middle hallway section are connected by a door. |
Prereferences | : | akref Floorplan |
Property | D_F8 |
---|
Formal | : | ( h2. westDoor = h3. eastDoor ) |
NL | : | The middle and western hallway section are connected by a door. |
Prereferences | : | akref Floorplan |
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 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. |
Prereferences | : | pdref NF3 |
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 |
Property | R_F7 |
---|
NonFormal | : | The system issues warnings on unreasonable inputs. |
Prereferences | : | pdref NF9 |
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. |
Prereferences | : | pdref NF2 |