TLA+ Generation Demo

Use yichus tla to emit an initial TLA+ model from Bosatsu sources that use Yichus IO primitives.

java -jar yichus.jar tla --name CounterSpec --output counter.tla demos/ui/counter.bosatsu

Example Concurrent Counter Scenario

Two handlers issue read and write operations against the same state. The generated spec exposes these as transitions so TLC can explore competing orderings.

VARIABLES state, listState

Init == /\ state = 0 /\ listState = << >>

Next ==
  \/ /\ state' \in Nat /\ listState' = listState
  \/ /\ UNCHANGED <>

Spec == Init /\ [][Next]_<>