Merge pull request #3 from lf-lang/refine

Fix inconsistency, add tmux instructions, and add lff in CI test.

Author: hokeun

.github/workflows/lf-ci.yml

@@ -30,13 +30,21 @@ jobs:
           sudo apt-get update
           sudo apt-get install -y build-essential cmake
 
+      - name: Check LF files are formatted
+        uses: lf-lang/action-check-lf-files@main
+        with:
+          check_mode: "format"
+          search_dir: "src"
+          compiler_ref: "master"
+
       - name: Check LF files compile
         uses: lf-lang/action-check-lf-files@main
         with:
           check_mode: "compile"
           no_compile_flag: false
           search_dir: "src"
           compiler_ref: "master"
+          skip_clone: true
 
       - name: Smoke-run generated LF programs
         shell: bash
@@ -54,15 +62,12 @@ jobs:
           for file in "${lf_files[@]}"; do
             name="$(basename "$file" .lf)"
 
-            launch_script="bin/${name}_launch.sh"
             executable="bin/${name}"
 
-            if [[ -x "$launch_script" ]]; then
-              runner="$launch_script"
-            elif [[ -x "$executable" ]]; then
+            if [[ -x "$executable" ]]; then
               runner="$executable"
             else
-              echo "No generated executable or launch script found for $file."
+              echo "No generated launcher found at $executable for $file."
               exit 1
             fi
 

01-actor-model.md

@@ -20,7 +20,7 @@ In the classical actor model, components communicate via **asynchronous message
 
 Here is what our system looks like:
 
-![DistibutedPowerGrid Actor](fig/DistibutedPowerGrid1_Actor.svg)
+![Step 1 actor model diagram](fig/Step1_Actor.svg)
 
 
 The squiggly arrows (`~>`) are **physical connections** in Lingua Franca: they use TCP for reliable in-order delivery on each link, but carry **no timestamp coordination** between links. Messages from California and New York may arrive at either grid manager in any order.
@@ -35,51 +35,98 @@ The core reactor is `SimpleGridManager`:
 
 ```lf
 reactor SimpleGridManager {
-  input in1: int   // commands arriving from local operator
-  input in2: int   // commands arriving from remote operator
+  input in1: int   // commands arriving from California
+  input in2: int   // commands arriving from New York
   output out: int  // current balance reported back to local operator
 
   state balance: int = 0
 
   reaction(in1, in2) -> out {=
     if (in1->is_present) {
         self->balance += in1->value;
-        lf_print("Local command %+d MW -> balance now %d MW",
+        lf_print("California command %+d MW -> balance now %d MW",
                  in1->value, self->balance);
     }
     if (in2->is_present) {
         self->balance += in2->value;
-        lf_print("Remote command %+d MW -> balance now %d MW",
+        lf_print("New York command %+d MW -> balance now %d MW",
                  in2->value, self->balance);
     }
     lf_set(out, self->balance);
   =}
 }
 ```
 
-The top-level federated program wires everything together:
+The top-level federated program wires everything together. For the first exercise, the operator consoles are scripted with parameters, so you can change the trace without writing new reactors or timers:
 
 ```lf
 federated reactor {
-    op1 = new GridInterface(...)   // California operator console
-    op2 = new GridInterface(...)   // New York operator console
-    gm1 = new SimpleGridManager()
-    gm2 = new SimpleGridManager()
-
-    op1.command ~> gm1.in1    // California commands -> California manager (local)
-    op2.command ~> gm2.in2    // New York commands   -> New York manager (local)
-    op1.command ~> gm2.in1    // California commands -> New York manager (remote)
-    op2.command ~> gm1.in2    // New York commands   -> California manager (remote)
-
-    gm1.out ~> op1.status
-    gm2.out ~> op2.status
+    gi1 = new ScriptedGridInterface(
+        node_name="California",
+        command_value=100,
+        command_time=0 ms
+    )
+    gi2 = new ScriptedGridInterface(
+        node_name="New York",
+        command_value=-100,
+        command_time=1 ms
+    )
+    gm1 = new SimpleGridManager(node_name="California manager")
+    gm2 = new SimpleGridManager(node_name="New York manager")
+
+    gi1.command ~> gm1.in1    // California commands -> California manager (local)
+    gi2.command ~> gm2.in2    // New York commands   -> New York manager (local)
+    gi1.command ~> gm2.in1    // California commands -> New York manager (remote)
+    gi2.command ~> gm1.in2    // New York commands   -> California manager (remote)
+
+    gm1.out ~> gi1.status
+    gm2.out ~> gi2.status
 }
 ```
 
 Each grid manager receives commands from **both** operators and keeps its own copy of the balance. The local operator console gets the balance back from its local manager.
 
 ---
 
+## Running Step 1
+
+Compile the LF program with `lfc`:
+
+```bash
+lfc src/Step1_Actor.lf
+```
+
+Because this is a federated LF program, compilation generates a launcher under `bin/` named after the source file:
+
+```bash
+./bin/Step1_Actor
+```
+
+This launches the runtime infrastructure (RTI) and the four federates:
+
+- `federate__gi1`: California grid interface
+- `federate__gi2`: New York grid interface
+- `federate__gm1`: California grid manager
+- `federate__gm2`: New York grid manager
+
+To see each federate in its own terminal pane, run the launcher with `--tmux`:
+
+```bash
+./bin/Step1_Actor --tmux
+```
+
+If `tmux` is not installed, install it first, for example with `brew install tmux` on macOS or `sudo apt-get install tmux` on Ubuntu.
+
+Inside the tmux view, the top pane is the RTI and the other panes are the federates. The program has a built-in timeout, so it should finish on its own. To leave and close the entire tmux session after the run, press `Ctrl+B`, then `D`. If you need to stop a still-running federation, press `Ctrl+C` in the RTI pane, then detach with `Ctrl+B`, then `D`.
+
+Example tmux run:
+
+![Step 1 tmux run](assets/step1-actor-tmux.png)
+
+In the screenshot, the managers receive the California and New York commands in different orders, but both managers end with balance `0 MW`.
+
+---
+
 ## Why This Works, Sometimes
 
 The operation `balance += value` has a special mathematical property: it is **associative and commutative**. It doesn't matter what order the additions happen; the final sum is always the same.
@@ -108,7 +155,7 @@ That's what we explore next.
 
 ## Exercises
 
-1. Trace through a scenario: California dispatches +100 MW at time 0, New York curtails −100 MW at time 1 ms. Show that both grid managers reach the same balance regardless of message arrival order.
+1. Trace through a scenario: California dispatches +100 MW at time 0 ms, New York curtails −100 MW at time 1 ms. Show that both grid managers reach the same balance regardless of message arrival order.
 
 2. What would happen if TCP delivery were *not* guaranteed? How would the ACID 2.0 / CRDT properties need to change?
 

02-inconsistency.md

@@ -44,7 +44,7 @@ reactor InconsistentGridManager {
 
 Here is what our system looks like:
 
-![DistibutedPowerGrid2_Inconsistency](fig/DistibutedPowerGrid2_Inconsistency.svg)
+![Step 2 inconsistency diagram](fig/Step2_Inconsistency.svg)
 
 
 ---

03-timestamps.md

@@ -30,12 +30,12 @@ The only syntactic change in the Lingua Franca program is replacing physical con
 
 ```lf
 // Before (Step 2): physical, unordered
-op1.command ~> gm1.in1
-op1.command ~> gm2.in1
+gi1.command ~> gm1.in1
+gi1.command ~> gm2.in1
 
 // After (Step 3): logical, timestamp-ordered
-op1.command -> gm1.in1
-op1.command -> gm2.in1
+gi1.command -> gm1.in1
+gi1.command -> gm2.in1
 ```
 
 This small change has a profound effect: LF now gives both `gm1` and `gm2` the same logical timestamps and a deterministic rule for processing them, provided the coordination assumptions are met.
@@ -46,7 +46,7 @@ This small change has a profound effect: LF now gives both `gm1` and `gm2` the s
 
 See [`src/Step3_Timestamps.lf`](src/Step3_Timestamps.lf). And here is what our system looks like:
 
-![DistributedPowerGrid3 TimeStamped](fig/DistibutedPowerGrid3_TimeStamped.svg)
+![Step 3 timestamped diagram](fig/Step3_Timestamps.svg)
 
 
 Key differences from Step 2:
@@ -108,10 +108,23 @@ For two nodes in California and New York (cross-continental latency ~60–80 ms)
 Tardy events, if not handled, result in messages like this:
 
 ```
-Fed 1 (op2_main): ERROR: STP violation occurred in a trigger to reaction 3, and there is no handler.
+Fed 3 (gm2_main): ERROR: STP violation occurred in a trigger to reaction 1, and there is no handler.
 **** Invoking reaction at the wrong tag!
 ```
 
+To intentionally trigger this error in [`src/Step3_Timestamps.lf`](src/Step3_Timestamps.lf):
+
+1. Temporarily remove the `tardy {= ... =}` block attached to the `GridManager` reaction.
+2. Make both `GridManager` `@maxwait` values very small, for example `@maxwait(1 us)` or `@maxwait(0 ms)`.
+3. Compile and run:
+
+   ```bash
+   lfc src/Step3_Timestamps.lf
+   ./bin/Step3_Timestamps
+   ```
+
+With a very small `maxwait`, a grid manager may advance logical time before an earlier remote message arrives. Without a tardy handler, the runtime reports the STP violation. After observing the error, restore the `tardy` block and return `maxwait` to `100 ms`.
+
 Tardy events may be handled with a **tardy handler**.
 For example, we can add the following to the `GridManager` reaction:
 

04-conservative.md

@@ -100,7 +100,7 @@ This is the CAL theorem in action: **strong consistency costs availability when
 
 See [`src/Step4_Conservative.lf`](src/Step4_Conservative.lf). Here is what our system looks like:
 
-![DistibutedPowerGrid4 Chandy & Misra](fig/DistibutedPowerGrid4_ChandyMisra.svg)
+![Step 4 conservative coordination diagram](fig/Step4_Conservative.svg)
 
 Key changes from Step 3:
 - `GridInterface` is wrapped in `GridServer`, which adds a null-message timer.

05-hybrid.md

@@ -24,7 +24,7 @@ The `GridManager` (from Step 4, with `maxwait = forever`) continues to maintain
 
 And here is what our system looks like:
 
-![DistibutedPowerGrid5 Hybrid](fig/DistibutedPowerGrid5_Hybrid.svg)
+![Step 5 hybrid design diagram](fig/Step5_Hybrid.svg)
 ---
 
 ## The `QuickDispatch` Reactor

README.md

@@ -1,6 +1,6 @@
 # LF Tutorial @ CPS-IoT Week 2026 - Hands-on Session: Logical Time in Distributed Systems: A Power Grid Tutorial
 
-> **Based on:** ["Consistency vs. Availability in Distributed Cyber-Physical Systems" by Lee et al. (2023)](https://arxiv.org/abs/2301.08906)
+> **Based on:** ["Consistency vs. Availability in Distributed Cyber-Physical Systems" by Lee et al. (2023)](https://dl.acm.org/doi/10.1145/3609119)
 > **Domain:** Distributed power grid control using Lingua Franca
 
 ---
@@ -9,7 +9,7 @@
 
 Modern power grids are distributed cyber-physical systems. Generation, transmission, and load are spread across vast geographic areas. Multiple control nodes must coordinate in real time, and they must **agree** on the state of the grid even when separated by hundreds of milliseconds of network latency.
 
-This tutorial takes you through a series of progressively more sophisticated designs for a distributed grid controller, using the [Lingua Franca (LF)](https://lf-lang.org/) coordination language. Each design exposes a new problem and motivates the next solution, culminating in a system that achieves **eventual consistency** while bounding unavailability to a manageable risk.
+This tutorial takes you through a series of progressively more sophisticated designs for a distributed grid controller, using the [Lingua Franca (LF)](https://lf-lang.org/) coordination language. Each design exposes a new problem and motivates the next solution, ending with a hybrid design that separates fast, low-risk commands from slower, strongly consistent decisions.
 
 The design journey mirrors the consistency-vs-availability tradeoff captured by the **CAL theorem**: stronger consistency requires more waiting, more assumptions about latency, or carefully chosen fault handling. Each design makes an explicit, application-specific compromise.
 
@@ -48,9 +48,10 @@ This follows the paper's focus on shared physical state in real-time systems: in
 - **Physical connections** (`~>`) vs **logical connections** (`->`) in LF
 - **Eventual consistency** via ACID 2.0 / CRDTs
 - **Logical timestamps** and the notion of *logical time*
-- **STA** (Safe To Advance) and **STAA** (Safe To Assume Absent) parameters
+- **`maxwait`** as a practical safe-to-advance bound
+- **Tardy handlers** for messages that arrive too late
 - **Conservative coordination** (Chandy-Misra null messages)
-- **The CAL theorem**: Consistency–Availability–Latency tradeoff
+- **The CAL theorem**: consistency, availability, and latency tradeoff
 - **Fault handlers** for bounded unavailability
 
 ---
@@ -60,6 +61,8 @@ This follows the paper's focus on shared physical state in real-time systems: in
 - Basic familiarity with concurrent programming concepts
 - Some exposure to distributed systems (helpful but not required)
 - Lingua Franca installed: see [lf-lang.org](https://lf-lang.org/docs/installation)
+- A C build toolchain and CMake, since the examples use `target C`
+- `tmux` if you want to run federates in separate terminal panes
 
 ---
 
@@ -83,23 +86,44 @@ After creation, clone **your** new repository locally and follow [Running the Co
 
 ## Running the Code
 
-Each `.lf` file in the `src/` directory can be compiled and run with:
+All `.lf` files in this repository are federated LF programs. Compile an example with `lfc`:
 
 ```bash
 lfc src/<filename>.lf
-./bin/<program_name>
 ```
 
-For federated programs (Steps 3 onward), each federate runs as a separate process. The LF compiler generates a launch script:
+For example:
 
 ```bash
-lfc src/<filename>.lf
-./bin/<program_name>_launch.sh
+lfc src/Step1_Actor.lf
+```
+
+Compilation generates a launcher under `bin/` with the same base name as the source file, without the `.lf` extension. For `src/Step1_Actor.lf`, the launcher is:
+
+```bash
+./bin/Step1_Actor
 ```
 
-# References
+That launcher starts the runtime infrastructure (RTI) and all federates for the example. There is no `_launch.sh` script in this repository.
+
+To run a different step, replace the filename and launcher name:
+
+```bash
+lfc src/Step5_Hybrid.lf
+./bin/Step5_Hybrid
+```
+
+The launcher also supports tmux panes, which can make federated output easier to read:
+
+```bash
+./bin/Step1_Actor --tmux
+```
+
+Step 1 exits on its own because it has a short timeout. Other steps may keep running until you stop them with `Ctrl+C` in the launcher or RTI pane.
+
+## References
 
-[1] E. A. Lee, R. Akella, S. Bateni, S. Lin, M. Lohstroh, and C. Menard, "Consistency vs. Availability in Distributed Cyber-Physical Systems," arXiv:2301.08906, 2023. [Online]. Available: https://arxiv.org/abs/2301.08906
+[1] E. A. Lee, R. Akella, S. Bateni, S. Lin, M. Lohstroh, and C. Menard, "Consistency vs. Availability in Distributed Cyber-Physical Systems," arXiv:2301.08906, 2023. [Online]. Available: https://dl.acm.org/doi/10.1145/3609119
 
 [2] T. Zhao, Z. Li and Z. Ding, "Consensus-Based Distributed Optimal Energy Management With Less Communication in a Microgrid," in IEEE Transactions on Industrial Informatics, vol. 15, no. 6, pp. 3356-3367, June 2019, doi: 10.1109/TII.2018.2871562.