From e89aec16b1a0b249d56aa0bce20e018a346bdaf4 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 24 Aug 2023 13:52:55 +1000 Subject: [PATCH 1/3] Add explanation for the `condition.substitution` field in `implies` results Closes #3445 --- docs/2022-07-18-JSON-RPC-Server-API.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 4aa914bd7e..b4d684d3fc 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/docs/2022-07-18-JSON-RPC-Server-API.md @@ -314,7 +314,7 @@ Other errors are specific to the implication checker and what it supports. These The endpoint simplifies `antecedent` and `consequent` terms and checks whether the implication holds. The simplified implication is returned (as a KORE term) in field `implication`. -If the implication holds, `satisfiable` is `true` and `condition` contains a unifying condition for the simplified antecedent and consequent (as provided in `implication`). +If the implication holds, `satisfiable` is `true` and `condition` contains a witness, in the form of a predicate and a substitution which unifies the simplified antecedent and the consequent with existential quantifiers removed. The `condition.substitution` will contain a witnessing value for each existentially quantified variable of the RHS. ```json { From 8a53c61a90696b9136d63dc5c0d2f0d1e12fdb34 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 24 Aug 2023 14:02:31 +1000 Subject: [PATCH 2/3] Explain a subtlety of `next-states` in `branching` results In a `branching` result, the user might be thinking that all states in `next-states` have taken a single rewrite step from `state`. This is not correct. If the branching condition together with other predicates in `state` make the state `\bottom` as a whole, the result will contain the `term` from `state`and the `predicate` adding the branching condition to the existing predicates from `state`. This state is in fact `stuck` but is reported to the caller as a branch to provide all available information. Closes #3622 --- docs/2022-07-18-JSON-RPC-Server-API.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index b4d684d3fc..9ed2640170 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/docs/2022-07-18-JSON-RPC-Server-API.md @@ -178,6 +178,9 @@ If `"reason": "branching"`, an additional `next-states` field contains all follo } ``` +**Note that** it is possible that some of the `next-states` have not actually taken rewrite steps. In cases where one of the branches is stuck because of an added (branching) side condition, `next-states` will contain this branch with a term identical to the one in `state` and the branching condition added to the prior `predicate` from `term` (Rationale: a subsequent `execute` step starting from this `state` will of course immediately report `stuck`, and the branching should be indicated to the user). + + If `"reason": "cut-point-rule"`, the `next-states` field contains the next state (if any) in a list. The `rule` field indicates which rule led to stopping. ```json From 295214b1130f1a63e262034369cf8cbb9f2e7c01 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 24 Aug 2023 14:37:09 +1000 Subject: [PATCH 3/3] Enrich RPC documentation of execute stop reasons, add `vacuous` Each stop reason for `execute` is discussed in its own paragraph, explaining what they mean and relating to relevant request parameters (which are typically optional). Closes #3642 All optionaity of parameters is clearly stated IMHO, and what they do is explained while discussing the different `reason`s. Closes #3629 The `vacuous` reason was added while rearranging the text. --- docs/2022-07-18-JSON-RPC-Server-API.md | 89 +++++++++++++++++--------- 1 file changed, 60 insertions(+), 29 deletions(-) diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index 9ed2640170..b88a825bab 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/docs/2022-07-18-JSON-RPC-Server-API.md @@ -100,10 +100,11 @@ All correct responses have a result containing a `reason`, with one of the follo * `"reason": "depth-bound"` * `"reason": "cut-point-rule"` * `"reason": "terminal-rule"` +* `"reason": "vacuous"` * `"reason": "timeout"` * `"reason": "aborted"` -A field `state` contains the state reached (including optional `predicate` and `substitution`), a field `depth` indicates the execution depth. +and a field `state` which contains the state reached (including optional `predicate` and `substitution`), as well as a field `depth` indicating the execution depth (i.e., number of rewrite steps. ```json { @@ -122,12 +123,30 @@ A field `state` contains the state reached (including optional `predicate` and ` } ``` -The above will be also be the same for: - * `"reason": "depth-bound"` - * `"reason": "timeout"` - * `"reason": "aborted"` +#### Explanation of `reason` field and additional fields. +The `reason` field provides information about why the execution stopped. +Depending on the given `reason`, additional fields may be present. -If `"reason": "terminal-rule"`, an additional `rule` field indicates which of the `terminal-rule` labels or IDs led to terminating the execution: +##### `"reason": "stuck"` +Execution reached a state where no rewrite rule could be applied. +This response has no additional fields. + +##### `"reason": "depth-bound"` +Execution reached the `max-depth` bound provided in the request +This response has no additional fields. + +##### `"reason": "timeout"` +Execution was stopped because a rewrite step took longer than the `step-timeout` provided in the request (either in absolute time for a single step, or as a moving average value). +This response has no additional fields. + +##### `"reason": "aborted"` +Execution reached a state that the server cannot handle. +This response has no additional fields. + +##### `"reason": "cut-point-rule"` +Execution was about to perform a rewrite with a rule whose label is one of the `cut-point-rules` labels/IDs of the request. +An additional `rule` field indicates which of the `cut-point-rules` labels/IDs led to stopping. +An additional `next-states` field contains the next state (which stems from the RHS of this rule) in a singleton list. ```json { @@ -139,16 +158,25 @@ If `"reason": "terminal-rule"`, an additional `rule` field indicates which of t "predicate": {"format":"KORE", "version":1, "term":{}}, "substitution": {"format":"KORE", "version":1, "term":{}}, }, - "depth": 1, - "reason": "terminal-rule", - "rule": "ruleFoo", + "depth": 2, + "reason": "cut-point-rule", + "rule": "rule1", + "next-states": [ + { + "term": {"format": "KORE", "version": 1, "term": {}}, + "predicate": {"format":"KORE", "version":1, "term":{}}, + "substitution": {"format":"KORE", "version":1, "term":{}}, + } + ], "logs": [] } } ``` +##### `"reason": "terminal-rule"` +Execution performed a rewrite with a rule whose label is one of the `terminal-rules` labels/IDs of the request. +An additional `rule` field indicates which of the `terminal-rule` labels or IDs led to terminating the execution: -If `"reason": "branching"`, an additional `next-states` field contains all following states of the branch point. ```json { "jsonrpc": "2.0", @@ -159,30 +187,22 @@ If `"reason": "branching"`, an additional `next-states` field contains all follo "predicate": {"format":"KORE", "version":1, "term":{}}, "substitution": {"format":"KORE", "version":1, "term":{}}, }, - "depth": 2, - "reason": "branching", - "next-states": [ - { - "term": {"format": "KORE", "version": 1, "term": {}}, - "predicate": {"format":"KORE", "version":1, "term":{}}, - "substitution": {"format":"KORE", "version":1, "term":{}}, - }, - { - "term": {"format": "KORE", "version": 1, "term": {}}, - "predicate": {"format":"KORE", "version":1, "term":{}}, - "substitution": {"format":"KORE", "version":1, "term":{}}, - } - ], + "depth": 1, + "reason": "terminal-rule", + "rule": "ruleFoo", "logs": [] } } ``` -**Note that** it is possible that some of the `next-states` have not actually taken rewrite steps. In cases where one of the branches is stuck because of an added (branching) side condition, `next-states` will contain this branch with a term identical to the one in `state` and the branching condition added to the prior `predicate` from `term` (Rationale: a subsequent `execute` step starting from this `state` will of course immediately report `stuck`, and the branching should be indicated to the user). - +##### `"reason": "vacuous"` +Execution reached a state where, most likely because of ensured side conditions, the configuration became equivalent to `\bottom`. +The `state` field contains this last configuration, no additional fields are present. -If `"reason": "cut-point-rule"`, the `next-states` field contains the next state (if any) in a list. The `rule` field indicates which rule led to stopping. +##### `"reason": "branching"` +More than one rewrite rule has applied (possibly because of splitting the state and adding branching conditions) +An additional `next-states` field contains all following states of the branch point. ```json { "jsonrpc": "2.0", @@ -194,9 +214,13 @@ If `"reason": "cut-point-rule"`, the `next-states` field contains the next state "substitution": {"format":"KORE", "version":1, "term":{}}, }, "depth": 2, - "reason": "cut-point-rule", - "rule": "rule1", + "reason": "branching", "next-states": [ + { + "term": {"format": "KORE", "version": 1, "term": {}}, + "predicate": {"format":"KORE", "version":1, "term":{}}, + "substitution": {"format":"KORE", "version":1, "term":{}}, + }, { "term": {"format": "KORE", "version": 1, "term": {}}, "predicate": {"format":"KORE", "version":1, "term":{}}, @@ -208,6 +232,13 @@ If `"reason": "cut-point-rule"`, the `next-states` field contains the next state } ``` +##### Clarifications +* It is possible that some of the `next-states` in a `branching` result have not actually taken rewrite steps. If one of the branches is stuck because of the added (branching) side condition, `next-states` will also contain this branch, with a term identical to the one in `state` and the branching condition added to the prior `predicate` from `term`. + Rationale: The branching should be indicated to the user. A subsequent `execute` step starting from this stuck `state` will of course immediately report `stuck`. +* `branching` results are preferred to `cut-point-rule` and `terminal-rule` results. That means, if execution reaches a branch with one of the applying rules having a label/ID from `cut-point-rules` or `terminal-rules`, the response will be `branching`. + Rationale: The branching information must be provided, assuming the client will re-execute on each branch. + +#### Optional Logging If any logging is enabled, the optional `logs` field will be returned containing an array of objects of the following structure: ```json