CHASE MCP Server

Overview Schema Source Related Servers Discussions Admin

is_vacuous

Read-onlyIdempotent

Detect outputs whose liveness guarantees are vacuously satisfied in GR(1) synthesis, listing each output's vacuity mode and a winning strategy to guide contract repair.

Instructions

GR(1) synthesis (slugs): vacuity. Can the component win without an output that a liveness guarantee asks for (Bloem et al., FMSD 2021)? vacuous lists each such output with its mode, never (a winning strategy never sets it: the guarantee that names it is discharged by the assumptions) or eventually (a winning strategy stops setting it), and the strategy; with core, a minimal set of assumptions that lets it. not_vacuous; unrealizable when the contract itself is; unknown. The outputs checked are outputs, by default those that occur only positively in a liveness guarantee (G F ...).

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_vacuous"
  }
}

Input Schema

Name	Required	Description	Default
`core`	No
`outputs`	No
`timeout`	No
`contract`	Yes

Schema Changelog

Changes observed during successful MCP inspections.

Changed1 schema field changedv0.7.0Nov 2, 2026

addedInput schema / $defs / ContractSpec / properties / constants

Added value: +{
+  "additionalProperties": {
+    "anyOf": [
+      {
+        "type": "integer"
+      },
+      {
+        "type": "number"
+      }
+    ]
+  },
+  "description": "Named constants: name -> value; the formulas use the names (repair changes them)",
+  "title": "Constants",
+  "type": "object"
+}

Addedv0.4.2Oct 29, 2026

TDQS

A3.5/5.0

Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With annotations already declaring readOnlyHint=true, openWorldHint=false, and idempotentHint=true, the description adds substantial behavioral context: it explains the vacuous modes 'never' and 'eventually', the effect of the 'core' option, and the not_vacuous/unrealizable/unknown outcomes. It does not discuss timeout behavior or error conditions, but the semantic disclosure is strong.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is dense but front-loaded, beginning with the specific GR(1) vacuity question before moving into result modes and defaults. It avoids filler, though the semicolon-heavy run-on structure makes it harder to parse than a more structured presentation would be.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a complex synthesis tool with no output schema, the description does a good job explaining the returned outcomes and the meaning of vacuous modes and core sets. It still omits timeout semantics and exact response shape details, but the core behavioral completeness is solid.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is reported as 0%, so the description must compensate. It does explain the 'outputs' parameter and its default selection rule, and it implies the meaning of 'core' by saying it returns a minimal set of assumptions. However, it does not explain 'timeout', and the required 'contract' parameter is only indirectly described through the vacuity concepts, leaving clear gaps.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly identifies the tool as a GR(1) vacuity check and explains the core question: whether a component can win without producing an output required by a liveness guarantee. It also names the possible outcomes (vacuous, not_vacuous, unrealizable, unknown). It does not explicitly contrast itself against sibling tools such as is_realizable or synthesize, so it falls short of a 5.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explains what the vacuity check returns and how outputs are selected, but it gives no explicit guidance on when to call this tool instead of alternatives like is_realizable, unrealizable_core, or synthesize. There are no when-to-use or when-not-to-use conditions.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.