next up previous contents index FOREST_HomepageFOREST_Example_Homepage
Next: Index Up: No Title Previous: Description Class StairCase

   
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

SIGNATURE

Object  o415  :  Office(numDoorHallway  = 1)
Intention : This object represents the office with room number 415. This office is equipped with
  • one door to the hallway
Postreferences : lsref Floor : ROOMS

Object  o417  :  Office(numDoorHallway  = 1)
Intention : This object represents the office with room number 417. This office is equipped with
  • one door to the hallway
Postreferences : lsref Floor : ROOMS

Object  o419  :  Office(numDoorHallway  = 1)
Intention : This object represents the office with room number 419. This office is equipped with
  • one door to the hallway
Postreferences : lsref Floor : ROOMS

Object  o429  :  Office(numDoorHallway  = 1)
Intention : This object represents the office with room number 429. This office is equipped with
  • one door to the hallway
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
  • one door to the hallway
  • one door to a neighbour room
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
  • one door to the hallway
  • one door to a neighbour room
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
  • one door to the hallway
  • one door to a neighbour room
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
  • one door to the hallway
  • two doors to neighbour rooms
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
  • one door to the hallway
  • two doors to neighbour rooms
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
  • one door to the hallway
  • one door to a neighbour room
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
  • one door to the hallway
Postreferences : lsref Floor : ROOMS

Object  cl411  :  NoOffice(numDoorHallway  = 2)
Intention : This object represents the computer lab with room number 411. It is equipped with
  • two doors to the hallway
Postreferences : lsref Floor : ROOMS

Object  cl426  :  NoOffice(numDoorHallway  = 1)
Intention : This object represents the computer lab with room number 426. It is equipped with
  • one door to the hallway
Postreferences : lsref Floor : ROOMS

Object  o424  :  Office(numDoorHallway  = 1)
Intention : This object represents the office with room number 424. It is equipped with
  • one door to the hallway
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
  • one door to the hallway item one door to a neighbour room
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
  • one door to the hallway
  • two doors to neighbour rooms
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
  • one door to the hallway
  • two doors to neighbour rooms
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
  • one door to the hallway
  • one door to a neighbour rooms
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
  • one door to the hallway
Postreferences : lsref Floor : ROOMS

Object  cl410  :  NoOffice(numDoorHallway  = 3)
Intention : This object represents the computer lab with room number 410. It is equipped with
  • three doors to the hallway
Postreferences : lsref Floor : ROOMS

Object  h1  :  HallwaySection
Intention : This object represents the hallway in the east of floor 32/4.
Postreferences : lsref Floor : HALLWAYS
    dkref Floor : D_F7

Object  h2  :  HallwaySection
Intention : This object represents the hallway in the middle of floor 32/4.
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.
Postreferences : lsref Floor : HALLWAYS
    dkref Floor : D_F8

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  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 : msref Floor : M_F2

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
    rsref Floor : R_F1
    msref Floor : M_F2
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.

Property  D_F7 
Formal : (  h1. westDoor =  h2. eastDoor )
NL : The eastern and middle hallway section are connected by a door.

Property  D_F8 
Formal : (  h2. westDoor =  h3. eastDoor )
NL : The middle and western hallway section 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 : If a malfunction occurs, the control system supports the facility manager by finding the reason.

Property  R_F3 
NonFormal : The system provides reports on current and past energy consumption.

Property  R_F4 
NonFormal : All malfunctions and unusual conditions are stored and reported on request.

Property  R_F5 
NonFormal : All hardware connections have to be made according to DIN standards.

Property  R_F6 
NonFormal : No hazardous condition for persons, inventory or building are allowed.

Property  R_F7 
NonFormal : The system issues warnings on unreasonable inputs.

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.

next up previous contents index FOREST_HomepageFOREST_Example_Homepage
Next: Index Up: No Title Previous: Description Class StairCase
Forest-System
1999-06-10