Specify composite objects of Reactive system

[Faria Kanwal]

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.

[Andrew Helwer]

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

[Faria Kanwal]

Thank you for your response. I tried record/structure to define a composite object, Node. Below is the part of the specification. Is it the right and the only way to specify such composite object? 

------------------------------------------ MODULE Node ------------------------------------------

\* 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 }

Next==

===============

[Andrew Helwer]

It is not the only way. There is the age-old design decision analogous to the choice between an array-of-records and  record-of-arrays. You have gone for the array-of-records approach here, and an alternative is to make each field in the node (NodeType, ConnectionStatus, etc.) its own variable, and then index into those variables with the node ID to get the value of that field for a given node.

Also note that CHOOSE is not nondeterministic. It will always give the same choice from a set.

Andrew