sim_verify
Verify declared properties of a stored model: a report with one verdict per property, proved, refuted or unknown (unknown is never a pass, and ok is true only when every property is proved), with evidence for a proof and a counterexample for a refutation, plus caveats naming anything the analysis net could not express. Unset properties check bounded and deadlock-free. Every check starts from the model's own initial marking. Each verdict's method says how far it reaches. structural: from the incidence matrix, with no state search. A structural bounded holds for every initial marking (every place is covered by a P-invariant), and so does a structural conserves (the token total is a P-invariant). A structural invariant or mutual-exclusion verdict rests on a P-invariant's value at this initial marking (its evidence names the P-invariant and the value), so it holds from this marking and from any other that gives that P-invariant the same value, not from every marking: two workers sharing one lock token are proved mutually exclusive, and the same net with two lock tokens is refuted. exhaustive: every state reachable from this initial marking. witness: a firing sequence found by targeted search, decisive for this initial marking (a cycle that grows a place without bound). partial: the search was truncated, so only a refutation is sound. vacuity holds one reading per verdict, in the same order, decided by the engine. proved-vacuously: a proved unreachable whose target needs a token on a place never marked from the initial marking, a proved invariant or mutual-exclusion whose places are all never marked, a proved mutual-exclusion whose marked places never hold more than the bound on their own (so they never compete), or a proved bounded, terminating or conserves when no transition can fire at all (deadlock-free is then refuted); neverMarked names the never-marked places the claim reads and deadTransitions the transitions that would mark them, which never fire. not-vacuous: each place the claim reads (for unreachable, each place its target asks a token on) that neverMarked does not list is marked at some reachable marking the search found; a listed place adds nothing, and a target that asks for no token is not-vacuous without a search. method says what decided it: structural (the arcs alone) or exhaustive (sim_reach's search of the model under its firing rule, evaluating the guards that read only the marking, up to 20000 markings or 20000000 work units). unknown is open, never a no: the search stopped at a bound, skipped a firing the model may make (a guard over action parameters, a lost precondition), or did not run (the model declares a delay, which a one-step search misreads), or a kind with no antecedent has only guarded transitions to fire; it may still list neverMarked. not-applicable: a verdict other than proved, a proved live or reachable (each rests on a firing sequence), or a kind with no antecedent where some transition can fire. ok, the counts and every verdict do not read vacuity: a proved-vacuously verdict still counts as proved. To ask about another starting marking, store the model with that marking (sim_extend's set_initial) and verify it. Read the Verification properties section of sim://docs/authoring for each kind's fields. Free (no compute token); writes nothing.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| id | Yes | model id | |
| properties | No | JSON array of properties, each a kind plus the fields that kind reads: deadlock-free, bounded, live, terminating and conserves read none; reachable and unreachable read target (place → token count; places it leaves out are unconstrained); invariant reads expr (a linear relation over place ids, "a + 2*b <= 10"); mutual-exclusion reads places and bound (the token counts of places sum to at most bound at every reachable marking, default 1; for places that each hold at most one token, at most bound of them are marked at once). Any property may carry a name. E.g. [{"kind":"deadlock-free"},{"kind":"mutual-exclusion","places":["win_x","win_o"]},{"kind":"invariant","expr":"a + 2*b == 10"}]. Unset checks bounded and deadlock-free. An unknown kind or field, a field the kind does not read, a missing one, a negative target count, a bound of 0 or less, or a place named twice in places (the counts are summed, so a repeat would count that place twice) is refused with every reason at once, each with the likely meaning; a field sent as null is left out. A place id in places, target or expr that the model does not have is refused too, naming it with the place id it most likely meant, and so is a data place, which holds a value rather than a count; either is refused rather than answered unknown. |