puml-parallel

README

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 verifies that a single CSDF diagram is livelock free, i.e. has no divergence: no cycle reachable from the start state consisting entirely of internal tau transitions. The analysis is purely structural over event labels; natural-language guards and postconditions are not evaluated, so a diagram with no tau edges is trivially livelock free.

$ csdflivelockfree examples/valid/vending_machine.puml
livelock free
$ csdfparallel a.puml b.puml | csdflivelockfree -

When the diagram is livelock free it prints livelock free and exits 0. Otherwise it prints a witness — the path from the start state into the offending tau cycle, followed by the cycle itself — and exits non-zero. 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