From eccf08db550e1d8fdc480cd817f8aa67b668ed90 Mon Sep 17 00:00:00 2001
From: "Edward A. Lee" <eal@berkeley.edu>
Date: Mon, 15 Jan 2024 17:38:06 -0800
Subject: [PATCH] Tuned docs and formatting

---
 examples/C/src/leader-election/NRP_FD.lf              |  5 +++--
 examples/C/src/leader-election/NRP_FD_Partitioning.lf | 11 ++++++++---
 examples/C/src/leader-election/NRP_FD_PrimaryFails.lf | 11 +++++++++--
 3 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/examples/C/src/leader-election/NRP_FD.lf b/examples/C/src/leader-election/NRP_FD.lf
index 1de9b10f..ea172f35 100644
--- a/examples/C/src/leader-election/NRP_FD.lf
+++ b/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
             );
diff --git a/examples/C/src/leader-election/NRP_FD_Partitioning.lf b/examples/C/src/leader-election/NRP_FD_Partitioning.lf
index 62c01a95..3a046333 100644
--- a/examples/C/src/leader-election/NRP_FD_Partitioning.lf
+++ b/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
diff --git a/examples/C/src/leader-election/NRP_FD_PrimaryFails.lf b/examples/C/src/leader-election/NRP_FD_PrimaryFails.lf
index b0973995..c9ed2969 100644
--- a/examples/C/src/leader-election/NRP_FD_PrimaryFails.lf
+++ b/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