state-model-checker
State Machine Model Checker — Returns PASS, FAIL or INCONCLUSIVE for a finite state machine, protocol, or concurrent routine, with the shortest failing path as readable process.transition steps and a next step. Accepts a formal spec (no LLM), a plain-language workflow, or source code (translated to a spec by an LLM, with every transition quoted from the source and two independent translations compared). A pure TypeScript expli
Tool call template
This tool declares no required parameters. Add optional parameters from the input schema as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {},
"name": "state-model-checker"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| code | No | Source code of a state machine, protocol, or concurrent routine; translated to a spec by an LLM, with each transition carrying its verbatim source span. | |
| spec | No | Formal spec (zero LLM calls). {vars:{name:{type:'bool'|'int'|'enum'|'array',min,max,values,size|keys,of,init}}, processes:[{name,instances?,fairness?:'none'|'weak'|'strong',transitions:[{name,guard?,updates:[{var,at?,value}]}]}], initWhere?, terminal?, progress?, invariants:[{name,expr}], liveness:[{name,kind:'eventually'|'alwaysEventually'|'leadsTo',p,q?}]}. Expressions are JSON nodes ({var,at?}, {sym}, {param}, {op,args}, forall/exists) or infix strings such as "pc[self] == wait && !flag[1 - self]"; nothing is evaluated as code. | |
| options | No | ||
| properties | No | Properties to check, in plain language (with description or code only). | |
| description | No | Natural-language workflow or protocol; translated to a spec by an LLM, with each transition quoted from the text. |