Visualization of the system map SENSOR_TYPE deployed read LOCATION_TYPE TEMPERATURE_TYPE

A system maintains a number of sensors, where each is deployed in a separate location in order to read the location’s temperature. Before the system is deployed, all locations are marked on a map, and each location will be addressed by a sensor. The formal specification of the system introduces the following three types: 
SENSOR_TYPE, 
LOCATION_TYPE, 
TEMPERATURE_TYPE

State schema:

--TempMonitor------------------------------------------
|deployed : P SENSOR_TYPE 
|map : SENSOR_TYPE ↛ LOCATION_TYPE
|read : SENSOR_TYPE ↛ TEMPERATURE_TYPE 
|________________
|deployed = dom map 
|deployed = dom read
|____________________________________________________________

Operation DeploySensorOK:
Operation DeploySensorOK places a new sensor to a unique location. We may assume that some (default) temperature is also passed as an argument.

--DeploySensorOK------------------------------------------
|∆TempMonitor 
|sensor? : SENSOR_TYPE 
|location? : LOCATION_TYPE 
|temperature? : TEMPERATURE_TYPE
|________________
|sensor? ∈/ deployed 
|location? ∈/ ran map 
|deployed′ = deployed ∪ {sensor?} 
|map′ = map ∪ {sensor? 7→ location?} 
|read′ = read ∪ {sensor? 7→ temperature?} 
|_______________________________________________________________

Operation ReadTemperatureOK:
Operation ReadTemperatureOK obtains the temperature reading from a sensor, given the sensor’s location.

--ReadTemperatureOK----------------------------------------
| ΞTempMonitor 
|location? : LOCATION_TYPE 
|temperature! : TEMPERATURE_TYPE 
|______________
|location? ∈ ran map 
|temperature! = read(map^−1 (location?)) 
__________________________________________________________________

Success and error schemata: 
We introduce an enumerated type MESSAGE which will assume values that correspond to success and error messages. 
-Success-------------------------------------------------- 
|ΞTempMonitor 
|response! : MESSAGE 
_____________
|response! = ′ok′ 
_____________________________________________________________

Error schema SensorAlreadyDeployed for DeploySensorOK:
Operation DeploySensorOK places the following precondition: 
sensor? ∈/ deployed
We provide an error schema for the case where this precondition fails:

--SensorAlreadyDeployed---------------------------------------
|ΞTempMonitor 
|sensor? : SENSOR_TYPE
|response! : MESSAGE 
_____________
|sensor? ∈ deployed 
|response! = ′Sensor deployed′ 
____________________________________________________________________

Error schema LocationAlreadyCovered for DeploySensorOK:
Operation DeploySensorOK places the following precondition: 
location? ∈/ ran map 
We provide an error schema for the case where this precondition fails: 

-LocationAlreadyCovered------------------------------------
|ΞTempMonitor 
|location? : LOCATION_TYPE 
|response! : MESSAGE 
_____________
|location? ∈ ran map 
|response! = ′Location already covered′ 
________________________________________________________________

Error schema LocationUnknown for ReadTemperatureOK:
 Operation ReadTemperatureOK places the following precondition: location? ∈ ran map 
We provide an error schema for the case where this precondition fails: 

-LocationUnknown-----------------------------------------------
|ΞTempMonitor 
|location? : LOCATION_TYPE 
|response! : MESSAGE 
____________
|location? ∈/ ran map 
|response! = ′Location not covered′ 
____________________________________________________________________

Defining reliable operations:
DeploySensor ˆ= (DeploySensorOK ∧ Success) ⊕ (SensorAlreadyDeployed ∨ LocationAlreadyCovered) 
ReadTemperature ˆ= (ReadTemperatureOK ∧ Success) ⊕ LocationUnknown

QUESTION: Consider the temperature monitoring system. In this part, extend the specification with a new requirement: Operation ReplaceSensor Sensors are physical devices, subjected to deterioration, or
other type of damage. We need to provide the ability of the system to replace a sensor with another. For simplicity, let us not plan to (“fix” and) reuse them, but permanently remove them from the system.