ltl-analyze

The commands are under static analysis. This page is the module.

npm install --save-dev @rhysbalevicius/ltl-analyze

The four analyses

Each opens and closes a solver session around the call, except verify, which needs none.


`vacuity(spec, options?)`	Rules that pass for the wrong reasons.
`consistency(spec, options?)`	Whether the rules can hold together.
`witness(spec, ruleId, options?)`	The shortest trace that breaks one rule while the others hold.
`verify(spec, workflow)`	Rules against a declared graph. Synchronous.
`RunOptions`	`{ horizon }`.

Report
`VacuityReport`	`Finding`s, each `unsatisfiable`, `never-fires` or `implied`.
`ConsistencyReport`	`{ consistent, conflict?, witness? }`.
`WitnessReport`	The trace, or why there is none.
`VerifyReport`	`VerifyFinding`s, including out-of-scope rules.
`Finding`, `VerifyFinding`, `Witness`	The entries those carry.

Underneath


`analyzeVacuity`, `analyzeConsistency`, `synthesizeWitness`	The same analyses, taking a solver rather than opening one.
`verifyWorkflow(spec, source)`	What `verify` calls.
`withSolver(work)`	Opens a session, runs the work, closes it.
`openSolver()`	`{ solve, close }`. The session owns worker threads: a process that forgets `close` will not exit.
`SolverUnavailable`	Thrown when the solver cannot start. Also exported as `SolverError`.
`Z3Session`	What `openSolver` returns.
`AnalyzeOptions`	`{ solver, horizon }`.
`info`, `AnalyzeInfo`	The capability probe the CLI reads after its dynamic import, so an older binary can say what a newer package offers.

Encoding


`encode(spec, options)`	A rule set into constraints.
`decode(assignment, alphabet)`	A satisfying assignment back into events.
`horizonFor(spec)`	The bound, sized from the widest window the rules declare.
`alphabetOf(spec)`	The events the rules can distinguish.
`Encoding`, `Alphabet`, `FieldAlphabet`	Those types.
`Problem`, `Declarations`, `Term`, `Assignment`	The solver-independent constraint IR.
`evaluate(problem, assignment)`	The IR under an assignment, which is how a candidate is checked before it is reported.
`solveByEnumeration(problem)`	A reference solver, used to test the real one.
`Solver`, `Verdict`	The solver interface.

Graphs and CTL


`skeletonOf(source)`, `Skeleton`	The step structure a declaration determines.
`pathsOf(skeleton)`	Every step order it permits.
`traceOf(path)`	One of those as real events, which is what gets replayed.
`checkCtl(graph, formula)`	A quantified rule against a graph.
`labelGraph(graph, props)`	The graph with propositions attached to states.
`containsExistential(f)`	Whether a result rests on a possibilistic claim.
`CtlReport`, `CtlResult`, `CtlWitness`	What `checkCtl` returns, including the path or lasso.
`GraphSource`	A workflow, or a graph supplied directly.
`PAYLOAD_MATCHER_MESSAGE`, `CUSTOM_PREDICATE_MESSAGE`, `linearOperatorMessage`	What the CTL fragment says when it refuses something, so a report explains rather than declines.

The soundness stance is worth reading before trusting any of this: universal verdicts are sound, existential ones are possibilistic, and the reports label which is which.