{"actions":{"bootstrapAndRun":{"effect":"installs rote if missing, inspects, prepares, and asks before running","href":"https://play.modiqo.ai/install?play=himanshu-jha/state-machine-liveness-proof@0.1.0","method":"GET","rel":"https://rote.dev/rels/bootstrap-and-run","requiresConsent":true,"responseMediaType":"text/x-shellscript"},"inspect":{"command":"rote play inspect https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0","effect":"read-only"},"installCliOnly":{"effect":"installs the rote CLI, nothing else","href":"https://play.modiqo.ai/install","method":"GET","rel":"https://rote.dev/rels/install-cli","requiresConsent":true,"responseMediaType":"text/x-shellscript"},"run":{"command":"rote play run https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0","effect":"executes the play locally after consent","headless":{"approvalAssertion":"--yes","approvalRequiredBeforeInvocation":true,"commandTemplate":"rote play run https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0 <name=value...> --yes","stdinPolicy":"never pipe input to automate the interactive Ready selector"},"requiresConsent":true}},"description":"Checks a bounded finite JSON state machine for more than syntactic validity: it proves reachability, computes strongly connected components, identifies reachable states with no path to a terminal, and emits a prefix-plus-cycle counterexample for closed livelocks or possible starvation. Four independent graph probes feed a join that distinguishes a proof failure from an incomplete run. It is useful for queue workers, workflow engines, payment states and reconciliation loops before implementation. The contract caps models at 500 states and 5,000 transitions, rejects string-coerced fairness and duplicate edges, and makes terminal semantics explicit: halting by default or reachability goal. Guards remain labels unless callers expand them into states, so the play does not pretend to model arbitrary program semantics.","distribution":{"digest":"sha256:d090afdcdab5dc2048d82bb861676c4ef1d04d20b3d8278d116c0edf5948dc09","mediaType":"application/vnd.modiqo.rote-flow","size":9245,"verifiedBy":"rote verifies the downloaded archive against this digest before it runs"},"effects":{"credentialsProvidedBy":"runner","credentialsRemainLocal":true,"declaredWrites":[],"publisherReceivesCredentials":false},"id":"https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0","inputPolicy":{"optionalWithDefault":"show_default_and_accept_override","optionalWithoutDefault":"omit_unless_supplied","required":"ask","secrets":"collect_locally_outside_conversation"},"license":"MIT","links":{"docs":"https://rote.dev","page":"https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0","protocol":"https://play.modiqo.ai/.well-known/rote","self":"https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0.json"},"name":"state-machine-liveness-proof","owner":{"kind":"org","slug":"himanshu-jha"},"parameters":[{"description":"JSON containing states, initial, terminal_states, and labeled transitions. Empty uses the packaged counterexample model; missing or malformed custom input is fatal.","example":"./worker-state-machine.json","input":{"allowCustom":true,"choices":[],"label":"Input"},"name":"input","required":false,"type":"string"}],"preparation":[{"action":{"command":"rote play inspect https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0 --json","effect":"read-only"},"step":1,"type":"inspect_local_readiness"},{"references":["/parameters"],"step":2,"type":"collect_parameters"},{"references":["/parameters","/requirements","/effects"],"step":3,"type":"review"},{"consentBoundary":"the user approves the exact play and parameter values","references":["/parameters","/requirements","/effects"],"step":4,"type":"obtain_run_consent"},{"action":{"command":"rote play run https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0","headlessCommandTemplate":"rote play run https://play.modiqo.ai/himanshu-jha/state-machine-liveness-proof@0.1.0 <name=value...> --yes"},"preservesAcquisitionBoundaries":["adapter_selection","oauth_dcr","google_discovery","static_token_setup","runtime_security_checks"],"requiresConsent":true,"step":5,"type":"run"}],"producedBy":{"roteVersion":"0.79.0"},"publishedAt":"2026-09-04T07:58:17.125721+00:00","reference":"himanshu-jha/state-machine-liveness-proof@0.1.0","requirements":{"adapters":[],"browser":{"dependencies":[],"runtime":false,"signIn":false},"localTools":["python3"],"roteCli":{"minimumVersion":"0.62.0"},"sessions":false},"resolution":"pinned","schema":"rote.play.v1","stats":{"downloads":1,"installs":0},"steps":{"count":5,"names":["compute_reachability","decompose_strong_components","prove_machine_liveness","search_livelock_counterexamples","validate_machine_contract"]},"title":"state-machine-liveness-proof","type":"play","version":"0.1.0","visibility":"public"}