Fix further inconsistencies.

Author: hokeun

02-inconsistency.md

@@ -83,14 +83,14 @@ Time →
 California node:    curtail -80 ──────────────────────────► gm1 sees it first
 New York node:                   dispatch +100 ────────────► gm1 sees it second
                                                                    ↓
-                                                         gm1 final: -130 MW ✓ no event
+                                                          gm1 final: -50 MW ✓ no event
 
 California node:    curtail -80 ────────────────────────────────────────────────► gm2 sees it second  
 New York node:                   dispatch +100 ──────────────────────────────► gm2 sees it first
                                                                                      ↓
-                                                                           gm2 final: -50 MW ✓ no event
+                                                                           gm2 final: -130 MW ✓ no event
 
-But gm1 (-130) ≠ gm2 (-50): INCONSISTENT STATE!
+But gm1 (-50) ≠ gm2 (-130): INCONSISTENT STATE!
 ```
 
 In a real grid, this inconsistency means the two control centers have **contradictory views of grid health**. Automated systems making decisions based on these views could take opposing corrective actions, worsening the situation.

06-cal-theorem.md

@@ -28,34 +28,31 @@ The CAL theorem says that strong consistency requires enough waiting, or enough
 
 ## The Design Space, Summarized
 
-Here is a map of the designs from this tutorial against the consistency-availability tradeoff:
+Here is a map of the designs from this tutorial against the consistency-availability tradeoff. Step 5 is shown as two paths because it deliberately gives different guarantees to different classes of commands:
 
 ```
 CONSISTENCY
-    ▲
-    │  Step 4 (Chandy-Misra, maxwait=forever)
-    │    Strong consistency
-    │    Availability: unbounded wait on failure
-    │
-    │  Step 3 (Timestamps, finite maxwait)
-    │    Strong consistency when maxwait ≥ latency
-    │    Availability: bounded wait (<= maxwait)
-    │    Risk: fault is possible if maxwait < actual latency
-    │
-    │  Step 5 (Hybrid)
-    │    Strong consistency for curtailments (maxwait=forever)
-    │    Bounded availability for dispatches (maxwait=30ms)
-    │    Fault handler handles occasional stale estimates
-    │
-    │  Step 2 (Non-commutative, no coordination)
-    │    No consistency (permanent divergence)
-    │    High availability (no wait)
-    │
-    │  Step 1 (Commutative CRDT)
-    │    Eventual consistency
-    │    Maximum availability (no wait)
-    │
-    └────────────────────────────────────────────► AVAILABILITY
+strong ▲  Step 4: conservative coordination
+       │    Strong consistency; may wait forever if an upstream node stops.
+       │
+       │  Step 5 slow path: curtailments
+       │    Same strong-consistency path as Step 4 for high-risk commands.
+       │
+       │             Step 3: finite maxwait
+       │               Strong consistency only while apparent latency <= maxwait;
+       │               otherwise the tardy handler is part of the design.
+       │
+eventual│                                      Step 5 fast path: dispatch-up
+       │                                        Fast response with later reconciliation.
+       │
+       │                                      Step 1: commutative actor
+       │                                        Eventual consistency and maximum availability.
+       │
+none   │                                      Step 2: non-commutative actor
+       │                                        High availability, but possible permanent divergence.
+       │
+       └────────────────────────────────────────────────────────► AVAILABILITY
+          low / may block                                      high / responds fast
 ```
 
 ---

src/Step2_Inconsistency.lf

@@ -96,7 +96,7 @@ reactor InconsistentGridManager(node_id: int = 1) {
 // ------------------------------------------------------------
 federated reactor {
   gi1 = new GridInterface(id=1, node_name="California")
-  gi2 = new GridInterface(id=2, node_name="NewYork")
+  gi2 = new GridInterface(id=2, node_name="New York")
   gm1 = new InconsistentGridManager(node_id=1)
   gm2 = new InconsistentGridManager(node_id=2)
 

src/Step3_Timestamps.lf

@@ -91,6 +91,17 @@ reactor GridManager {
         }
     }
     lf_set(out, self->balance);
+  =} tardy {=
+    tag_t intended_tag;
+    if (in1->is_present) {
+        intended_tag = in1->intended_tag;
+    } else {
+        intended_tag = in2->intended_tag;
+    }
+    lf_print_warning("[ts=%lld] Tardy message with intended timestamp %lld received at physical time %lld",
+                     lf_time_logical_elapsed(),
+                     intended_tag.time - lf_time_start(),
+                     lf_time_physical_elapsed());
   =}
 }
 
@@ -101,7 +112,7 @@ reactor GridManager {
 // ------------------------------------------------------------
 federated reactor {
   gi1 = new GridInterface(id=1, node_name="California")
-  gi2 = new GridInterface(id=2, node_name="NewYork")
+  gi2 = new GridInterface(id=2, node_name="New York")
 
   // maxwait: physical time to wait before assuming no more messages will
   // arrive at a given logical time or earlier. A tardy message is one that
@@ -112,9 +123,9 @@ federated reactor {
   // maxwait = 100 ms: safe for cross-continental links with NTP sync.
   // A smaller maxwait will improve responsiveness, but increase the risk
   // of tardy messages.
-  @maxwait(1 us)
+  @maxwait(100 ms)
   gm1 = new GridManager()
-  @maxwait(1 us)
+  @maxwait(100 ms)
   gm2 = new GridManager()
 
   gi1.command -> gm1.in1  // Logical connections: timestamps are carried and ordering is enforced.