[tlaplus] Specify composite objects of Reactive system

[Faria Kanwal <faria.kanwal106@xxxxxxxxx>]

First of all, apologies for poor English, as its not my first language.

I have read the books Specifying Systems, and few topics of Practical
TLA+. Still I'm  not able to understand how to specify a system consist of many different components.
let’s take example of IoT/sensor-base Air Quality monitoring system.
suppose it has different type of nodes (gateway, sensors, and actuator)
Field of node & description
1	N_id: Every node has a unique ID
2	Type: A node may be sensor, gateway or actuator
3	Mode: A node may be in sleeping or active mode
5	Connected: It describes the connectivity of a node
7	info: Represents data which may be sensed, transmitted or received
Types of sensor
1.	Temperature sensor {S_node = Node, S_id = N_id, S_type=”TempSen”, threshold +- 5}
2.	Humidity sensor
Sensors and actuators are connected with the gateway. Sensors are continuously monitoring and transmit info to gateway if passes the threshold. Once gateway receives info it passed it to actuator for some action i.e. turning ON Air conditioner or Humidifier. We can make it more interesting by adding connection type/edge type like edge between sensor-senor -> SS, senor-gateway -> SG … so on. 

All I want to learn how we can specify composite objects like nodes can be of different type each having different properties.

i really appricate if someone point me to the similar examples.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2d243b15-f2a7-4c50-9c0b-75fd4dfb81b3n%40googlegroups.com.