visualize
Draw assume-guarantee contracts as an interactive web page, composing parts by ports and checking assumptions, guarantees, refinements, and environments to expose specification issues.
Instructions
Draw contracts as a web page: the contracts given as JSON, or the
contracts of a specification in the logics language of CHASE (text, or
the path of a file). Without draw and refines, the contracts are put
together by their ports: an output and an input of the same name are
wired; contracts with the same ports are versions of one part, and the
first one is wired; a contract whose outputs several parts drive, and
which gives them what they read from outside, has the parts drawn
inside it. draw names the contracts to draw instead; NAME+NAME draws
their composition, a box with the contracts inside, wired by the names
of their variables. refines lists [refined, abstract] pairs: the
refined one is drawn inside the abstract one, and checked against it. A
decomposition is drawn and checked only when a pair names it:
refines: [["Sensor+Controller", "Cruise"]]. An input of a part that no
other part or input of the box drives is marked (its name in orange).
environments lists [model file, contract] pairs: the state machine
(SMV, JSON, or a controller of slugs) is drawn on the left of the
contract, as an environment. check (the default) checks that the
assumptions and the guarantees of each contract can hold together
(A ∧ G, with the core when they cannot), and the refinements and the
environments drawn; for a file (path), the results are kept next to
it (FILE.results.json), and a check of contracts that have not changed
is not run again. verify and realizable check each contract drawn, and
mark the terms of a core when a check fails. open names the contracts
drawn open (their terms, and the core of a check that fails). The
page is written to output (default: a new temporary file) and opens in
any browser. Returns its path, and for each box its checks.
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": "visualize"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| draw | No | ||
| open | No | ||
| path | No | ||
| text | No | ||
| check | No | ||
| output | No | ||
| verify | No | ||
| refines | No | ||
| timeout | No | ||
| contracts | No | ||
| realizable | No | ||
| environments | No |