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

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 + 2b <= 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 + 2b == 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.

Name

Required

Description

Default

id

Yes

model id

properties

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.

Previous value: -"JSON array of properties, e.g. [{\"kind\":\"deadlock-free\"},{\"kind\":\"mutual-exclusion\",\"places\":[\"win_x\",\"win_o\"]},{\"kind\":\"invariant\",\"expr\":\"a + 2*b == 10\"}]. Default: bounded + deadlock-free."New value: +"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."

whatif

Input Schema

Schema Changelog

TDQS

Glama MCP Gateway

Resources