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