SRing_3Node
Sensor1
Sensor2
Sensor2
Sensor3
Sensor3
Sensor1
Sensor1->Sensor2
Sensor2->Sensor3
Sensor3->Sensor1
//Assertions
#define FalseUpdated Sensor1.App.code == 0;
#define AllUpdated (Sensor1.App.code == 1 && Sensor2.App.code == 1 && Sensor3.App.code == 1);
#assert SensorNetwork deadlockfree;
#assert SensorNetwork reaches FalseUpdated;
#assert SensorNetwork |= <> AllUpdated;
#assert SensorNetwork |= []<> AllUpdated;
Sensor1
0
TrickleNewAppC
/* enter the sensor settings here... */
2
Sensor2
0
TrickleAppC
/* enter the sensor settings here... */
2
Sensor3
0
TrickleAppC
/* enter the sensor settings here... */
2