STLmc / workspace

Signal Temporal Logic ยท Model checking

Local connection

Disconnected

Start stlmc-gui on your computer and paste the session token from its terminal. No solver or model is uploaded to this website.

Advanced connection settings

Disconnected. Tokens are kept in memory only.

File watch starts after connecting.

Verification workspace

Model & configuration

Model editor

Not saved

Configuration editor

Not saved

Analysis settings

Advanced options

Connect to read STLmc settings.

Values come from STLmc's default and loaded configuration. Only edited fields override it. Wall-clock timeout is a separate workspace limit; visualization is enabled for workspace runs.

Ready to run

Results apply to the selected bounds and robustness threshold, not an unbounded proof. dReal precision is a separate setting.

Analysis output

Bound progress

No analysis selected

Completed bounds appear as soon as their result is available. Encoding and solver work before the first completed bound do not produce a row.

Select or start an analysis to inspect its results.

Raw progress events