is_receptive
Checks whether a state machine accepts every input allowed by its contract assumptions and returns a refusal trace when it does not.
Instructions
Does the state machine accept every input that the assumptions of the
contract allow? A machine that refuses an input has no behavior with it,
so is_implementation may hold only because it blocks the inputs. receptive, or
not_receptive with the trace to the state after which it refuses an
input (details: state and input). Uses the initial and safety
assumptions; the inputs must be Boolean or integer ranges.
The state machine is given as one of: smv, a program in SMV (the input
language of nuXmv: MODULE main with VAR/IVAR, INIT, TRANS..., no
specification) that declares the variables of the contract; machine, a
state machine in JSON {"name", "inputs", "outputs", "states", "initial",
"transitions": [{"from", "when", "outputs", "to"}]}: at each step, in its
state, the machine takes a transition whose when (a formula over the
variables) holds, sets the outputs of that step, and moves to to; or
controller, the controller returned by synthesize, with the contract it
was synthesized from in synthesized_from (default: the contract); or
rtl, a Verilog or SystemVerilog module (see rtl_ports for its ports).
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_receptive"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| rtl | No | ||
| smv | No | ||
| backend | No | auto | |
| machine | No | ||
| timeout | No | ||
| contract | Yes | ||
| controller | No | ||
| synthesized_from | No |