[tlaplus] Re: Specify composite objects of Reactive system

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

Yes, you probably want to use records for this. So your set of all valid records might look like (trying to figure out from your description):

CONSTANT NodeId

VARIABLE state

State == [
  type      : {"gateway", "sensor", "actuator"},
  id        : NodeId,
  mode      : {"sleeping", "active"},
  connected : BOOLEAN,
  info      : Info
]

And then you would define variable state to be some member of the set State that can transition to other values over time (perhaps gaining or losing connection, becoming active or going to sleep, sending data to other nodes, etc.)

Andrew Helwer

On Tuesday, October 15, 2024 at 3:57:50 AM UTC-4 Faria Kanwal wrote:

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/99e29141-9f1d-4a6f-8147-0ea2e6ccc5f1n%40googlegroups.com.