models
Class DirectionRequestButtonsOnFloors

java.lang.Object
  extended by models.DirectionRequestButtonsOnFloors
All Implemented Interfaces:
HasInvariant

public class DirectionRequestButtonsOnFloors
extends java.lang.Object
implements HasInvariant

Tested by JUnit_DirectionRequestButtonsOnFloors and Validation_DirectionRequestButtonsOnFloors
For managing the state of the direction requests on all floors of an elevator (see ElevatorSpecification)

Version:
1
Author:
J Paul Gibson

Constructor Summary
DirectionRequestButtonsOnFloors(int numberOfFloors)
          Initialises all direction requests (up and down, on each floor) to be false
 
Method Summary
 void cancelDownRequest(int floor)
          Cancel the down request at the specified floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Down_presses_cancels()
 void cancelUpRequest(int floor)
          Cancel the up request at the specified floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()
 boolean downPressedAtFloor(int floor)
          Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()
 boolean invariant()
          The following safety conditions are required: number of floors must be at least 2 the number of up/down buttons is the same as the number of floors the down button on the bottom floor is disabled the up button on the top floor is disabled Tested by JUnit_DirectionRequestButtonsOnFloors.test_invariant()
 boolean noMoreRequestsAbove(int floor)
          Tested by JUnit_DirectionRequestButtonsOnFloors.test_noMoreRequestsAbove()
 boolean noMoreRequestsBelow(int floor)
          Tested by JUnit_DirectionRequestButtonsOnFloors.test_noMoreRequestsBelow()
 void pressDown(int floor)
          Update the down button request except if it is made on bottom floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Down_presses_cancels()
 void pressUp(int floor)
          Update the up button request except if it is made on top floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()
 java.lang.String toString()
          Typical string representation is of the form: Direction Requests For Elevator At Floor: 0- 1-UD 2- 3- 4- 5- 6- 7- 8- 9- In this example, there are 10 floors and up and down requests on the 1st floor
 boolean upPressedAtFloor(int floor)
          Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

DirectionRequestButtonsOnFloors

public DirectionRequestButtonsOnFloors(int numberOfFloors)
                                throws java.lang.IllegalArgumentException,
                                       InvariantBroken
Initialises all direction requests (up and down, on each floor) to be false

Parameters:
numberOfFloors - is the number of floors in the lift system
Throws:
java.lang.IllegalArgumentException - if the number of floors is <=1
InvariantBroken - if not initialised in a safe state
Method Detail

cancelDownRequest

public void cancelDownRequest(int floor)
                       throws java.lang.IllegalArgumentException,
                              InvariantBroken
Cancel the down request at the specified floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Down_presses_cancels()

Parameters:
floor -
Throws:
java.lang.IllegalArgumentException - if the floor specified is not valid
InvariantBroken

cancelUpRequest

public void cancelUpRequest(int floor)
                     throws java.lang.IllegalArgumentException,
                            InvariantBroken
Cancel the up request at the specified floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()

Parameters:
floor -
Throws:
java.lang.IllegalArgumentException - if the floor specified is not valid
InvariantBroken

downPressedAtFloor

public boolean downPressedAtFloor(int floor)
                           throws java.lang.IllegalArgumentException
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()

Parameters:
floor - specifies the floor at which the down request is being checked
Returns:
if a request to go down has been made at the specified floor
Throws:
java.lang.IllegalArgumentException - if the floor specified is not valid

invariant

public boolean invariant()
The following safety conditions are required: Tested by JUnit_DirectionRequestButtonsOnFloors.test_invariant()

Specified by:
invariant in interface HasInvariant
Returns:
true if all these safety conditions are met, and false otherwise.

noMoreRequestsAbove

public boolean noMoreRequestsAbove(int floor)
                            throws java.lang.IllegalArgumentException
Tested by JUnit_DirectionRequestButtonsOnFloors.test_noMoreRequestsAbove()

Parameters:
floor -
Returns:
whether there is a request at a floor (up or down) above the specified floor
Throws:
java.lang.IllegalArgumentException - if the number of floors specified is not in range

noMoreRequestsBelow

public boolean noMoreRequestsBelow(int floor)
                            throws java.lang.IllegalArgumentException
Tested by JUnit_DirectionRequestButtonsOnFloors.test_noMoreRequestsBelow()

Parameters:
floor -
Returns:
whether there is a request at a floor (up or down) below the specified floor
Throws:
java.lang.IllegalArgumentException - if the number of floors specified is not in range

pressDown

public void pressDown(int floor)
               throws java.lang.IllegalArgumentException,
                      InvariantBroken
Update the down button request except if it is made on bottom floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Down_presses_cancels()

Parameters:
floor - specifies the floor at which the down request is being made
Throws:
java.lang.IllegalArgumentException - if the floor specified is not valid
InvariantBroken

pressUp

public void pressUp(int floor)
             throws java.lang.IllegalArgumentException,
                    InvariantBroken
Update the up button request except if it is made on top floor
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()

Parameters:
floor - specifies the floor at which the up request is being made
Throws:
java.lang.IllegalArgumentException - if the floor specified is not valid
InvariantBroken

toString

public java.lang.String toString()
Typical string representation is of the form:
 Direction Requests For Elevator At Floor: 0- 1-UD 2- 3- 4- 5- 6- 7- 8- 9-
 
In this example, there are 10 floors and up and down requests on the 1st floor

Overrides:
toString in class java.lang.Object

upPressedAtFloor

public boolean upPressedAtFloor(int floor)
                         throws java.lang.IllegalArgumentException
Tested by JUnit_DirectionRequestButtonsOnFloors.test_Up_presses_cancels()

Parameters:
floor - specifies the floor at which the up request is being checked
Returns:
if a request to go up has been made at the specified floor
Throws:
java.lang.IllegalArgumentException - if the floor specified is not valid