Internal Mail Delivery Robot

Introduction

This robot example, originally from a tutorial of PRISM (see here for more information about the example), aims to show how to model and verify the probabilistic behaviour of an internal mail delivery robot.

The original PRISM model consists of three modules:

• controller for robot movements,
• battery for charge of the battery,
• task for handling of tasks and task completion.

The map of the workplace is shown below.

V1

This version uses a multi-way synchronisation of the move event, but the multi-way synchronisation is not supported in RoboChart yet. Please see V2 for another model that uses two-way synchronisation only.

Model (download)

Accordingly, our RoboChart model is also composed of three state machines too:

• movingSTM for movements,
• batterySTM for charge of the battery,
• taskSTM for task management.

The overall behaviour of the robot is specified by a controller deliverCTRL.

Controller

The controller declares two constants

• batteryCharge: initial capacity of the battery,
• and chargeSpeed: charge speed of the battery,

and two variables

• p: current location of the robot,
• and c: current level of the battery,

to allow exchange of information between state machines. Additionally, an interface ctrlVarInf is declared and it will be used in state machines.

As seen from the controller diagram, three state machines will synchronise on the move event.

Movements

The movingSTM state machine has one simple state Stuck to denote the robot gets stuck and cannot move forward, and one composite state Move to specify the movement behaviour from the initial location s0. Inside Move, it has nine sub-states from s0 to s8 that correspond to the nine locations in the map. Please note that each sub-state has an entry action (such as p=3) to update the value of p to its corresponding location. The probabilities of transitions between these sub-states are given by p{...}.

A high-level transition from Move to Stuck (or Move) via a junction provides a way for the robot to be in Stuck (simutaneously set p to 9) when it runs out of power and is not in the charge station 0. Otherwise, it will re-enter the Move and stay in the charge station.

Battery

The battery state machine batterySTM only has one state s0. s0 has two self-loop transitions:

• if the robot is in the charge station (p==0), then the battery will be charged but it won’t exceed its capacity,
• if the robot is not in the charge station (p!=0) and not out of power (c > 0), every move will cost it 1 unit of battery.

Task

The task state machine taskSTM also has only one state s0 but it has more transitions:

• if the robot is free and has no task (FD_NoTask) scheduled, then a new fetching location may be allocated with an equal probability (f/8) and it is going to fetch the mail (FD_FetchMail), or just stay in no task with a probability (1-f);
• if the robot is not in FD_NoTask and its current location is not equal to new destination (g!=p), the robot will continuously synchronise on move (either charge or move to another location);
• if the robot reaches the fetching location (g==p), then it randomly chooses a destination with an equal probability of 1/7 except the fetching location. Additionally, it switches to the mail delivery (FD_DeliverMail);
• after the robot gets to the destiniation (g==p) when it is in FD_DeliverMail, it is back to FD_NoTask and ready for the next task.

Generated PRISM model (download)

Used configuration file.

Analysis

P1) Deadlock free (pass)

!E [ F "deadlock" ]

P2) the probability of running out of power in each location

Using the experiment feature of PRISM to verify the property below by choosing x ranging from 0 to 10 when batteryCharge=20 and chargeSpeed=4,

const int x;
P=? [ F ctrl_ref0_deliverCTRL_p = x & ctrl_ref0_deliverCTRL_c=0 ]

the result is shown below.

We can see that it is highly possible that the robot gets stuck (p=9).

P3) the probability of running out of power in various battery capacites and charge speeds

Using the experiment feature of PRISM to verify the property below by choosing x ranging from 1 to 8 and batteryCharge ranging from 10 to 30 while chargeSpeed is set 4

const int x;
P=? [ F ctrl_ref0_deliverCTRL_p = x & ctrl_ref0_deliverCTRL_c=0 ]

the result is shown below.

Different bettary capacities have different impacts on the probability of running out of power in various locations.

• for the location 2 and 7, no much impact;
• for the location 1, 4 and 6, a larger capacity lowers the possibility;
• however, for the reming locations, a larger capacity increases the possibility.

If we fix the batteryCharge to 20 but change chargeSpeed from 2 to 6, the result is similar.

P4) average number of moves that the robot can perform before running out of power

Add the following reward to the model,

rewards "nbmove"
   [move_xxx_9] true : 1;
endrewards

and check the reward by the R operator below.

R{"nbmove"}=? [ F ctrl_ref0_deliverCTRL_c=0 ]

The result is 31.68876486425289.

P5) average number of deliveries that the robot can perform before running out of power

Add a similar reward to the model,

rewards "nbdelivery"
   [ctrl_ref0_deliverCTRL_stm_ref2_delivery] true : 1;
endrewards

and check the reward by the R operator below.

R{"nbdelivery"}=? [ F ctrl_ref0_deliverCTRL_c=0 ]

The result is 0.5208043954240161.

P6) will the robot always get stuck?

Using the CTL formula below, it is verified to be false. In other words, there exists at least one path to make the robot always run and deliver the mail without being out of power and stuck.

A [ G F ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Stuck ]

But what’s the probability of not being stuck? It is 0.025714458225085668.

P=? [ G ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_scpc!=ctrl_ref0_deliverCTRL_stm_ref0_movingSTM_Stuck ]

V2

Based on the observations about the three-way synchronisation of the model V1,

• batterySTM is always available for synchronisation on move as long as moveSTM is ready since each move in moveSTM has a guard condition c>0. In other word, batterySTM won’t prevent synchronisation but just uses synchronisation to update the current battery level c.

we can use two-way synchronisation only to update c, instead of three-way synchronisation.

Model (download)

The RoboChart module deliverMOD is shown below.

The platform deliverRP provides two constants and two variables wrapped in an interface ctrlVarInf. The controller deliverCTRL synchronises with the platform on three events:

• request for the delivery request from the platform with a location parameter to indicate which office requests it,
• dest for the delivery destination from the platform with a location parameter to indicate which office the delivery targets,
• delivered for the notification from the controller to the platform to indicate the delivery is done.

In stead of three-way synchronisation of the move event, this model only uses two-way synchronisation that RoboChart is able to support now. We still use the move event to synchronise between moveSTM and taskSTM as seen in the controller diagram below.

With regards to the synchronisation between moveSTM and batterySTM, we add two extra events upstart and upend to denote start and end of updates. For moveSTM, we add an action upstart;upend for each transition leaving from a probabilistic junction.

And for batterySTM, we change its state machine as illustrated below.

These two events ensure that every move will be followed by a upstart and a upend to update c, then moveSTM will update p before the next synchronisation on move.

The task state machine is given below.

Note that we use a different way (from the original PRISM model) to model the robot’s behaviour when it runs out of power at the charge station. The robot in the original model will get stuck, however, we still allow its battery to be charged if it runs out of power at the station. The behaviour is reflected by the synchronisation between the transitions from Move to Move via a junction in moveSTM and the transition (modelling the charge of the battery) in batterySTM.

Generated PRISM model (download)

Used configuration file.

Analysis

Properties

constants C1: 
	deliverMOD::rp_ref0::batteryCapacity set to 20, and
	deliverMOD::rp_ref0::chargeStep set to 4
	
constants C2: 
	deliverMOD::rp_ref0::batteryCapacity from set 8:20:4,
	deliverMOD::rp_ref0::chargeStep set to 4
	
label l_stuck = 
		deliverMOD::ctrl_ref0::stm_ref0 is in 
		deliverMOD::ctrl_ref0::stm_ref0::Stuck

label l_batterystate = 
		deliverMOD::ctrl_ref0::stm_ref1 is in 
		deliverMOD::ctrl_ref0::stm_ref1::batteryState
		
label l_move = 
		deliverMOD::ctrl_ref0::stm_ref0 is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move

label l_move_s0 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s0
	
label l_move_s1 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s1
		
label l_move_s2 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s2

label l_move_s3 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s3
		
label l_move_s4 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s4
		
label l_move_s5 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s5
		
label l_move_s6 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s6
		
label l_move_s7 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s7
		
label l_move_s8 =
		deliverMOD::ctrl_ref0::stm_ref0::Move is in 
		deliverMOD::ctrl_ref0::stm_ref0::Move::s8

prob property P_deadlock_free: 
	!E [Finally "deadlock"] 
	with constants C1

rewards nbmove = 
	[deliverMOD::ctrl_ref0::stm_ref0::move] true : 1;
endrewards

prob property R_outofpower_moves: 
	Reward {nbmove} =? [ 
		Reachable {deliverMOD::rp_ref0::c=0} && "l_batterystate" 
	]
	with constants C2

rewards nbdelivery = 
	[deliverMOD::ctrl_ref0::stm_ref2::delivered] true : 1;
endrewards
	 
prob property R_outofpower_deliveries: 
	Reward {nbdelivery} =? [ 
		Reachable {deliverMOD::rp_ref0::c=0} && "l_batterystate"
	]
 	with constant C2

prob property P_stuck_loc_0: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s0"
	] 
	with constant C1

prob property P_stuck_loc_1:
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s1"
	] 
	with constant C1

prob property P_stuck_loc_2: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s2"
	] 
	with constant C1

prob property P_stuck_loc_3: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s3"
	] 
	with constant C1
	
prob property P_stuck_loc_4: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s4"
	] 
	with constant C1
	
prob property P_stuck_loc_5: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s5"
	] 
	with constant C1
	
prob property P_stuck_loc_6: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s6"
	] 
	with constant C1
	
prob property P_stuck_loc_7: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s7"
	] 
	with constant C1
	
prob property P_stuck_loc_8: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_move" && "l_move_s8"
	] 
	with constant C1

prob property P_stuck_loc_9: 
	Prob=? [Finally {deliverMOD::rp_ref0::c=0} 
		&& "l_batterystate" && "l_stuck"
	] 
	with constant C1

Reports

The verification results are displayed in the report below.

Property: P_deadlock_free

Property: R_outofpower_moves

Property: R_outofpower_deliveries

Property: A_stuck

Property: P_stuck_loc_0

Property: P_stuck_loc_1

Property: P_stuck_loc_2

Property: P_stuck_loc_3

Property: P_stuck_loc_4

Property: P_stuck_loc_5

Property: P_stuck_loc_6

Property: P_stuck_loc_7

Property: P_stuck_loc_8

Property: P_stuck_loc_9

V3

Model (download)

The connections of events in the controller have been changed.

In this version, we change the direction of the connection upend from moveSTM to batterySTM. This is due to the fact that a well-formedness condition has been strengthened and so the connection in V2 is no longer valid because a SendEvent statement like upend in moveSTM should be treated as events for output. If the direction isn’t changed, we have to use upend in moveSTM as input. For a simple event like this one, the only place is in the trigger of a transition. We change the direction and so upend will be used in statements, the same as upstart.

The moveSTM is also changed.

We have one more state Update in the Move state. This change is based on an observation in V2 that many transitions in Move have a very similar structure such as p{1/3}/upstart;upend (only the differenece is the probability). So we can have only one probabilistic junction reused by all these states. Now each state in [s0-s8] has one outgoing transition to Update with a trigger move and a condition c>0, then Update has an action upstart;upend leading to the probabilistic junction. From the junction, there is a transition to each state. The transition has only a probability and its value is a conditional depending on the current position of the robot (p). We also make sure the summation of the probabilities from the junction is always equal to 1.0 no matter what p is.

And for batterySTM, we change its state machine as illustrated below, which is also due to the change of the direction of upend.

Since upend is used as input for batterySTM, it could only be in a trigger. So we add a Update state and its outgoing transition to batteryState has the trigger upend.

The task state machine is given below.

Generated PRISM model (download)

Used configuration file.

Analysis

Properties

• basics:

• stuck:

• miscellaneous

Reports

The verification results are displayed in the report below.

Assertion: P_deadlock_free

Assertion: P_stuck_loc

Assertion: P_stuck_loc1

Assertion: R_outofpower_moves

Assertion: R_outofpower_deliveries

Assertion: R_outofpower_deliveries1

Assertion: A_stuck

Assertion: P_stuck

Assertion: A_infinite_delivery

Assertion: P_stuck_loc_0

Assertion: P_stuck_loc_1

Assertion: P_stuck_loc_2

Assertion: P_stuck_loc_3

Assertion: P_stuck_loc_4

Assertion: P_stuck_loc_5

Assertion: P_stuck_loc_6

Assertion: P_stuck_loc_7

Assertion: P_stuck_loc_8

Assertion: P_stuck_loc_9

Conclusion

This case study shows how our RoboChart could be used to model the stochastic behaviour of a delivery robot controller that has a movement control, a battery control, and a task management. The support of hierarchical state machines in RoboChart entitles us to model the situation when the robot runs out of power and gets stuck in a nice way. Additionally, automatically generated PRISM model from the RoboChart model in RoboTool allows us to analyse the probabilistic behaviour of the robot using PRISM.