This is an example of the website to submit for each robot. The website is incomplete in some places indicated by '...'. For the exact numbers and types of assumptions and guarantees you need to include, check the email sent by Shahar. If you have any questions ask us.
To download the sources and CSS of this website use this link.
Forklift Robot Synthesis Specification Example
We present a forklift robot. The robot can drive around, avoid obstacles, detect cargo stations, and lift and deliver cargo.
The NXT Robot
The NXT robot has a fork it can lift and drop. It has two motors powering its left and right wheel while a third wheel stabilizes the robot in the back. The forklift has a distance sensors to detect low obstacles and cargo, a distance sensor to detect obstacles that block its way, a color sensor to detect, based on the color of the floor, whether it is at a station, and an emergency off switch.
The robot is built from a LEGO MINDSTORMS NXT 2.0 (8547) set. The building instructions are available here. We have extended the robot with a color sensor (number 9694) and a second ultrasonic distance sensor (number 9846) as shown in the picture below.
We now give an informal description of the forklift robot and its task in natural language. The description has a numbered list of requirements that describe what the forklift should do and what it should not do (this description is independent of the technical realization).
The list of requirements of the forklift is followed by a list of assumptions on the environment the forklift operates in. These assumptions describe properties of the environment that the forklift may rely on, to fulfil its requirements. The assumptions are again numbered so we can later refer to them.
Requirements
Do not run into obstacles. Pay special attention to low obstacles to not hit them with the fork.
Only pick up or drop cargo at stations.
Do not attempt to lift cargo if cargo is lifted.
Always keep on delivering cargo.
Never drop cargo at the station where it was picked up.
Stop moving if emergency off switch is pressed.
Assumptions
The forklift will always be able to eventually find a station with cargo by going forward. The same applies for delivering cargo.
The forklift will always be able to eventually leave a station by going forward or backward.
The forklift can back up or turn to avoid obstacles.
If the forklift stops at a station it remains there.
The forklift is implemented as a Component and Connector architecture, where components encapsulate functionality and connectors enable communication between components.
The components of the forklift are shown below. The system is composed from four sensor components, a controller component, and three actuator components:
stationSense of type StationSensor(SensorPort) encapsulates access to the color sensor detecting a station
...
...
...
...
lMot and rMot of type Motor(MotorPort) encapsulate control of the right and left motor
The most interesting component in this system is the component Controller. This component controls the actions of the motors based on the values received from the sensors. We will synthesize the implementation of this component.
Controller Interface
The interface of a component defines how it can interact with its environment. An interface consists of types input and output ports. The controller component of the forklift is shown below. The datatypes used for the definition of its interface the type boolean and additional enumeration types shown in the right part of the figure below.
The controller component has five input ports:
liftAck of type boolean to receive feedback from the lift motor
atStation of type boolean to receive inputs from the station sensor
obstacle of type Distance to receive inputs from the upper distance sensor
cargo of type Distance to receive inputs from the lower distance sensor
emgOff of type boolean to receive inputs from the emergency off button
The controller component has three output ports:
lMot of type MotorCmd to send commands to the left motor
rMot of type MotorCmd to send commands to the right motor
lift of type LiftMotorCmd to send commands to the motor lifting the fork
Wrappers for Sensors and Actuators
All sensor and actuator components are implemented as wrappers in Java that provide access to the underlying APIs of LeJOS to interface the hardware of the NXT.
The component StationSensor is implemented on top of LeJOS API class ColorSensor. In the constructor of the component the flood light of the color sensor is turned on to provide better readings. During each execution cycle the component reads the light value of the color sensor and decides for dark color values to send the output true. Lighter values above the threshold of 400 are treated as not detecting a station. Relevant code of the component is shown below.
The component DistanceSensor is implemented on top of LeJOS API class UltraSonicSensor. ...
The component Motor is implemented on top of LeJOS API class NXTRegulatedMotor. ...
The component LiftMotor is implemented on top of LeJOS API class NXTRegulatedMotor. ...
The components of the forklift are executed according to a fixed schedule. First all sensor components compute the input for the controller, second the controller executes, and third the actuator components are executed.
The execution of component LiftMotor is a special case. This component produces an input (liftAck) that has to be available for the execution of the controller. LiftMotor is thus executed first:
The following CMP code shows the implementation of the scheduler.
<<Deploy>> component ForkLift {
// exception to put it first because it sends data to controller
component LiftMotor(lejos.nxt.Motor.A) mLift;
// sensors
component StationSensor(lejos.nxt.SensorPort.S1) stationSense;
component DistanceSensor(lejos.nxt.SensorPort.S2, 20) distSense;
component Button(lejos.nxt.SensorPort.S3) emgOffButton;
component DistanceSensor(lejos.nxt.SensorPort.S4, 9) cargoSense;
// controller
component Controller controller;
// actuators
component Motor(lejos.nxt.Motor.B) mLeft;
component Motor(lejos.nxt.Motor.C) mRight;
// input from sensors to controller
connect stationSense.sense -> controller.station;
connect distSense.sense -> controller.sense;
connect emgOffButton.pressed -> controller.emgOff;
connect cargoSense.sense -> controller.cargo;
connect mLift.ack -> controller.liftAck;
// output from controller to actuators
connect controller.lift -> mLift.cmd;
connect controller.mLeft -> mLeft.cmd;
connect controller.mRight -> mRight.cmd;
}
The scheduler generated from the CMP code executes the compute() method of each component one after the other and then waits two seconds to start the next execution cycle.
We synthesize an implementation for the component Controller from an Spectra specification consisting of variable declarations and assumptions and guarantees written in Spectra.
Variable definition
As part of the synthesis module we define one variable for every input port of the component controller (env) and one variable for every output port (sys). The domain of the variables corresponds to the datatype of the ports.
The monitor loaded used in the assumptions and guarantees below is defined using the following code. It "remembers" whether the forklift has loaded cargo or not.
/**
* monitor loaded is true iff we have cargo loaded and acknowledged
*/
monitor boolean loaded {
!loaded;
G (liftAck & !loaded -> next(loaded));
G (liftAck & loaded -> next(!loaded));
G (!liftAck -> loaded = next(loaded));
}
Guarantees
We express the requirements of the forklift as guarantees in Spectra.
Initially, the forklift does not move, does not lift anything, and has no cargo loaded:
// initial state
guarantee
stopping & lift = NIL;
The forklift should not run into obstacles and it should not turn if it is too close to a low obstacle (otherwise the fork might hit the obstacle).
// G1 dont run into obstacles
guarantee
G ((sense = BLOCKED | lowObstacle) -> ! forwarding);
// don't mess with low obstacles
guarantee
G (cargo=BLOCKED -> !turning);
The following guarantee uses the Spectra specification pattern P09 to express that the forklift has to leave the station before it delivers its cargo:
gar leaveStationForDelivery:
pBecomesTrue_betweenQandR(!station, lifting, dropping);
Finally, we state that the forklift should always eventually deliver cargo:
guarantee
GF (lift=DROP | emgOff | lowObstacle);
The initial version of the last guarantee shown above was GF (lift = DROP) without the alternatives emgOff | lowObstacle. It turns out that there exists an adversarial environment that prevents any system from fulfilling this original goal by always eventually stopping or blocking the robot. The alternatives have thus been added to the specification.
Assumptions
We now present and discuss the environment assumptions of the forklift.
We assume that the forklift will always eventually find cargo or a station to drop off cargo by going forward. Exceptions are made if the forklift goes backwards or stops. These two assumptions use the response pattern:
// A1 find cargo if going forward to next station
assumption
pRespondsToS(forwarding & !loaded, (station & cargo=BLOCKED) | backing | stopping);
assumption
pRespondsToS(forwarding & loaded, (station & cargo=CLEAR) | backing | stopping);
Very similar assumptions following the same pattern are that the forklift will be able to leave stations by going forward or backward without stopping:
// A2 leave station eventually
assumption
pRespondsToS(forwarding, !station | stopping);
assumption
pRespondsToS(backing, !station | stopping);
An important assumption about the station sensor is that its reading remains the same whenver the forklift does not move:
// station does not change when stopping
assumption
G (stopping -> station = next(station));
Statistics
The specification is realizable. The statistics of synthesis are as follows:
The forklift specification allows for multiple variants. We present a variant where the emergency off feature is missing. The new specification is smaller and can be synthesized faster. Another variant of the forklift uses continuous control instead of a delay. The specification is larger but still synthesizes faster.
We also present two unrealizable specifications and explain their reasons for unrealizability.
No Emergency Off Switch (Realizable)
In the specification variant that does not support the emergency off switch the input emgOff for the switch and the guarantee to stop when it is pressed are removed:
// deleted environment variable emgOff
env boolean emgOff;
// removed guarantee to stop
guarantee
G (emgOff -> (stopping & lift=NIL));
In addition the occurrence of the variable emgOff in the justice constraint to always eventually deliver cargo is removed:
// deleted emgOff from the following justice constraint
guarantee
GF (lift=DROP | lowObstacle);
The specification is realizable. The statistics of synthesis are as follows:
We now focus on a variant where the controller to be aware whether lifting actions have completed or not. Driving actions already get feedback from distance sensors but we had to add an additional feedback signal from the lift motor to acknowledge completion of its actions (see highlight in CMP model below).
The scheduler has to execute component LiftCmd first, see Scheduler).
The input signal liftAck is modeled by a boolean environment variable. We have added a monitor waitingForLifting to remember whether a lifting command was sent but not yet acknowledged.
/**
* monitor waitingForLifting is true when we have lifted or dropped and are
* not received a liftAck
*/
monitor boolean waitingForLifting {
!waitingForLifting;
// monitorWaitingForLifting:
G ((lift=LIFT | lift=DROP) -> next(waitingForLifting));
// switchWaitingUnlessNewCommand:
G (liftAck -> (next(!waitingForLifting) | lift=LIFT | lift=DROP));
// sameWaitingStatus:
G (!(lift=LIFT | lift=DROP | liftAck) -> waitingForLifting = next(waitingForLifting));
}
The following assumptions were added to model the behavior of component LiftMotor regarding acknowledgements.
assumption
!liftAck;
assumption
pRespondsToS(waitingForLifting, liftAck);
// no strange lifting acks
assumption
G (next(liftAck) -> (waitingForLifting & !liftAck));
The last assumption is a bit tricky: It basically expresses that the environment can only acknowledge lifting in the next state if in the current state the controller is waiting for lifting and the environment does not already acknowledge lifting.
Two new guarantees state that the forklift should not move whenever it is waiting for lifting to be completed and that it should not send another lift command while it is waiting:
guarantee stopWhenWaiting:
G (waitingForLifting -> stopping);
guarantee dontLiftWhenWait:
G (waitingForLifting -> lift=NIL);
The specification is realizable. The statistics of synthesis are as follows:
A variant of the above specification has a simplified justice constraint:
guarantee
GF (lift = DROP);
This variant is unrealizable. An adversary environment can always win. Initially, the forklift is not at a station. The forklift drives forwards to force the environment to reach a station (see assumption above about driving forward). The environment prevents the forklift from finding a station by presenting a low obstacle. The forklift will stop or turn because of the obstacle. This satisfies the assumption of finding a station.
To download the sources and CSS of this website use this link.