Tuned docs and formatting

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

@@ -16,12 +16,13 @@
  *
  * This implementation omits some details in the paper. See NOTEs in the comments.
  *
+ * This version has switch1 failing at 3s, node1 failing at 10s, and node2 failing at 15s.
+ *
  * @author Edward A. Lee
  * @author Marjan Sirjani
  */
 target C {
   tracing: true,
-  logging: DEBUG,
   timeout: 20 s
 }
 
@@ -271,7 +272,7 @@ reactor Node(
             }
             self->ping_pending = false;
           } else if (in[c]->value.type == new_NRP) {
-            // FIXME: Should ping the new NRP and send confirmation back to primary.
+            // NOTE: Should ping the new NRP and send confirmation back to primary.
             lf_print(PRINTF_TIME ": Backup node %d received new NRP %d on network %d.",
                 lf_time_logical_elapsed(), self->id, in[c]->value.payload, c
             );

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

@@ -1,6 +1,11 @@
-// This version partitions the network and shows that the protocol
-// prevents the backup from becoming primary, thereby preventing
-// two primaries.
+/**
+ * This version of NRP_FD partitions the network and shows that the protocol prevents the backup
+ * from becoming primary, thereby preventing two primaries.
+ *
+ * @author Edward A. Lee
+ * @author Marjan Sirjani
+ */
+// This version
 target C {
   tracing: true,
   timeout: 20 s

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

@@ -1,5 +1,12 @@
-// This version simply has the primary failing after 5 seconds.
-// Switch 1 remains the NRP.
+/**
+ * This version of NRP_FD simply has the primary (node1) failing after 5 seconds and the backup
+ * (node2) failing at at 15s. The backup detects simultaneous loss of the heartbeat on both networks
+ * and hence assumes that the primary has failed rather than there being a network failure. Switch 1
+ * remains the NRP.
+ *
+ * @author Edward A. Lee
+ * @author Marjan Sirjani
+ */
 target C {
   tracing: true,
   timeout: 20 s