Updated to use multiports and make federated

examples/C/src/leader-election/NRP_FD.lf

@@ -1,6 +1,6 @@
 /**
- * This program models a redundant fault tolerant system where a primary node, if and when it fails,
- * is replaced by a backup node. The protocol is described in this paper:
+ * This program implements a redundant fault-tolerant system where a primary node, if and when
+ * it fails, is replaced by a backup node. The protocol is described in this paper:
  *
  * Bjarne Johansson; Mats Rågberger; Alessandro V. Papadopoulos; Thomas Nolte, "Consistency Before
  * Availability: Network Reference Point based Failure Detection for Controller Redundancy," Emerging
@@ -465,8 +465,7 @@ reactor Switch(
     =}
   }
 }
-// FIXME: This should be federated, but bugs in federated execution make it fail.
-main reactor(heartbeat_period: time = 1 s, delay: time = 1 ms) {
+federated reactor(heartbeat_period: time = 1 s, delay: time = 1 ms) {
   node1 = new Node(heartbeat_period=heartbeat_period, id=1, fails_at_time = 10 s)
   switch1 = new Switch(id=1, fails_at_time = 3 s)
   switch3 = new Switch(id=3)

examples/C/src/leader-election/NRP_FD_Partitioning.lf

@@ -1,36 +1,32 @@
 // This version partitions the network and shows that the protocol
 // prevents the backup from becoming primary, thereby preventing
 // two primaries.
-target C
+target C {
+  tracing: true,
+  timeout: 20 s
+}
 
 import Switch, Node from "NRP_FD.lf"
 
-main reactor(heartbeat_period: time = 1 s, delay: time = 1 ms) {
+federated reactor(heartbeat_period: time = 1 s, delay: time = 1 ms) {
   node1 = new Node(heartbeat_period=heartbeat_period, id=1, fails_at_time = 15 s)
   node2 = new Node(heartbeat_period=heartbeat_period, id=2, fails_at_time = 15 s)
 
   switch1 = new Switch(id=1, fails_at_time = 3 s)
   switch2 = new Switch(id=2)
+  switch3 = new Switch(id=3)
+  // Failure of switch4 will partition the network.
+  switch4 = new Switch(id=4, fails_at_time = 10 s)
 
-  node1.out1 -> switch1.in1 after delay
-  switch1.out1 -> node1.in1 after delay
+  node1.out -> switch1.in1, switch3.in1 after delay
+  switch1.out1, switch3.out1 -> node1.in after delay
 
   switch1.out2 -> switch2.in2 after delay
   switch2.out2 -> switch1.in2 after delay
 
-  switch2.out1 -> node2.in1 after delay
-  node2.out1 -> switch2.in1 after delay
-
-  switch3 = new Switch(id=3)
-  // Failure of switch4 will partition the network.
-  switch4 = new Switch(id=4, fails_at_time = 10 s)
-
-  node1.out2 -> switch3.in1 after delay
-  switch3.out1 -> node1.in2 after delay
+  switch2.out1, switch4.out1 -> node2.in after delay
+  node2.out -> switch2.in1, switch4.in1 after delay
 
   switch3.out2 -> switch4.in2 after delay
   switch4.out2 -> switch3.in2 after delay
-
-  switch4.out1 -> node2.in2 after delay
-  node2.out2 -> switch4.in1 after delay
 }

examples/C/src/leader-election/NRP_FD_PrimaryFails.lf

@@ -1,34 +1,30 @@
 // This version simply has the primary failing after 5 seconds.
 // Switch 1 remains the NRP.
-target C
+target C {
+  tracing: true,
+  timeout: 20 s
+}
 
 import Switch, Node from "NRP_FD.lf"
 
-main reactor(heartbeat_period: time = 1 s, delay: time = 1 ms) {
+federated reactor(heartbeat_period: time = 1 s, delay: time = 1 ms) {
   node1 = new Node(heartbeat_period=heartbeat_period, id=1, fails_at_time = 5 s)
   node2 = new Node(heartbeat_period=heartbeat_period, id=2, fails_at_time = 15 s)
 
   switch1 = new Switch(id=1)
   switch2 = new Switch(id=2)
+  switch3 = new Switch(id=3)
+  switch4 = new Switch(id=4)
 
-  node1.out1 -> switch1.in1 after delay
-  switch1.out1 -> node1.in1 after delay
+  node1.out -> switch1.in1, switch3.in1 after delay
+  switch1.out1, switch3.out1 -> node1.in after delay
 
   switch1.out2 -> switch2.in2 after delay
   switch2.out2 -> switch1.in2 after delay
 
-  switch2.out1 -> node2.in1 after delay
-  node2.out1 -> switch2.in1 after delay
-
-  switch3 = new Switch(id=3)
-  switch4 = new Switch(id=4)
-
-  node1.out2 -> switch3.in1 after delay
-  switch3.out1 -> node1.in2 after delay
+  switch2.out1, switch4.out1 -> node2.in after delay
+  node2.out -> switch2.in1, switch4.in1 after delay
 
   switch3.out2 -> switch4.in2 after delay
   switch4.out2 -> switch3.in2 after delay
-
-  switch4.out1 -> node2.in2 after delay
-  node2.out2 -> switch4.in1 after delay
 }