sim_reach
Returns whether the marking to is reachable from the marking from in ONE stored net (a model, or a system that is one net): yes with a firing trace, no with a re-checkable P-invariant (or after an exhaustive search), or unknown with every reason. A sim_compose result is one fused net, so it qualifies; a sim_bind binding or a collection links rates, not tokens, and answers unknown (not-one-net). A system id (sim_create_system) is answered on its one net when one member has every other embedded in it by a witnessed subnetOf or isomorphicTo edge or a chain of edges of one predicate (the answer carries via: an edge and witness per member, or the derivation sim_check_witness(derivation=…) re-checks); otherwise it answers unknown: not-one-net when it holds bindings (they link rates, not tokens) or no member qualifies, system-truncated when its witness bound was reached or the chain search stopped at a bound. On a one-net system, a key in from or to may name a member's place as : (the member's id, or its name when no other member shares it): it is translated into the net place that member's embedding maps it to, the answer's from and to are the translated question, and via.translation lists each key's member, place and net place, which sim_check_witness(reach=…) re-checks against the stored witnesses. Refused, naming the key: a member or place the system does not have, a data place, a key that reads more than one way, a place two valid witnesses of the member's edge map differently, and two keys landing on one net place with different counts; more than 16 other witnesses to compare answers unknown (translation-budget). from is a sparse override on the model's declared initial marking (unset = declared). to constrains only the places it names, each to exactly that count; naming every token place asks for an exact marking. Unknown or data places, negative or fractional counts and counts over the scenario caps (1,000,000 per place, 4,000,000 in total) are refused. Reachability here is untimed: each firing is one atomic step under the shared firing rule (read and inhibitor arcs, capacities, guards decidable from the marking); rates, schedules, delays and stages play no part. Answers: no with a P-invariant y whose weighted sum differs between from and to (when to leaves a place of y free, to alone must already exceed it), valid whatever read arcs, inhibitors, capacities or guards allow, since those only remove firings; no (exhaustive) when every marking reachable from from was searched; yes with a firing trace (shortest among the firings the search makes; reads says when it skipped some); unknown (unknownBecause lists each cause) when neither is found within 100,000 markings or 20,000,000 work units, when a firing would pass 1,000,000 tokens on a place, when a guard fails to evaluate at a reached marking, when a transition whose guard reads action parameters (or does not parse, or whose precondition was lost) was enabled and so left out, when the invariant algebra runs past its 20,000,000-operation budget, is cut short or needs coefficients over 2147483647, or when a found trace would cost the independent checker more than 200,000,000 work units to replay. Unknown is not a no. Every answer (unknown included) is stored: question is the content id of the question as asked (the id, from and to as written, the definition and the budgets), result the id of the answer with what it was computed over (the net, every model, edge and witness via rests on, the predicate registry and system view for a system); a repeated question is served from a per-instance cache with the same bytes, and storedNote says why an answer too large to store (over 262,144 bytes) was not. Public: no sign-in; costs 2 compute tokens (a search plus a store). Re-check a yes or an invariant no with sim_check_witness(reach=), which also re-checks via whole; re-check a stored answer end to end with sim_check_witness(reachResult=) or GET /api/lineage/.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| to | Yes | JSON object of the places to constrain, each to exactly that count, e.g. {"done": 1}. On a system, a key may be <model>:<place> for a member's place, translated into the net's | |
| from | No | JSON object of place -> whole token count overriding the declared initial marking, e.g. {"queue": 3}; unset = the declared marking. On a system, a key may be <model>:<place> for a member's place | |
| system | Yes | content id of one stored model, or of a system (sim_create_system) |