puml-parallel

PlantUML Interface Parallel

A Go tool for composing multiple PlantUML state diagrams in parallel with synchronization events, following CSP (Communicating Sequential Processes) semantics.

Overview

This tool takes multiple Composable State Diagram files and composes them into a single parallel state diagram with specified synchronization events. The composition follows CSP interface parallel semantics.

Installation

Download binaries from Releases.

Usage

$ csdfparallel [--sync event1;event2;...] <file1.puml> [file2.puml] ...

Options

• --sync: Semicolon-separated list of synchronization events for interface parallel

Examples

$ csdfparallel -sync 'insert;showAvailable;showPurchasable;choose;drop' ./examples/user.puml ./examples/vendormachine.puml

Input Format

The tool accepts PlantUML state diagram files in a specific Composable State Diagram format. See the SYNTAX.md and examples/ directory for sample input files.

Inputs may be either .puml text files or .png images generated by PlantUML (plantuml -tpng). For PNG inputs, the embedded source is read from the plantuml text chunk written by PlantUML. The same applies to csdfparse, csdfparallel, csdfevents, csdfrepl, csdfnorm, csdflivelockfree, and csdfreplcmd session new.

csdfparse reads a single diagram. A file argument, a - argument, and stdin are all equivalent:

$ csdfparse diagram.png
$ csdfparse < diagram.png
$ csdfparse - < diagram.png
$ csdfparallel diagram1.png diagram2.puml
$ csdfrepl diagram.png

csdfparse writes one JSON object followed by a newline. Its keys use snake_case, and optional end edges are represented by null when absent. State variables are objects with a name and an optional type. Events are free-form strings.

$ csdfparse < examples/valid/skip.puml
{"states":{"s0":{"id":"s0","name":"SKIP","vars":[]}},"start_edge":{"dst":"s0","post":"true"},"edges":[],"end_edge":{"src":"s0","guard":"true"}}

Normalization

csdfnorm normalizes (determinizes) a single CSDF diagram via subset construction with τ-closure, then prints the result as PlantUML. This is the FDR normal form used as the basis of stable-failures refinement (see REFINEMENT_ALGORITHM.md §4).

$ csdfnorm examples/valid/client.puml
$ csdfnorm < examples/valid/client.puml
$ csdfnorm - < examples/valid/client.puml

Each normal-form state is a set of source states, shown as its label (e.g. "{s0, s1}"). Multiple edges sharing an event are merged into one, with their guards and postconditions combined as a true-aware disjunction. The internal tau event is removed by τ-closure. A file argument, a - argument, and stdin are all equivalent. End edges (state --> [*]) are not currently supported.

Livelock freedom

csdflivelockfree compiles a livelock-freedom proof obligation for a single CSDF diagram and exits 0. Livelock freedom — no divergence: no reachable cycle of internal tau transitions that can actually run forever — depends on the natural-language guards and postconditions, which this tool does not interpret. So rather than decide the verdict via exit status, it emits a proof obligation that leaves each predicate opaque, to be discharged downstream.

The output format is chosen with -target:

• ir-json (default) — a prover-agnostic JSON obligation IR.
• isabelle — an Isabelle/HOL proof-obligation skeleton.
• lean — a Lean 4 proof-obligation skeleton.

$ csdflivelockfree examples/valid/vending_machine.puml
{"structurally":true,"predicates":{...},"states":{...},"constants":[],"edges":[...],"init":{...}}
$ csdflivelockfree -target lean examples/valid/vending_machine.puml
$ csdflivelockfree -target isabelle examples/valid/vending_machine.puml
$ csdfparallel a.puml b.puml | csdflivelockfree -

The JSON IR describes the state space as an ADT (one constructor per state, fields from its variables), the transitions, the initial predicate, and the opaque predicates with their argument signatures. Predicates are deduplicated: predicates is keyed by a hash of the text and the argument types, and an edge names its guard and post by that id, so two transitions carrying the same condition share one entry. structurally is true when no reachable tau cycle exists, in which case the obligation holds regardless of the predicates. Options precede the file; a file argument, a - argument, and stdin are all equivalent.

For the isabelle and lean targets, the skeleton declares the state space as an ADT, an init predicate over the start state's variables, a step relation over every transition, an inductive reachable/Reachable predicate (the start state under init, closed under step), and a tau_step/tauStep relation over the tau transitions only. It then states the livelock-freedom theorem — well-foundedness of the tau relation restricted to the reachable states — left as oops/sorry. The restriction matters: the state ADT also holds valuations the diagram can never enter, and a tau cycle among those would make the unrestricted theorem false even for a diagram that is livelock free. Isabelle uses wf_on {s. reachable s} …; Lean folds Reachable s into the relation instead, which is equivalent because Reachable is closed under step, and keeps the skeleton free of imports. When the diagram is structurally livelock free the obligation is already discharged, so only a note is emitted instead. Each distinct opaque predicate becomes a True placeholder definition named pred_<id> after its hash and preceded by a comment carrying its original natural-language text; every tau transition then gets guard_L<line> and post_L<line> aliases of those placeholders, so a human or LLM can fill in the real predicate body and discharge the proof. Both targets name predicates identically, so the two skeletons can be read side by side. State-variable values are arbitrary JSON, so each variable is typed with a generated val/Val datatype (floats folded into the integer case for now); any declared ; Type annotation is preserved as a comment on the state constructor.

Compiling the obligation IR separately

obligationirc is the same IR compiler as a standalone tool: it reads the JSON IR (from csdflivelockfree, or a file) and compiles it with the same -target values. So these are equivalent:

$ csdflivelockfree -target lean examples/valid/vending_machine.puml
$ csdflivelockfree examples/valid/vending_machine.puml | obligationirc -target lean

This is handy when the IR is produced or stored separately. A file argument, a - argument, and stdin are all equivalent.

Interactive exploration

csdfrepl interactively explores one CSDF file:

$ csdfrepl examples/valid/vending_machine.puml

For each state, enter its variable values as a JSON array in declaration order. The initial implementation records the values but does not evaluate guards or postconditions. JSON null is not accepted.

Commands use zero-based indexes:

• l lists the current state and outgoing transitions.
• t displays the current visible trace. The internal event tau is hidden.
• h displays the exploration history.
• s INDEX selects an outgoing transition.
• j INDEX jumps to a history entry.
• ? or help displays command help.

See CSDFREPL.puml for the behavioral specification.

Headless exploration for agents

csdfrepld is a daemon that holds the same exploration sessions in memory and serves them over a Unix domain socket, and csdfreplcmd is a one-shot client. Together they let a coding agent (or any script) drive exploration without an interactive terminal. The client and daemon speak JSONL, one request per connection.

$ csdfrepld &                                            # listens on $XDG_RUNTIME_DIR/csdfrepld.sock
$ SID=$(csdfreplcmd session new examples/valid/vending_machine.puml)
$ csdfreplcmd read                                       # -s is optional when there is one session
$ csdfreplcmd statevar -json '[0]'                       # enter the current state's values
$ csdfreplcmd select 0                                   # choose a transition, then enter its values
$ csdfreplcmd statevar -json '["done"]'
$ csdfreplcmd trace
$ csdfreplcmd jump 0                                     # branch from an earlier history entry
$ csdfreplcmd read -json                                 # structured output for parsing
$ csdfreplcmd session list
$ csdfreplcmd serverversion                              # the daemon's version
$ csdfreplcmd session rm -s "$SID"

The socket path is shared by both binaries via -sock, then $CSDFREPLD_SOCK, then $XDG_RUNTIME_DIR/csdfrepld.sock, then a temporary directory. Every command prints human-readable text by default and structured JSON with -json; statevar instead takes its values via -json <json-array> or -json-file <file>. Run csdfreplcmd help for the full command list.

Documentation

• Requirements - Project requirements (Japanese)
• Specification - Technical specification (Japanese)
• Syntax - Syntax documentation
• Glossary - Term definitions

License

MIT License