Merge pull request #2 from lf-lang/refine

Improve clarify of the tutorial materials and add CI test.

Author: hokeun

.github/workflows/lf-ci.yml

@@ -0,0 +1,84 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - main
+      - "releases/*"
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  check-compile-and-run:
+    name: Compile and run LF examples
+    runs-on: ubuntu-24.04
+
+    steps:
+      - name: Check out repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Set up Java 17
+        run: |
+          echo "$JAVA_HOME_17_X64/bin" >> "$GITHUB_PATH"
+          echo "JAVA_HOME=$JAVA_HOME_17_X64" >> "$GITHUB_ENV"
+        shell: bash
+
+      - name: Install C build dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y build-essential cmake
+
+      - 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"
+
+      - name: Smoke-run generated LF programs
+        shell: bash
+        run: |
+          set -euo pipefail
+
+          shopt -s nullglob
+          lf_files=(src/*.lf)
+
+          if (( ${#lf_files[@]} == 0 )); then
+            echo "No .lf files found under src/."
+            exit 1
+          fi
+
+          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
+              runner="$executable"
+            else
+              echo "No generated executable or launch script found for $file."
+              exit 1
+            fi
+
+            echo "::group::Run $runner"
+            set +e
+            timeout --kill-after=5s 10s "$runner"
+            status=$?
+            set -e
+
+            if [[ "$status" -ne 0 && "$status" -ne 124 && "$status" -ne 137 ]]; then
+              echo "$runner failed with exit code $status."
+              exit "$status"
+            fi
+
+            if [[ "$status" -eq 124 || "$status" -eq 137 ]]; then
+              echo "$runner ran until the smoke-test timeout, as expected for a reactive example."
+            fi
+            echo "::endgroup::"
+          done

.gitignore

@@ -0,0 +1,2 @@
+bin/*
+fed-gen/*

01-actor-model.md

@@ -1,8 +1,8 @@
-# Step 1: The Actor Model — Commutative Grid Dispatch
+# Step 1: The Actor Model: Commutative Grid Dispatch
 
 ## The Problem We're Solving
 
-Two control centers — one in California, one in New York — each manage a portion of the national grid. Both maintain a copy of the **grid balance**: a signed integer representing net generation in megawatts (positive = excess, negative = deficit).
+Two control centers, one in California and one in New York, each manage a portion of the national grid. Both maintain a copy of the **grid balance**: a signed integer representing net generation in megawatts (positive = excess, negative = deficit).
 
 Operators at either location can issue dispatch commands:
 - **Dispatch up**: bring more generation online (+MW)
@@ -29,7 +29,7 @@ The squiggly arrows (`~>`) are **physical connections** in Lingua Franca: they u
 
 ## The Code
 
-See [`src/DistibutedPowerGrid1_Actor.lf`](src/DistibutedPowerGrid1_Actor.lf).
+See [`src/Step1_Actor.lf`](src/Step1_Actor.lf).
 
 The core reactor is `SimpleGridManager`:
 
@@ -80,9 +80,9 @@ Each grid manager receives commands from **both** operators and keeps its own co
 
 ---
 
-## Why This Works — Sometimes
+## 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.
+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.
 
 This means that even though `gm1` and `gm2` may process the same two commands in different orders, they will eventually agree on the same balance. This property is called **eventual consistency**.
 
@@ -92,15 +92,15 @@ More formally, this design satisfies **ACID 2.0** properties (Helland & Campbell
 - **I**dempotent: TCP guarantees exactly-once delivery, so each command is applied exactly once
 - **D**istributed: state is maintained at multiple nodes
 
-A datatype with these properties is called a **Conflict-Free Replicated Datatype (CRDT)** — one of the simplest CRDTs in existence.
+A datatype with these properties is called a **Conflict-Free Replicated Datatype (CRDT)**. This example is one of the simplest CRDTs in existence.
 
 ---
 
 ## The Catch
 
-This design would allow operators to curtail generation far below zero — a dangerous grid imbalance that could trip protective relays and cause a cascading blackout. 
+This design would allow operators to curtail generation far below zero, creating a dangerous grid imbalance that could trip protective relays and cause a cascading blackout.
 
-Any **business logic** that enforces limits (e.g., "don't curtail if balance is already at its minimum threshold") breaks commutativity — and with it, our consistency guarantees.
+Any **business logic** that enforces limits (e.g., "don't curtail if balance is already at its minimum threshold") breaks commutativity. That also breaks the consistency guarantee from this simple CRDT-style design.
 
 That's what we explore next.
 
@@ -112,8 +112,8 @@ That's what we explore next.
 
 2. What would happen if TCP delivery were *not* guaranteed? How would the ACID 2.0 / CRDT properties need to change?
 
-3. Why does the CAL theorem (Consistency vs. Availability under Latency constraints) apply here? What is the partial order? [[More Reading]](https://arxiv.org/abs/2301.08906)
+3. Now consider the potential effect of network delays in this example. How would network delays affect the consistency of this example?
 
 ---
 
-**Next:** [Step 2 — When Operations Are Non-Commutative](02-inconsistency.md)
+**Next:** [Step 2: When Operations Are Non-Commutative](02-inconsistency.md)

02-inconsistency.md

@@ -1,4 +1,4 @@
-# Step 2: When Operations Are Non-Commutative — The Consistency Problem
+# Step 2: When Operations Are Non-Commutative: The Consistency Problem
 
 ## Adding Real Business Logic
 
@@ -10,7 +10,7 @@ Real grid operators enforce **safety constraints**. A typical rule:
 >
 > If a curtailment would push the balance below the threshold, reject it and log an **imbalance event** (which triggers automated protective relays in a real system).
 
-Let's say our minimum safe threshold is **−200 MW**. Here is the updated reactor (See [`src/DistibutedPowerGrid2_Inconsistency.lf`](src/DistibutedPowerGrid2_Inconsistency.lf)).
+Let's say our minimum safe threshold is **−200 MW**. Here is the updated reactor (See [`src/Step2_Inconsistency.lf`](src/Step2_Inconsistency.lf)).
 
 
 ```lf
@@ -59,17 +59,17 @@ This new operation is **not commutative**. The result of applying two commands d
 - California: curtail −80 MW (would bring balance to −230 MW, below threshold)
 - New York: dispatch +100 MW (would bring balance to −50 MW)
 
-**Scenario A — California manager sees curtail first:**
+**Scenario A: California manager sees curtail first:**
 1. California curtail (−80): `−150 + (−80) = −230`. Below threshold → **rejected**.
 2. New York dispatch (+100): `−150 + 100 = −50`. Applied.
 3. Final balance at `gm1`: **−50 MW**. No imbalance event.
 
-**Scenario B — California manager sees dispatch first:**
+**Scenario B: California manager sees dispatch first:**
 1. New York dispatch (+100): `−150 + 100 = −50`. Applied.
 2. California curtail (−80): `−50 + (−80) = −130`. Above threshold → **applied**.
 3. Final balance at `gm1`: **−130 MW**. No imbalance event.
 
-Since `gm1` and `gm2` receive these messages over physical (unordered) connections, they may each experience a different scenario. **They permanently disagree on the balance** — and worse, they may disagree on whether an imbalance event occurred.
+Since `gm1` and `gm2` receive these messages over physical (unordered) connections, they may each experience a different scenario. **They permanently disagree on the balance**, and worse, they may disagree on whether an imbalance event occurred.
 
 This is the fundamental consistency problem in distributed systems.
 
@@ -90,14 +90,14 @@ New York node:                   dispatch +100 ───────────
                                                                                      ↓
                                                                            gm2 final: -50 MW ✓ no event
 
-But gm1 (-130) ≠ gm2 (-50) — INCONSISTENT STATE!
+But gm1 (-130) ≠ gm2 (-50): 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.
 
 ---
 
-## Fixing It — The Options
+## Fixing It: The Options
 
 We'll explore three approaches to fix the inconsistency issue:
 
@@ -121,4 +121,4 @@ The single-node approach defeats the purpose of having two control centers. So w
 
 ---
 
-**Next:** [Step 3 — Adding Logical Timestamps](03-timestamps.md)
+**Next:** [Step 3: Adding Logical Timestamps](03-timestamps.md)

03-timestamps.md

@@ -1,19 +1,19 @@
-# Step 3: Logical Timestamps — Ordering Events Across the Grid
+# Step 3: Logical Timestamps: Ordering Events Across the Grid
 
 ## The Core Insight
 
-When a California operator curtails generation at the same physical instant that a New York operator dispatches generation, there is no objective "ground truth" about which happened first. Special relativity tells us the ordering can depend on the observer — and for events separated by thousands of kilometers, the difference in light travel time is measurable.
+When a California operator curtails generation at the same physical instant that a New York operator dispatches generation, there is no objective "ground truth" about which happened first. Special relativity tells us the ordering can depend on the observer, and for events separated by thousands of kilometers, the difference in light travel time is measurable.
 
-Fortunately, we don't need ground truth. We just need **both control nodes to agree on the same ordering** — and for that ordering to look reasonable to human operators. Logical timestamps achieve exactly this.
+Fortunately, we don't need ground truth. We need **both control nodes to agree on the same ordering**, and for that ordering to look reasonable to human operators. Logical timestamps achieve exactly this.
 
 ---
 
 ## What Is Logical Time?
 
-Lingua Franca assigns a **timestamp** to every message at the point it is created. In a federated (distributed) program, each node uses its **local physical clock** to assign timestamps. Clock synchronization protocols like NTP, PTP, or GPS ensure that these clocks are close to each other — within a bounded error `ε`.
+Lingua Franca assigns a **timestamp** to every message at the point it is created. In a federated (distributed) program, each node uses its **local physical clock** to assign timestamps. Clock synchronization protocols like NTP, PTP, or GPS keep these clocks close to each other, within a bounded error `ε`.
 
 A timestamp becomes a **logical time** because:
-- When Node A sends a message with timestamp `t`, Node B processes it at logical time `t` — even if Node B's physical clock has already advanced past `t`.
+- When Node A sends a message with timestamp `t`, Node B processes it at logical time `t`, even if Node B's physical clock has already advanced past `t`.
 - Logical time is a shared reference frame that both nodes agree on, independent of physical clock drift.
 
 ---
@@ -38,21 +38,21 @@ op1.command -> gm1.in1
 op1.command -> gm2.in1
 ```
 
-This small change has a profound effect: LF now **guarantees** that both `gm1` and `gm2` handle every pair of commands in the same logical time order.
+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.
 
 ---
 
 ## Code
 
-See [`src/DistibutedPowerGrid3_TimeStamped.lf`](src/DistibutedPowerGrid3_TimeStamped.lf). And here is what our system looks like:
+See [`src/Step3_Timestamps.lf`](src/Step3_Timestamps.lf). And here is what our system looks like:
 
 ![DistributedPowerGrid3 TimeStamped](fig/DistibutedPowerGrid3_TimeStamped.svg)
 
 
 Key differences from Step 2:
 1. Connections use `->` instead of `~>`
 2. `GridManager` has a `maxwait` attribute
-3. No other changes to the reactor logic — timestamp ordering is handled by the LF runtime
+3. No other changes to the reactor logic; timestamp ordering is handled by the LF runtime
 
 ---
 
@@ -73,7 +73,7 @@ reaction(in1, in2) -> out {=
 =}
 ```
 
-Because the connection wiring is symmetric (California always feeds `in1`, New York always feeds `in2` at both managers), both managers give priority to the California operator at simultaneous timestamps. This is a deterministic policy — not the most fair one, but a consistent one.
+Because the connection wiring is symmetric (California always feeds `in1`, New York always feeds `in2` at both managers), both managers give priority to the California operator at simultaneous timestamps. This is a deterministic policy. It may not be the fairest policy, but it is consistent.
 
 ---
 
@@ -151,11 +151,11 @@ If it is OK for these reports to be made late, then we can annotate the reaction
 
 ## The CAL Theorem
 
-The waiting introduced by timestamps is not a bug — it is **fundamental**. The **CAL theorem** ([Lee et al., 2023](https://doi.org/10.1145/3609119)) states:
+The waiting introduced by timestamps is not a bug; it is **fundamental**. The **CAL theorem** ([Lee et al., 2023](https://doi.org/10.1145/3609119)) states:
 
 > It is impossible to achieve consistency without paying a price in **availability**, where the price is proportional to the latencies in the system.
 
-"Availability" here means: how long must an operator wait before their dispatch command takes effect? The longer the `maxwait`, the more consistent the system — and the longer operators wait. We'll return to this in Step 6.
+"Availability" here means: how long must an operator wait before their dispatch command takes effect? A larger `maxwait` can tolerate larger apparent latency, but operators may wait longer. We'll return to this in Step 6.
 
 ---
 
@@ -169,4 +169,4 @@ The waiting introduced by timestamps is not a bug — it is **fundamental**. The
 
 ---
 
-**Next:** [Step 4 — Conservative Coordination with Null Messages](04-conservative.md)
+**Next:** [Step 4: Conservative Coordination with Null Messages](04-conservative.md)

04-conservative.md

@@ -1,4 +1,4 @@
-# Step 4: Conservative Coordination — Chandy-Misra with Null Messages
+# Step 4: Conservative Coordination: Chandy-Misra with Null Messages
 
 ## The Problem with Finite maxwait
 
@@ -33,17 +33,17 @@ LF supports this method via `maxwait = forever`:
   gm1 = new GridManager()
 ```
 
-With `maxwait = forever`, the grid manager will wait **indefinitely** — until it receives positive evidence from the remote node that no message with tag ≤ `g` is coming.
+With `maxwait = forever`, the grid manager will wait **indefinitely** until it receives positive evidence from the remote node that no message with tag ≤ `g` is coming.
 
 Of course, waiting forever sounds like a bad idea.
-What if the remote `GridInterface` 
-How does that evidence arrive? That's where **null messages** come in.
+What if the remote `GridInterface` has no real commands to send?
+How does the evidence arrive? That's where **null messages** come in.
 
 ---
 
 ## Null Messages
 
-In our grid, commands are sent only when operators issue dispatches or curtailments. If California issues no commands for 10 minutes, New York's manager has no evidence about California's timeline — and blocks forever under `maxwait = forever`.
+In our grid, commands are sent only when operators issue dispatches or curtailments. If California issues no commands for 10 minutes, New York's manager has no evidence about California's timeline and blocks forever under `maxwait = forever`.
 
 The fix: California's node sends **null messages** periodically. A null message says:
 
@@ -78,7 +78,7 @@ reactor GridServer(null_message_period: time = 1 s) {
 }
 ```
 
-The timer fires every second. If no real command has arrived, a `0` is forwarded — which the grid manager interprets as "no change." This lets the grid manager advance its logical time by at least 1 second per second, bounding the wait.
+The timer fires every second. If no real command has arrived, a `0` is forwarded, which the grid manager interprets as "no change." This lets the grid manager advance its logical time by at least 1 second per second, bounding the wait.
 
 ---
 
@@ -89,7 +89,7 @@ The timer fires every second. If no real command has arrived, a `0` is forwarded
 - **Bounded wait**: the maximum wait is ~1 second (the null message period) plus network latency.
 
 **What you give up:**
-- **Availability under failure**: if the California `GridServer` crashes, it stops sending null messages. New York's manager blocks indefinitely — it cannot advance time because it has no proof that California won't send a message.
+- **Availability under failure**: if the California `GridServer` crashes, it stops sending null messages. New York's manager blocks indefinitely because it has no proof that California won't send a message.
 - **Network overhead**: null messages are sent every second even when there are no real commands. For a grid with hundreds of nodes, this multiplies.
 
 This is the CAL theorem in action: **strong consistency costs availability when network behavior is unbounded**.
@@ -98,9 +98,7 @@ This is the CAL theorem in action: **strong consistency costs availability when
 
 ## Code
 
-See [`src/DistibutedPowerGrid4_ChandyMisra.lf`](src/DistibutedPowerGrid4_ChandyMisra.lf). And here is what our system looks like:
-
-And here is what our system looks like:
+See [`src/Step4_Conservative.lf`](src/Step4_Conservative.lf). Here is what our system looks like:
 
 ![DistibutedPowerGrid4 Chandy & Misra](fig/DistibutedPowerGrid4_ChandyMisra.svg)
 
@@ -121,4 +119,4 @@ Key changes from Step 3:
 
 ---
 
-**Next:** [Step 5 — Hybrid Design: Fast-Path for Safe Commands](05-hybrid.md)
+**Next:** [Step 5: Hybrid Design: Fast-Path for Safe Commands](05-hybrid.md)