[tlaplus] Re: Specify composite objects of Reactive system

\* Node is composite object
\*where a node can be a Sensor Node, Actuator Node, or a Gateway Node.
\* depending on the type of Node it may sense or keep monitoring the environment, gateway relay the received infomation to the actuators. Actuator nodes are sleeping and get activicated after receiving the information.
\* A node regardless of whether it is sensor, actuator or a gateway has some common fields like NodeID, NodeType, ConnectStatus

EXTENDS Naturals, Sequences, TLC
CONSTANT N
ASSUME N \in 1..10

NodeTypes == {"Sensor", "Gateway", "Actuator"}
EquInfoSensor == {"Sensed", "Monitoring"}
ModeActuator == {"Sleep", "Active"}
EquInfoGateway == {"Received", "Transmitted"}

Node(n) ==
[ NodeID : N,
NodeType : CHOOSE type \in NodeTypes: TRUE,
ConnectStatus : CHOOSE conn \in {TRUE, FALSE}: TRUE,
Attributes : IF NodeTypes = "Sensor"
THEN [ EquInfo |-> CHOOSE e \in EquInfoSensor: TRUE ]
ELSE IF NodeTypes = "Actuator"
THEN [ Mode |-> CHOOSE m \in ModeActuator: TRUE ]
ELSE [ EquInfo |-> CHOOSE e \in EquInfoGateway: TRUE ]
]

VARIABLES nodes

Init ==
/\ nodes = { Node(n) : n \in 1..10 }

On Tuesday 15 October 2024 at 17:33:49 UTC+5 Andrew Helwer wrote:

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.