LTSVisualizer

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.

Ways to use LTSVisualizer

Online

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/

Offline

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:

1. Download LTSVisualizer.html and SHA256SUMS.txt.
2. Optionally verify the checksum as described below.
3. Double-click LTSVisualizer.html, or use Open with and select a modern browser.
4. Open a local JSON graph from the application.

No installation, local server, Node.js, or Python runtime is required.

Verify an offline release

On Windows PowerShell:

Get-FileHash .\LTSVisualizer.html -Algorithm SHA256
Get-Content .\SHA256SUMS.txt

The calculated hash must match the hash recorded for LTSVisualizer.html.

Features

JSON graph input

• Open .json LTS 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 nodes and edges.
• Reopen selected-path JSON exports as regular graphs.
• Preserve transition labels and colors such as darkorange or #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.

Graph exploration

• 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.

Inspection

• 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.

Graph analysis

• 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.

Bounded alternative path search

• Open the Paths tab and choose Shortest paths or Any witness (fast).
• Use Shortest paths to compute up to a user-defined number of paths in deterministic shortest-first order.
• Use Any witness (fast) to compute up to a user-defined number of satisfying paths in deterministic heuristic discovery order; these paths are not guaranteed to be shortest.
• Any-witness priority is generic and favors candidates with more accepting constraints, more exercised constraints, and more monitors advanced from their initial state before using path length and insertion order as tie-breakers.
• Set Visits per state to 1 for loopless paths or to a higher value to allow bounded revisits and self-loops.
• 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.
• Use reverse shortest-distance guidance from a fixed target for shortest-path search and generic Declare-monitor progress for Any-witness search.
• 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.

Data-aware Declare-constrained path search

• Add one or more Declare constraints to bounded path search.
• Enable or disable individual constraints without deleting their configuration.
• Match activation and target events by transition name and structured transition data.
• Build transition pickers and data-field choices from the currently loaded graph.
• Evaluate transition inputs and outputs during search rather than only matching transition labels.
• Combine multiple conditions within one predicate using AND semantics.
• Use string, number, boolean, and null comparison values.
• Use exists and does-not-exist without 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.
• Capture values from qualifying activation events and correlate them with structured target data.
• Search either toward a required target state or for a constraint-satisfying path without a fixed target.
• Optionally require every applicable enabled constraint to be exercised, excluding paths that satisfy only vacuously.
• Apply exercise checking consistently to target-specific and target-free searches.
• Run constrained searches in the existing path-search worker with cancellation, stale-result protection, bounded revisits, parallel-edge identity, and a choice between deterministic shortest-first search and deterministic any-witness heuristic discovery.
• 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. Vacuous satisfaction remains part of Declare semantics; Require constraints to be exercised can be used when returned paths must demonstrate participating constraint events.

Supported Declare templates

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
• Past: Precedence, Not precedence, Chain precedence, Not chain precedence, Alternate precedence
• Bidirectional: Succession, Not succession, Chain succession, Not chain succession, Alternate succession

The 27 supported templates determine which predicate roles are required. Cardinality templates require a non-negative count. Templates that support correlation can relate data captured by an activation to data on a target.

The positive Alternate family follows standard Declare/MP-Declare semantics:

• Alternate response: every qualifying activation must receive a correlated later target before another qualifying activation occurs.
• Alternate precedence: every qualifying target must have a correlated activation since the previous qualifying target.
• Alternate succession: both Alternate response and Alternate precedence must hold.

Unrelated transitions are allowed between the paired events. A transition with the same name interrupts alternation only when it also satisfies the relevant data predicate. Alternate templates use two operands; there is no third between predicate.

Transition-data conditions

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 index n.

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.

Path explanations

Each accepted constrained path can show Why this path satisfies the constraints. Explanations include:

• The constraint ID and template.
• A satisfaction summary.
• Whether the constraint was exercised or satisfied vacuously.
• Supporting transition events with one-based path steps, transition names, and exact edge IDs.
• Clickable evidence that focuses the corresponding transition and opens its data in the Inspector.

Constraint monitors remain authoritative for path pruning and acceptance. Explanation evidence is reconstructed only after a path has been accepted, avoiding explanation histories on every queued search candidate.

Persisted Declare search configuration

Complete-graph JSON exports preserve:

• Configured Declare constraints and their enabled state.
• Nested transition-data conditions, activation captures, and target correlations.
• Source state, endpoint mode, and selected search strategy.
• Optional target state.
• Requested path count and maximum visits per state.
• The Require constraints to be exercised setting.

Reopening the exported graph restores the configuration. Computed paths and explanations are intentionally not persisted; rerunning the search reconstructs them from the restored graph and constraint specification. Selected-path JSON exports preserve the configured Declare constraints but do not persist computed explanation results.

Manual path selection

• 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

• 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.

Sample data

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

JSON input format

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 }
        ]
      }
    }
  ]
}

Node fields

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 }
    ]
  }
}

Edge fields

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": null means output information was not supplied.
• "outputs": {} means the supplied output flow is known to be empty.
• The same distinction applies to outputs_raw: null means 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.

Lightweight graph documents

The format envelope is optional when importing JSON:

{
  "nodes": [
    { "id": "0" },
    { "id": "1" }
  ],
  "edges": [
    {
      "id": "edge-1",
      "source": "0",
      "target": "1",
      "transition": "Continue"
    }
  ]
}

Selected-path JSON format

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.

Using the dashboard

Use the side panel

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:

• ArrowLeft widens the panel by 16 pixels.
• ArrowRight narrows the panel by 16 pixels.
• Hold Shift with an arrow key to resize by 50 pixels.
• Home selects the minimum width.
• End selects the maximum allowed by the current viewport.

Open a graph

1. Open the online application or LTSVisualizer.html.
2. Select Open LTS Graph File.
3. Choose a .json graph file.
4. Wait for validation and rendering to complete.

Graph data remains in the browser and is not uploaded to a server.

Explore a graph

1. Enter a state ID to focus on that state.
2. Use 1 hop, 2 hops, or 3 hops to control neighborhood depth.
3. Use Show all to display the complete graph.
4. Switch between Hierarchical and Grid layouts.
5. Toggle transition labels for readability and performance.
6. Hover over a graph element to inspect its semantic data.
7. Select a state or transition to pin its inspector data.
8. Drag states to adjust positions.
9. Drag the background to pan.
10. Use the mouse wheel to zoom.

For very large graphs, neighborhood exploration is recommended instead of displaying every state and transition simultaneously.

Analyze a graph

1. Open the Analysis tab in the right-hand panel.
2. Select Run analysis. Loading a graph or opening the tab does not start computation.
3. Select Cancel if the analysis should be stopped.
4. Review the terminal-state and cyclic-component summary.
5. Expand Terminal states to filter and select a terminal state.
6. Expand Cyclic components to filter by minimum size and select a component.
7. Select Clear component view to return to normal neighborhood exploration.
8. 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.

Find alternative paths

1. Open the Paths tab.
2. Enter source and target state IDs.
3. Select Shortest paths for deterministic shortest-first results, or Any witness (fast) for heuristic discovery without a shortestness guarantee.
4. Choose the requested number of paths. Both strategies respect this value.
5. Set Visits per state to 1 for loopless paths or higher for bounded revisits and self-loops.
6. Select Find paths. During a running search, the action changes to Cancel.
7. Select a result to display it without relaying out its states.
8. Expand Show transition details to compare transition names, state pairs, and edge IDs.
9. Select a transition name or edge ID to center and select its edge, or select a state ID to center and select its state.
10. Use Export .puml or Export .json to export the displayed computed path.
11. Select Return to graph view to restore the prior graph context without clearing results.

Shortest-path results are ordered by transition count. Any-witness results are ordered by generic constraint-progress priority and are not guaranteed to be shortest. In both strategies, paths are unique by ordered edge IDs. If source and target are equal, the zero-transition path is valid.

Find Declare-constrained paths

1. Open the Paths tab.
2. Enter the source state ID.
3. 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.
4. Select Shortest paths or Any witness (fast).
5. Choose the requested number of paths and set Visits per state. Any-witness mode may find an initial satisfying path much sooner, while requesting additional witnesses can require substantially more search.
6. In the Declare constraints section, select Add constraint.
7. Choose a Declare template and configure its required activation and, where applicable, target transition.
8. 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.
9. Configure activation captures and target correlation when events must refer to the same data item.
10. Add further conditions or constraints as needed. Conditions within a predicate and enabled constraints in the search are combined conjunctively.
11. Enable Require constraints to be exercised when vacuously satisfied paths should be excluded.
12. Select Find paths. Invalid or incomplete constraints are reported before search starts.
13. Expand Why this path satisfies the constraints to inspect the evidence, or select a result to visualize and 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.

Interpreting optional-target results

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.

Some Declare templates are satisfied vacuously when no qualifying activation occurs. When Require constraints to be exercised is enabled, every applicable enabled constraint must participate in the returned path. This rule applies both with and without a target state. When the option is disabled, shorter vacuously satisfying paths may enter the top-K results and displace longer exercised paths because results remain ordered by transition count.

Select a path

1. Search for or focus the desired starting state.
2. Select Select path.
3. 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.

Export behavior

Export a selected path as JSON

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.

Export a selected path as PlantUML

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.

Export the complete graph as JSON

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, graph counts, configured Declare constraints, and path-search settings. Its filename is derived safely from the opened JSON filename. Computed search results and explanations are not persisted.

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.

Architecture

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 and Declare-constrained path search
        |   |-- Incremental Declare monitors and exercise tracking
        |   |-- Accepted-path explanation replay
        |   `-- 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/dist for static web hosting and GitHub Pages.
• The single-file build in frontend/dist-offline for a double-clickable offline LTSVisualizer.html release.

Technology stack

• React
• TypeScript
• Vite
• Cytoscape.js
• Vitest
• Oxlint
• vite-plugin-singlefile
• GitHub Actions
• GitHub Pages

Project structure

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/

Developer prerequisites

• Node.js 22 or newer
• npm
• Git

Set up the project

git clone https://github.com/dbera/LTSVisualizer.git
cd LTSVisualizer/frontend
npm install

For deterministic CI and release builds, use npm ci when node_modules is absent and package-lock.json is current.

Run in development mode

From frontend:

npm run dev

Open the URL printed by Vite, normally http://localhost:5173.

Development checks

From frontend:

npm test
npm run lint
npm run build
npm run build:offline

The 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, generic any-witness ordering, multiple witnesses, requested-count handling, reverse-distance pruning, resource safeguards, Declare constraint validation and monitor semantics, standard Alternate semantics, exercise enforcement for targeted and target-free searches, accepted-path explanations, persisted Declare/search configuration, 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.

Build targets

Static web build

From frontend:

npm run build

Output:

frontend/dist/

This build uses the /LTSVisualizer/ base path for GitHub Pages.

Offline single-file build

From frontend:

npm run build:offline

Output:

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 Actions

Continuous integration

.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 Pages

.github/workflows/pages.yml builds frontend/dist, uploads the Pages artifact, and deploys the static site from main.

Offline HTML release

.github/workflows/release.yml runs manually or when a tag matching v* is pushed. It:

1. Installs frontend dependencies.
2. Runs tests and linting.
3. Builds the offline single-file application.
4. Renames the output to LTSVisualizer.html.
5. Generates SHA256SUMS.txt.
6. Uploads both files as a workflow artifact.
7. Publishes both files to a GitHub Release for tag-triggered runs.

Publish a release

1. Update CHANGELOG.md and user-facing documentation.
2. Run all frontend checks.
3. Manually run Build offline HTML release and verify the downloaded file through a file:/// URL.
4. Commit and push release changes to main.
5. Wait for continuous integration to pass.
6. Synchronize the local branch:

git switch main
git pull origin main
git status

7. Create and push an annotated version tag:

git tag -a v0.6.0 -m "LTSVisualizer 0.6.0"
git push origin v0.6.0

The tag triggers the offline HTML release workflow and publishes LTSVisualizer.html and SHA256SUMS.txt to the corresponding GitHub Release.

Current limitations

• 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.
• Any-witness results are heuristic discoveries rather than shortest-path guarantees. Requesting additional witnesses can substantially increase search time and memory use.
• 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.
• LTSVisualizer currently implements control-flow and data-aware Declare semantics, but not MP-Declare quantitative time intervals.
• Explanation evidence is generated for accepted paths and is intended to support inspection; some templates may receive richer family-specific evidence in future releases.
• 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.

Roadmap

Potential future improvements include:

• Additional constraint combinations and richer Boolean grouping
• Reusable constraint presets independent of graph JSON documents
• Richer family-specific explanation evidence and diagnostics
• Quantitative time conditions inspired by MP-Declare
• 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

Contributing

Contributions, bug reports, and feature suggestions are welcome. See CONTRIBUTING.md for development and pull-request guidelines.

Security

Do not disclose security vulnerabilities through public GitHub issues. See SECURITY.md for the reporting process.

License

This project is licensed under the MIT License. See LICENSE for details.

Author

Debjyoti Bera

Project repository: https://github.com/dbera/LTSVisualizer