Interactive Concept Demo

ConTiNGENT-Style State Explorer

This page is a lightweight front-end demonstration inspired by TLC. It does not run the real model checker, but it simulates a small nondeterministic ReLiANT state space and draws the explored states live as the run unfolds, including repeated loops and alternate paths.

Workflow Summary

Concept View

This mock shows a simplified ReLiANT lifecycle, starting from a loaded formal model and ending in a replayable run.

Spec Loaded

The model is available and ready to explore.

Trace Generated

A possible behavior trace is produced from the model.

Review Needed

The trace may need refinement before translation.

Commands Mapped

Trace steps are converted into command-level intent.

Safe To Execute

Guardrails confirm the correct test device and run mode.

Run Complete

The system finishes with logs and replayable artifacts.

State Flow

Idle

The base diagram shows the available states. Running the demo adds live transitions and nondeterministic loops.

Unique States 0

Transitions 0

Invariant Status Idle

Trace exists before execution Waiting

Commands mapped before run Waiting

Safe test device selected Waiting