From d62f945bc553c391bd2dc042707b014961ed04bf Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 14 Dec 2023 17:35:07 +0100 Subject: [PATCH] tools/cexenum: Document JSON callback protocol --- tools/cexenum/callbacks.md | 46 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 tools/cexenum/callbacks.md diff --git a/tools/cexenum/callbacks.md b/tools/cexenum/callbacks.md new file mode 100644 index 0000000..ca3a3ec --- /dev/null +++ b/tools/cexenum/callbacks.md @@ -0,0 +1,46 @@ +# Callback JSON Protocol + +The `--callback` option allows controlling the counter-example enumeration using a JSON based protocol. + +With `--callback '-'`, callback events are output to stdout and callback responses are read from stdin. + +With `--callback ''` the given command line is launched as subprocess which recieves callback events on stdin and produces callback responses on stdout. + +Each event and response consists of a single line containing a JSON object. + +## Callback Events + +A callback event is emitted whenever: + +* a step is entered for the first time (`"event": "step"`), +* a new counter-example trace was found (`"event": "trace"`) or +* no counter-examples remain for the current step (`"event": "unsat"`). + +Every callback event includes the current step (`"step": `) and a list of enabled named blocked patterns (`"enabled": [...]`, see below). + +A trace event also includes a path to the `.yw` file of the counter-example trace. The `.aiw` file can be found by replacing the file extension. + +After an event is emitted, the enumeration script waits for one or multiple callback responses, continuing when a callback response includes the `"action"` key. + +## Callback Responses + +### Actions + +An action hands control back to the enumeration script. The following three actions are available: + +* `{"action": "search"}`: Search for a further counter-example in the current time step. +* `{"action": "advance"}`: Advance to the next time step, abandoning any not-yet-enumerated counter-examples of the current time step. +* `{"action": "next"}`: Search for the next counter-example, automatically advancing to the next time-step when necessary. + +Note that an `{"action": "search"}` response to an `"unsat"` event remains at the same time step, which can be used to disable a named blocked pattern, which can make further counter-examples available. + +In the interactive callback mode (`--callback '-'`) it is possible to use single letter shortcuts `s`, `a` and `n` instead of the JSON syntax `{"action": "search"}`, `{"action": "advance"}` and `{"action": "next"}` respectively. + +### Blocking Patterns + +A specific input pattern given as an `.yw` or `.aiw` file can be blocked. +During enumeration, only counter-examples that differ from in at least one non-`x` bit from every blocked pattern are considered. + +A `.yw` pattern can be blocked using `{"block_yw": ""}` and a `.aiw` pattern using `{"block_aiw": ""}`. Additionally a pattern can be given a name by using `{"block_...": "", "name": ""}`, in which case it will be possible to disable and reenable the blocked pattern. By default a newly added named blocked pattern is enabled. + +A named pattern can be disable with the `{"disable": ""}` response and re-enabled with the `{"enable": ""}` response.