sim_distinguish
Compare the behaviour of two stored models of one process — typically a net formalized from a document and a net sim_code_to_flow read out of code — and return proved (no word of visible steps separates them), refuted (with separation: the shortest firing sequence one net can make and the other cannot, or after which only one can stop) or unknown. Definition corresponded-traces-v1: correspondence maps subject transitions one-to-one to object transitions (unset: every transition id the two share); each mapped pair is a visible label, and every transition left out is hidden on its own side and closed over, so an internal step the code takes that the document does not name is not a difference. With outcomes (default true) it also compares where each net can stop (a marking where no transition, hidden ones included, is enabled), reading the observed places correspondence.places maps (unset: none, so it compares only whether each can stop); set outcomes=false for nets meant to run forever, such as a server loop. Untimed and interleaving through the shared firing rule: rates, delays and schedules are not compared; a guard, a precondition the net's source carried and it could not represent (guardUnrepresentable, as sim_code_to_flow can leave), a fixed delay, or two consuming arcs from one place into one transition make the answer unknown (nothing is compared). Budgets: 20,000,000 work units, 4,096 joint states, 4,096 markings per side after one word, 262,144 markings held across every joint state kept, 4,096 steps in a run, 1,000,000 tokens per place; the whole call is also bounded by the 55 s request limit. A budget that runs out answers unknown, with agreesThroughLength once the empty word was compared (no word of at most that many labels separates them), and never counts as agreement; retrying gives the same answer. A refuted answer's separation was re-checked by pkg/morphism before it was returned; pass it back as separation, with nothing else, to re-check it against both stored models now, with no search (valid, invalid, or uncheckable: a model was deleted, a net carries a guard, a lost precondition or a fixed delay, the separation names another definition, or the check is over the checker's bounds). A proved answer carries no certificate. Every answer carries means: a refutation shows the two NETS differ; whether the document and the code differ, or a formalization or the correspondence is wrong, the engine does not decide; a proof is agreement between two readings, not fidelity. Unlike sim_prove's refines (one direction, by id, no hidden steps, recorded), it is symmetric and records nothing; unlike sim_diff (the text of two models), it compares behaviour. Needs sign-in (opens OAuth the first time). Costs 2 compute tokens to compare, 1 to re-check a separation. Writes nothing.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| object | No | content id of the other stored model, e.g. the net sim_code_to_flow made from the code | |
| subject | No | content id of one stored model, e.g. the net formalized from the document | |
| outcomes | No | also compare where each net can stop (default true); false for nets meant to run forever | |
| separation | No | a refuted sim_distinguish answer's separation, the object exactly as returned (or that object as a string): {"subject", "object", "witness"}; re-checked with no search. Give it alone | |
| correspondence | No | JSON (an object, or a string holding one): {"transitions": {"<subject transition>": "<object transition>", …}, "places": {"<subject token place>": "<object token place>", …}}, each one-to-one; places optional (the observed places, read where a net stops). Unset: transitions matched by identical id, no observed places. At most 65,536 bytes |