is_realizable
Checks whether a GR(1) assume-guarantee contract is realizable by deciding if component outputs can satisfy guarantees for every environment satisfying assumptions; returns counter-strategy if not.
Instructions
GR(1) synthesis (slugs): realizability. Can a component choose its outputs so that the guarantees hold for every environment satisfying the assumptions? realizable, or unrealizable with the counter-strategy of the environment; with core, also the unrealizable core (see unrealizable_core). Needs slugs; the formulas must be in the GR(1) fragment.
Tool call template
Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {
"contract": "<contract>"
},
"name": "is_realizable"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| core | No | ||
| timeout | No | ||
| contract | Yes |