LTSVisualizer is a browser-based application for exploring, analyzing, and searching large labelled transition systems and reachability graphs stored as JSON. It supports ordinary bounded path search and data-aware constrained path discovery using Declare templates.
It was created primarily for reachability graphs generated from Colored Petri Nets, where:
- Nodes represent markings or states.
- Edges represent fired transitions.
- Transition inputs describe data consumed by a transition.
- Transition outputs describe tokens produced by a transition, grouped by output place.
- State markings describe the distribution of tokens across Petri-net places.
The application is implemented with React, TypeScript, Vite, and Cytoscape.js. Graph files are parsed and validated locally in the browser. LTSVisualizer has no backend, sends no graph data to a server, and requires no Python installation.
LTSVisualizer supports small linear graphs and large cyclic state spaces containing thousands of states and transitions.
The repository contains a GitHub Pages deployment workflow for the static application. When the deployment is available, the application is served at:
https://dbera.github.io/LTSVisualizer/
Download LTSVisualizer.html from a GitHub Release or from the artifact of a manually triggered Build offline HTML release workflow.
The file is self-contained and can be opened directly in a modern browser:
- Download
LTSVisualizer.htmlandSHA256SUMS.txt. - Optionally verify the checksum as described below.
- Double-click
LTSVisualizer.html, or use Open with and select a modern browser. - Open a local JSON graph from the application.
No installation, local server, Node.js, or Python runtime is required.
On Windows PowerShell:
Get-FileHash .\LTSVisualizer.html -Algorithm SHA256
Get-Content .\SHA256SUMS.txtThe calculated hash must match the hash recorded for LTSVisualizer.html.
- Open
.jsonLTS graph files directly in the browser. - Validate document structure, node IDs, edge IDs, source and target references, semantic fields, and saved paths.
- Accept complete LTSVisualizer graph documents and lightweight documents containing
nodesandedges. - Reopen selected-path JSON exports as regular graphs.
- Preserve transition labels and colors such as
darkorangeor#darkorange. - Preserve structured and raw state markings.
- Preserve structured and raw transition inputs and outputs.
- Distinguish parallel transitions using unique edge IDs.
LTSVisualizer does not import PlantUML files. PlantUML remains available only as an export format for selected paths.
- Search for a state by ID.
- Explore one-, two-, or three-hop neighborhoods around a focused state.
- Display the complete graph with Show all.
- Switch between hierarchical and grid layouts.
- Show or hide transition labels.
- Pan, zoom, select, and manually reposition states.
- Use a lightweight full-graph overview for large state spaces.
- Inspect state markings by hovering over or selecting states.
- Inspect consumed inputs and produced outputs by hovering over or selecting transitions.
- Inspect structured and raw semantic data through an expandable JSON viewer.
- Expand or collapse nested data and copy inspector data as JSON.
- Pin inspector content while continuing to explore the graph.
- Clear pinned inspector content without clearing a selected path.
- Open the Analysis tab without affecting the Inspector.
- Run analysis explicitly with Run analysis. Analysis is never started automatically when a graph is loaded.
- Detect terminal states, defined as states with no outgoing transitions.
- Compute strongly connected components using an iterative graph traversal that avoids recursive call-stack limits.
- Classify an SCC as cyclic when it contains more than one state or when a singleton state has a self-loop.
- Run graph analysis in an inline Web Worker so the browser interface remains responsive.
- Cancel an analysis while it is running.
- Ignore stale worker results after cancellation, reruns, or loading another graph.
- Filter terminal states by state ID and browse large result sets in pages of 100.
- Select a terminal state to open its current neighborhood view.
- Filter cyclic components by minimum component size and browse results in pages of 100.
- Select one cyclic component to display only its member states and internal transitions.
- Clear a component-only view and return to normal neighborhood exploration.
- Use the same analysis functionality in the hosted application and the offline
file:///build.
A terminal state is not automatically an error. Whether a terminal state represents successful completion or an unintended deadlock depends on the model. LTSVisualizer reports terminal states and does not attempt to classify their business meaning.
Analysis results are held in browser memory for the currently loaded graph. They are reset when another graph is opened and are not added to graph or selected-path exports.
- Open the Paths tab to compute up to a user-defined number of shortest paths between two states.
- Set Visits per state to
1for loopless paths or to a higher value to allow bounded revisits. - Support equal source and target states. The zero-transition path is returned first, and returning cycles may follow when the visit bound permits them.
- Treat paths as unique by ordered edge-ID sequence, so parallel transitions remain distinct even when they connect the same states.
- Order results by increasing transition count, with deterministic ordering for equal-length alternatives.
- Use reverse shortest-distance guidance from the target to prioritize reachable alternatives and prune states that cannot reach the target.
- Run searches in an inline Web Worker with cancellation, stale-result protection, errors, reruns, and reset when another graph is loaded.
- Stop safely at internal candidate safeguards and report partial results without claiming that no additional paths exist.
- Select a result to reuse existing path visualization and JSON and PlantUML exports.
- Separate parallel transitions visually and expose transition names, source and target states, and exact edge IDs.
- Select transition or state details to center and select the corresponding graph element without leaving the Paths tab.
- Pin clicked transition or state data for later viewing in Inspector without switching tabs automatically.
- Preserve search results while switching among Inspector, Analysis, and Paths.
- Fit the viewport around a computed path without changing node positions.
- Use Return to graph view to restore visible elements, positions, zoom, pan, focus, neighborhood depth, and layout while retaining results.
- Use the same functionality in hosted and offline
file:///builds.
Path-search results are kept in browser memory for the currently loaded graph and are reset when another graph is opened.
- Add one or more Declare constraints to bounded path search.
- Enable or disable individual constraints without deleting their configuration.
- Match activation, target, and where applicable between events by transition name and structured transition data.
- Build transition pickers and data-field choices from the currently loaded graph.
- Evaluate transition
inputsandoutputsduring search rather than only matching transition labels. - Combine multiple conditions within one predicate using AND semantics.
- Use string, number, boolean, and
nullcomparison values. - Use
existsanddoes-not-existwithout supplying a comparison value. - Traverse nested objects, arrays of objects, and arrays of primitive values.
- Configure every array level independently as an existential item match (
[*]) or a fixed zero-based index such as[2]. - Combine existential and indexed traversal at arbitrary multidimensional depth.
- Search either toward a required target state or for a constraint-satisfying path without a fixed target.
- Run constrained searches in the existing path-search worker with cancellation, stale-result protection, bounded revisits, deterministic shortest-first results, and parallel-edge identity.
- Use the same constrained-search functionality in hosted and offline
file:///builds.
All enabled constraints must be satisfied by a returned path. Disabling a constraint excludes it from evaluation but keeps it available for later reuse.
The constraint builder groups templates by purpose:
- Cardinality: At least N, At most N, Exactly N, Exactly N consecutively
- Position: Init, End
- Choice: Choice, Exclusive choice
- Existence: Responded existence, Not responded existence, Coexistence, Not coexistence
- Future: Response, Not response, Chain response, Not chain response, Alternate response, Not alternate response
- Past: Precedence, Not precedence, Chain precedence, Not chain precedence, Alternate precedence, Not alternate precedence
- Bidirectional: Succession, Not succession, Chain succession, Not chain succession, Alternate succession, Not alternate succession
The selected template determines which predicate roles are required. Cardinality templates require a non-negative count. Alternate templates also expose a between predicate. Templates that support correlation can relate data captured by an activation to data on a target.
A condition starts at either inputs or outputs and follows a path through the structured transition data. The available fields and observed scalar types are derived from occurrences of the selected transition in the loaded graph.
Examples:
inputs.request.priority
outputs.result.status
outputs.orders[*].items[2].status
outputs.matrix[1][3].value
outputs.tensor[*].rows[2].cells[*].enabled
Array access is configured per level:
[*]means that at least one item at that level must satisfy the remaining condition.[n]selects the item at zero-based indexn.
For example, outputs.tensor[*].rows[2].cells[*].enabled matches any tensor item whose third row contains a cell with a matching enabled value.
Existence operators test whether the configured path can be resolved. Other operators compare the resolved value with the typed value configured in the editor.
- Start a path from the currently focused state.
- Extend a path by selecting a highlighted successor state.
- Select an exact edge through Choose next transition.
- Distinguish parallel and identically named transitions by edge ID.
- Support loops, repeated states, and repeated edge traversals.
- Undo the most recent transition.
- Restart or clear the selected path.
- Preserve graph zoom, pan, and manually adjusted state positions while constructing a path.
- Export the complete loaded graph as JSON, independently of the visible neighborhood or selected path.
- Export a selected path as a self-contained JSON document.
- Export a selected path as PlantUML.
- Preserve exact transition order, loops, repeated traversals, and parallel-edge identity.
- Preserve state markings, transition inputs, transition outputs, raw semantic values, labels, and colors.
The repository includes:
sample-data/example.json: a small graph for quick checks.sample-data/rg_imaging.json: a larger, realistic reachability graph.sample-data/synthetic.json: a synthetic graph for terminal-state and strongly connected component analysis.
The expected analysis for synthetic.json is:
States: 32
Transitions: 41
Terminal states: 4
Cyclic components: 5
States in cyclic components: 19
Largest cyclic component: 8
Cyclic component sizes: 8, 5, 3, 2, 1
A complete LTSVisualizer graph document has explicit nodes and edges:
{
"format": "ltsvisualizer",
"version": 1,
"type": "graph",
"metadata": {
"title": "Example reachability graph"
},
"nodes": [
{
"id": "0",
"marking_raw": null,
"marking": {
"input": [
{ "id": 42 }
]
}
},
{
"id": "1",
"marking_raw": null,
"marking": {
"processing": [
{ "id": 42 }
]
}
}
],
"edges": [
{
"id": "edge-17",
"source": "0",
"target": "1",
"transition": "StartProcessing",
"color": "darkorange",
"inputs_raw": null,
"inputs": {
"request": { "id": 42 }
},
"outputs_raw": null,
"outputs": {
"processing": [
{ "id": 42 }
]
}
}
]
}Each node contains:
id: unique state identifier.marking: optional structured state marking.marking_raw: optional original marking text.
Example:
{
"id": "42",
"marking_raw": null,
"marking": {
"requests": [
{ "id": 100 }
]
}
}Each edge contains:
id: unique edge identifier.source: source node ID.target: target node ID.transition: transition name.color: optional transition color.inputs: optional structured transition-input bindings.inputs_raw: optional original transition-input text.outputs: optional structured transition-output flow. Each key is an output place and each value is an array of produced tokens.outputs_raw: optional original transition-output text.
Example:
{
"id": "edge-42",
"source": "10",
"target": "11",
"transition": "ProcessRequest",
"color": null,
"inputs_raw": null,
"inputs": {
"request": { "id": 100 }
},
"outputs_raw": "{completed={'{\"id\": 100}'}}",
"outputs": {
"completed": [
{ "id": 100 }
]
}
}The edge ID identifies the exact edge. Connectivity is represented separately by source and target, allowing parallel edges even when source, target, and transition name are identical.
outputs represents the tokens produced by the transition firing, not the complete target-state marking. Token order and duplicate occurrences are preserved.
Missing and explicitly empty output data have different meanings:
"outputs": nullmeans output information was not supplied."outputs": {}means the supplied output flow is known to be empty.- The same distinction applies to
outputs_raw:nullmeans unavailable, while"{}"represents a known empty raw output flow.
Older JSON files that omit outputs and outputs_raw remain supported. Missing optional semantic fields are normalized to null.
The format envelope is optional when importing JSON:
{
"nodes": [
{ "id": "0" },
{ "id": "1" }
],
"edges": [
{
"id": "edge-1",
"source": "0",
"target": "1",
"transition": "Continue"
}
]
}A selected-path export contains a self-contained graph subset and an ordered path:
{
"format": "ltsvisualizer",
"version": 1,
"type": "selected-path",
"metadata": {
"title": "Selected path 0 to 3",
"startStateId": "0",
"endStateId": "3",
"stateCount": 4,
"transitionCount": 3
},
"nodes": [
{
"id": "0",
"marking_raw": null,
"marking": null
},
{
"id": "1",
"marking_raw": null,
"marking": null
}
],
"edges": [
{
"id": "edge-1",
"source": "0",
"target": "1",
"transition": "Start",
"color": null,
"inputs_raw": null,
"inputs": null,
"outputs_raw": null,
"outputs": null
}
],
"path": {
"startNodeId": "0",
"edgeIds": ["edge-1"]
}
}The nodes and edges arrays describe unique graph elements. The ordered path.edgeIds array describes the exact traversal and preserves:
- Transition order
- Parallel-edge identity
- Repeated transitions
- Loops
- Repeated state occurrences
For example, the traversal 0 -> 1 -> 0 -> 1 contains four state occurrences and three transition steps, even if its graph subset contains only two unique states and two unique edges.
When a selected-path JSON file is reopened, LTSVisualizer loads its graph subset as a regular graph. Search, neighborhoods, layouts, labels, and Show all remain available.
The right-hand side panel contains the Inspector, Analysis, and Paths tabs.
- Drag the vertical separator to resize the panel.
- Use the collapse control to hide or restore the panel.
- The selected width and collapsed state are saved in browser local storage.
- Collapsing the panel does not discard path-search results or condition-editor state.
When the separator has keyboard focus:
ArrowLeftwidens the panel by 16 pixels.ArrowRightnarrows the panel by 16 pixels.- Hold
Shiftwith an arrow key to resize by 50 pixels. Homeselects the minimum width.Endselects the maximum allowed by the current viewport.
- Open the online application or
LTSVisualizer.html. - Select Open LTS Graph File.
- Choose a
.jsongraph file. - Wait for validation and rendering to complete.
Graph data remains in the browser and is not uploaded to a server.
- Enter a state ID to focus on that state.
- Use 1 hop, 2 hops, or 3 hops to control neighborhood depth.
- Use Show all to display the complete graph.
- Switch between Hierarchical and Grid layouts.
- Toggle transition labels for readability and performance.
- Hover over a graph element to inspect its semantic data.
- Select a state or transition to pin its inspector data.
- Drag states to adjust positions.
- Drag the background to pan.
- Use the mouse wheel to zoom.
For very large graphs, neighborhood exploration is recommended instead of displaying every state and transition simultaneously.
- Open the Analysis tab in the right-hand panel.
- Select Run analysis. Loading a graph or opening the tab does not start computation.
- Select Cancel if the analysis should be stopped.
- Review the terminal-state and cyclic-component summary.
- Expand Terminal states to filter and select a terminal state.
- Expand Cyclic components to filter by minimum size and select a component.
- Select Clear component view to return to normal neighborhood exploration.
- Select Run again to recompute the results for the current graph.
For large graphs, worker execution prevents the analysis algorithm from blocking the main browser interface. Preparing and transferring graph topology still consumes browser memory, so analysis remains an explicit user action.
- Open the Paths tab.
- Enter source and target state IDs.
- Choose the requested number of paths.
- Set Visits per state to
1for loopless paths or higher for bounded revisits. - Select Find paths. During a running search, the action changes to Cancel.
- Select a result to display it without relaying out its states.
- Expand Show transition details to compare transition names, state pairs, and edge IDs.
- Select a transition name or edge ID to center and select its edge, or select a state ID to center and select its state.
- Use Export .puml or Export .json to export the displayed computed path.
- Select Return to graph view to restore the prior graph context without clearing results.
Paths are ordered by transition count and are unique by ordered edge IDs. If source and target are equal, the zero-transition path is valid.
- Open the Paths tab.
- Enter the source state ID.
- Enter a target state ID when the path must end at a particular state, or leave the target empty to search for a constraint-satisfying path without a fixed destination.
- Choose the requested number of paths and set Visits per state.
- In the Declare constraints section, select Add constraint.
- Choose a Declare template and configure its required activation, target, and where applicable between transitions.
- For a transition-data predicate, select Add condition, choose an input or output field, configure each array-access level, select an operator, and provide a typed value when required.
- Add further conditions or constraints as needed. Conditions within a predicate and enabled constraints in the search are combined conjunctively.
- Select Find paths. Invalid or incomplete constraints are reported before search starts.
- Select a result to visualize, inspect, or export it using the normal computed-path controls.
Use the enable control to temporarily exclude a constraint while preserving its configuration. Changing a constraint invalidates earlier search results because those results were computed under a different search specification.
With a target state, a result must reach that state and satisfy every enabled constraint when the path is completed.
Without a target state, the search may return a path as soon as the enabled monitors consider the path complete and accepting. This is useful when the required behavior matters more than a particular destination state.
- Search for or focus the desired starting state.
- Select Select path.
- Extend the path by selecting a highlighted successor state or an exact edge under Choose next transition.
Path colors are:
- Green: path start
- Blue: selected path
- Orange: current endpoint
- Cyan: available next states and transitions
Use Choose next transition when multiple or parallel transitions lead to the same state, when transitions have identical names, or when an edge is difficult to select directly.
Selecting a transition back to an earlier state creates a loop. It does not rewind the traversal.
- Undo removes the most recently selected transition.
- Restart path discards the current traversal and starts a new selection.
- Clear path exits path-selection mode.
- The Inspector's clear action only unpins inspector content.
The JSON path export preserves:
- Unique graph nodes and edges
- Exact ordered edge IDs
- Loops and repeated traversals
- Parallel-edge identity
- State markings
- Transition inputs and outputs
- Raw markings, inputs, and outputs
- Transition labels and colors
Exported selected-path JSON files can be reopened as regular graphs.
The PlantUML export preserves selected states and transitions, transition order, labels, colors, state markings, transition inputs, and transition outputs.
When output information is available, the export includes a machine-readable comment:
'Transition Outputs: {completed={'{"id": 100}'}}A known empty output flow is exported as:
'Transition Outputs: {}The output comment is omitted when output information is unavailable.
PlantUML files exported by LTSVisualizer are intended for PlantUML-compatible tools. LTSVisualizer itself does not import PlantUML files.
Select Export graph JSON to export every state and transition in the loaded graph. The export is independent of:
- The visible neighborhood
- The focused state
- Whether Show all is active
- The selected path
The export preserves all unique states and transitions, parallel edges, semantic data, labels, colors, and graph counts. Its filename is derived safely from the opened JSON filename.
A complete graph export has document type graph and includes counts in its metadata:
{
"format": "ltsvisualizer",
"version": 1,
"type": "graph",
"metadata": {
"title": "Example graph",
"stateCount": 1000,
"transitionCount": 2500
},
"nodes": [],
"edges": []
}The document contains the complete graph held in memory, not only the elements currently rendered by Cytoscape.js.
Local JSON graph file
|
v
React and TypeScript application
|
|-- JSON parsing and validation
|-- Cytoscape.js visualization
|-- Search and neighborhood exploration
|-- Structured semantic-data inspection
|-- On-demand terminal-state and SCC analysis
| `-- Inline Web Worker with cancellation
|-- Bounded alternative path search
| `-- Reverse-distance-guided inline Web Worker with cancellation
|-- Manual path selection
|-- Complete-graph JSON export
|-- Selected-path JSON export
`-- Selected-path PlantUML export
All graph processing occurs in the browser. There is no application backend or API.
Two production build targets are maintained:
- The standard Vite build in
frontend/distfor static web hosting and GitHub Pages. - The single-file build in
frontend/dist-offlinefor a double-clickable offlineLTSVisualizer.htmlrelease.
- React
- TypeScript
- Vite
- Cytoscape.js
- Vitest
- Oxlint
- vite-plugin-singlefile
- GitHub Actions
- GitHub Pages
LTSVisualizer/
|-- .github/
| |-- dependabot.yml
| |-- ISSUE_TEMPLATE/
| |-- pull_request_template.md
| `-- workflows/
| |-- ci.yml
| |-- pages.yml
| `-- release.yml
|-- frontend/
| |-- public/
| |-- src/
| | |-- components/
| | |-- graph/
| | |-- workers/
| | |-- App.css
| | |-- App.tsx
| | |-- index.css
| | `-- main.tsx
| |-- index.html
| |-- package.json
| |-- package-lock.json
| |-- vite.config.ts
| `-- vite.offline.config.ts
|-- sample-data/
| |-- example.json
| |-- rg_imaging.json
| `-- synthetic.json
|-- CHANGELOG.md
|-- CONTRIBUTING.md
|-- LICENSE
|-- README.md
`-- SECURITY.md
Generated directories are intentionally ignored by Git:
frontend/dist/
frontend/dist-offline/
- Node.js 22 or newer
- npm
- Git
git clone https://github.com/dbera/LTSVisualizer.git
cd LTSVisualizer/frontend
npm installFor deterministic CI and release builds, use npm ci when node_modules is absent and package-lock.json is current.
From frontend:
npm run devOpen the URL printed by Vite, normally http://localhost:5173.
From frontend:
npm test
npm run lint
npm run build
npm run build:offlineThe current test suite covers JSON validation and round trips, graph serialization, complete-graph export, manual and computed path selection, loops, repeated states, bounded revisits, source-equals-target paths, self-loops, parallel edges, deterministic shortest-first ordering, reverse-distance pruning, resource safeguards, Declare constraint validation and monitor semantics, transition-data predicates and correlation, optional-target constrained search, nested and multidimensional array conditions, typed condition values, side-panel state, selected-path export, semantic data, PlantUML path export, terminal-state detection, iterative SCC computation, large synthetic graph topologies, and worker-controller lifecycle behavior.
From frontend:
npm run buildOutput:
frontend/dist/
This build uses the /LTSVisualizer/ base path for GitHub Pages.
From frontend:
npm run build:offlineOutput:
frontend/dist-offline/index.html
For release distribution, the workflow renames the file to LTSVisualizer.html and generates SHA256SUMS.txt.
The offline configuration disables copying frontend/public and removes the external favicon reference so the release contains no required external assets.
.github/workflows/ci.yml runs frontend checks on pushes and pull requests. It installs dependencies, runs tests, runs linting, and builds the standard frontend.
.github/workflows/pages.yml builds frontend/dist, uploads the Pages artifact, and deploys the static site from main.
.github/workflows/release.yml runs manually or when a tag matching v* is pushed. It:
- Installs frontend dependencies.
- Runs tests and linting.
- Builds the offline single-file application.
- Renames the output to
LTSVisualizer.html. - Generates
SHA256SUMS.txt. - Uploads both files as a workflow artifact.
- Publishes both files to a GitHub Release for tag-triggered runs.
- Update
CHANGELOG.mdand user-facing documentation. - Run all frontend checks.
- Manually run Build offline HTML release and verify the downloaded file through a
file:///URL. - Commit and push release changes to
main. - Wait for continuous integration to pass.
- Synchronize the local branch:
git switch main
git pull origin main
git status- Create and push an annotated version tag:
git tag -a v0.4.0 -m "LTSVisualizer 0.4.0"
git push origin v0.4.0The tag triggers the offline HTML release workflow and publishes LTSVisualizer.html and SHA256SUMS.txt to the corresponding GitHub Release.
- Only JSON graph input is supported.
- PlantUML is an export-only format.
- Extremely large full-graph views can be visually dense even when rendering remains responsive.
- Global force-directed layouts are intentionally avoided because they can be computationally expensive in the browser.
- Terminal states are reported topologically and are not classified as successful completions or definite deadlocks.
- Graph analysis uses a worker and is user-triggered, but very large graphs still require additional browser memory for topology transfer and analysis results.
- Bounded path search is user-triggered and uses a worker, but highly connected graphs can still reach internal candidate safeguards before every requested alternative is found. Partial results are reported and additional valid paths may exist.
- Cancelling path search terminates its worker immediately; partial paths found before cancellation are not retained.
- Declare constraints are evaluated during bounded path search; configured visit and result limits still determine the explored search space.
- Multiple conditions within a predicate and multiple enabled constraints are currently combined conjunctively.
- Transition-data fields are inferred from data present on occurrences of the selected transition. A field absent from the loaded graph cannot be selected through the graph-aware field picker.
- The offline release depends on browser support for local
file:///applications and file selection. - GitHub Pages availability depends on successful processing by GitHub's deployment service.
Potential future improvements include:
- Additional constraint combinations and richer Boolean grouping
- Import and export of reusable constraint configurations
- Further correlation editing for captured activation data
- Additional path-search diagnostics and progress reporting
- Performance tuning for highly connected constrained-search spaces
- More graph layouts and large-graph navigation aids
- Additional export formats
Contributions, bug reports, and feature suggestions are welcome. See CONTRIBUTING.md for development and pull-request guidelines.
Do not disclose security vulnerabilities through public GitHub issues. See SECURITY.md for the reporting process.
This project is licensed under the MIT License. See LICENSE for details.
Debjyoti Bera
Project repository: https://github.com/dbera/LTSVisualizer