Skip to main content
Glama
Sign In
CHASE MCP Server

CHASE MCP Server

by chase-cps
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

unrealizable_core

Read-onlyIdempotent

Computes a minimal set of guarantees that renders an assume-guarantee contract unrealizable under all assumptions, returning the core for GR(1) specification debugging.

Instructions

GR(1) synthesis (slugs): a minimal set of guarantees that is unrealizable under all the assumptions: removing any of them makes the contract realizable. status is found with core (the contract with those guarantees), none when the contract is realizable, or unknown with the reason. Needs slugs.

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": "unrealizable_core"
  }
}

Input Schema

NameRequiredDescriptionDefault
timeoutNo
contractYes

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed1 schema field changedv0.7.0
    • 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"
+}
  2. Changed4 schema fields changedv0.4.2
    • changedInput schema / $defs / ContractSpec / properties / inputs / additionalProperties / anyOf
      Previous value: -[
-  {
-    "enum": [
-      "bool",
-      "real"
-    ],
-    "type": "string"
-  },
-  {
-    "maxItems": 2,
-    "minItems": 2,
-    "prefixItems": [
-      {
-        "type": "integer"
-      },
-      {
-        "type": "integer"
-      }
-    ],
-    "type": "array"
-  }
-]New value: +[
+  {
+    "enum": [
+      "bool",
+      "real"
+    ],
+    "type": "string"
+  },
+  {
+    "maxItems": 2,
+    "minItems": 2,
+    "prefixItems": [
+      {
+        "type": "integer"
+      },
+      {
+        "type": "integer"
+      }
+    ],
+    "type": "array"
+  },
+  {
+    "pattern": "^(signed |unsigned )?word\\[[1-9][0-9]*\\]$",
+    "type": "string"
+  }
+]
    • changedInput schema / $defs / ContractSpec / properties / inputs / description
      Previous value: -"Input variables: \"bool\", [low, high], or \"real\""New value: +"Input variables: \"bool\", [low, high], \"real\", or \"word[n]\" (\"signed word[n]\")"
    • changedInput schema / $defs / ContractSpec / properties / outputs / additionalProperties / anyOf
      Previous value: -[
-  {
-    "enum": [
-      "bool",
-      "real"
-    ],
-    "type": "string"
-  },
-  {
-    "maxItems": 2,
-    "minItems": 2,
-    "prefixItems": [
-      {
-        "type": "integer"
-      },
-      {
-        "type": "integer"
-      }
-    ],
-    "type": "array"
-  }
-]New value: +[
+  {
+    "enum": [
+      "bool",
+      "real"
+    ],
+    "type": "string"
+  },
+  {
+    "maxItems": 2,
+    "minItems": 2,
+    "prefixItems": [
+      {
+        "type": "integer"
+      },
+      {
+        "type": "integer"
+      }
+    ],
+    "type": "array"
+  },
+  {
+    "pattern": "^(signed |unsigned )?word\\[[1-9][0-9]*\\]$",
+    "type": "string"
+  }
+]
    • changedInput schema / $defs / ContractSpec / properties / outputs / description
      Previous value: -"Output variables: \"bool\", [low, high], or \"real\""New value: +"Output variables: \"bool\", [low, high], \"real\", or \"word[n]\" (\"signed word[n]\")"
  3. First observedv0.3.1

TDQS

B3.2/5.0
Behavior3/5

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

With readOnlyHint/idempotentHint already declaring the safety profile, the description's real contribution is enumerating the three result states (found with core, none when realizable, unknown with reason) — genuinely useful behavior since there is no output schema. However it leaves the prerequisite opaque: 'Needs slugs' does not say whether an external binary must be installed, what happens if it is missing, or that unknown is the likely outcome then.

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?

Four short clauses, front-loaded with the operation and its defining property, then the return states, then the dependency note. No filler; the only roughness is the terse fragment 'Needs slugs' with no elaboration.

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

Completeness3/5

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

For a computational synthesis tool with no output schema, the three status values and the 'unknown with reason' behavior cover the essential return semantics. Missing are the external-tool prerequisite and timeout meaning, which matter for an agent deciding whether the call will succeed.

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

Parameters2/5

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

Schema description coverage is reported at 0% for the two top-level parameters: neither `contract` nor `timeout` is explained in the description. The $defs do document nested ContractSpec fields, but the description adds nothing about the timeout (default 300, what it bounds) or about building the contract. With low coverage the description should compensate and it does not.

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?

States a specific verb+resource: computes a minimal unrealizable set of guarantees from an assume-guarantee contract. The definition ('removing any of them makes the contract realizable') is precise and distinguishes it from plain realizability checking. It does not explicitly contrast itself with the sibling unsat_core, which is the closest conceptually adjacent tool.

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

Usage Guidelines3/5

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

Usage is implied rather than stated: you would call this when a GR(1) contract is unrealizable and you want to know why. There is no explicit 'use this instead of is_realizable / unsat_core when...' routing, and the 'Needs slugs' note hints at a prerequisite without stating what to do if slugs is unavailable.

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

Deploy Server

Other Tools