INTENTION
This class provides all definitions specific to all offices which are connected by at least one door to a neighbor room. Therefore, in addition to the definitions of the description class Office the definitions of the description class NeighborRoomConnections are inherited.
| Postreferences | : | lsref Floor : o435 |
| lsref Floor : o433 | ||
| lsref Floor : o431 | ||
| lsref Floor : o425 | ||
| lsref Floor : o423 | ||
| lsref Floor : o421 | ||
| lsref Floor : o416 | ||
| lsref Floor : o414 |
FORMAL PARAMETERS
| Function | numDoorHallway  NAT |
|---|
| Intention | : | This parameter represents the number of doors of a room to a hallway section. |
| Postreferences | : | lsref OfficeNeighbor : Office |
| Function | numDoorNeighbor NAT |
|---|
| Intention | : | This function represents the number of doors of a room to neighbor rooms. |
| Postreferences | : | lsref OfficeNeighbor : NeighborRoomConnections |
| msref OfficeNeighbor : M_ON1 |
BASE CLASSES
| Class | Office(numDoorHallway = numDoorHallway) |
|---|
Intention |
: | All definitions of description class Office are inherited. |
| Class | NeighborRoomConnections(numDoorNeighbor = numDoorNeighbor) |
|---|
Intention |
: | All definitions of description class NeighborRoomConnections are inherited. |
MACHINE SPECIFICATIONS
| Property | M_ON1 |
|---|
| Formal | : |  ( closedDoorContactNeighborMal 
 n  NAT ( numDoorNeighbor ) :
neighborDoor[n]. doorClosedContact. malSens. malDetMach ) |
| NL | : | A door closed contact of a door to a neighbor room has a malfunction if and only if at least one of these contacts has a malfunction. |