Merge pull request #3210 from apalache-mc/igor/json-rpc-assume-state

Refactor JSON handling code towards `assumeState`

Author: konnov

json-rpc/README.md

@@ -2,7 +2,7 @@
 
 **Authors:** [Igor Konnov][] and [Thomas Pani][]
 
-A simple JSON-RPC server module for Apalache. This is work in progress:
+A simple JSON-RPC server module for Apalache. **This is work in progress.**
 
 This server is not meant to be a replacement for the current gRPC server (SHAI).
 Rather, it is a lightweight alternative that can be used for symbolic
@@ -41,7 +41,7 @@ exploration of TLA+ specifications.
     - [Jetty Server][]. Yes, it is about 30 years old.
       It works. It is fast, simple, reliable, maintained, and is well-documented.
     - [Jackson][]. It is fast, simple, reliable, maintained, and is well-documented.
-      It uses plain-old Java objects, and it supports basic Scala types. No super-advanced
+      It uses plain-old Java objects, and it supports basic Scala types. No advanced
       FP here.
 
 ## 2. JSON-RPC methods
@@ -53,6 +53,15 @@ See the [JSON-RPC specification][] for more details. It is real short.
 
 This is work in progress. More methods to be added in the future.
 
+In the JSON format below, we write `"${placeholders}"` to indicate values that
+should be replaced with actual values. They have to be of proper types, e.g.,
+strings, numbers, booleans, arrays, or objects. We write them in quotes to
+produce valid JSON snippets.
+
+Some of the methods accept and return traces and expressions in the
+[ITF Format][]. You can use the [itf-py][] library to produce and parse
+such traces and expressions in Python.
+
 **Running the server.** To try the examples below, you need to start the server
 first:
 
@@ -83,21 +92,21 @@ be used in subsequent calls to refer to this session.
   "method": "loadSpec",
   "params": {
     "sources": [
-      <rootModuleInBase64>,
-      <importedModule1InBase64>,
-      ...
+      "${root-module-in-base64}",
+      "${imported-module1-in-base64}",
+      "..."
     ],
-    "init": "optional-initializer-predicate",
-    "next": "optional-transition-predicate",
+    "init": "${optional-initializer-predicate}",
+    "next": "${optional-transition-predicate}",
     "invariants": [
-      "invariant 1",
-      ...,
-      "invariant N"
+      "${invariant-1}",
+      "...",
+      "${invariant-N}"
     ],
     "exports": [
-      "exported-operator-1",
-      ...,
-      "exported-operator-M"
+      "${exported-operator-1}",
+      "...",
+      "${exported-operator-M}"
     ]
   }
 }
@@ -113,13 +122,13 @@ operators such as `Init`, `Next`, and the invariants.
 ```json
 {
   "result": {
-    "sessionId": "unique-session-identifier",
-    "snapshotId": snapshot-identifier-after-loading-the-spec,
+    "sessionId": "${unique-session-identifier}",
+    "snapshotId": "${snapshot-identifier-after-loading-the-spec}",
     "specParameters": {
-      "initTransitions": init-metadata,
-      "nextTransitions": next-metadata,
-      "stateInvariants": state-invariants-metadata,
-      "actionInvariants": action-invariants-metadata,
+      "initTransitions": "${init-metadata}",
+      "nextTransitions": "${next-metadata}",
+      "stateInvariants": "${state-invariants-metadata}",
+      "actionInvariants": "${action-invariants-metadata}"
     }
   }
 }
@@ -129,8 +138,8 @@ The metadata entries look like:
 
 ```json
 {
-  "index": i,
-  "labels": ["label1", "label2", ...]
+  "index": "${integer-index}",
+  "labels": ["label1", "label2", "..."]
 }
 ```
 
@@ -206,7 +215,7 @@ session identifier. No further calls should be made with this session identifier
 {
   "method": "disposeSpec",
   "params": {
-    "sessionId": "session-identifier"
+    "sessionId": "${session-identifier}"
   }
 }
 ```
@@ -219,7 +228,7 @@ This identifier cannot be used in the future calls.
 ```json
 {
   "result": {
-    "sessionId": "session-identifier"
+    "sessionId": "${session-identifier}"
   }
 }
 ```
@@ -262,8 +271,8 @@ roll back to it again later.
 {
   "method": "rollback",
   "params": {
-    "sessionId": "session-id",
-    "snapshotId": snapshot-id
+    "sessionId": "${session-id}",
+    "snapshotId": "${snapshot-id}"
   }
 }
 ```
@@ -276,8 +285,8 @@ that was rolled back to:
 ```json
 {
   "result": {
-    "sessionId": "session-id",
-    "snapshotId": snapshot-id
+    "sessionId": "${session-id}",
+    "snapshotId": "${snapshot-id}"
   }
 }
 ```
@@ -323,10 +332,10 @@ snapshot.
 {
   "method": "assumeTransition",
   "params": {
-    "sessionId": "session-identifier",
-    "transitionId": transition-identifier,
-    "checkEnabled": check-if-transition-is-enabled,
-    "timeoutSec": timeout-in-seconds-or-0,
+    "sessionId": "${session-identifier}",
+    "transitionId": "${integer-transition-identifier}",
+    "checkEnabled": "${boolean-flag}",
+    "timeoutSec": "${timeout-in-seconds-or-0}"
   }
 }
 ```
@@ -336,9 +345,9 @@ snapshot.
 ```json
 {
   "result": {
-    "sessionId": "session-identifier",
-    "snapshotId": new-snapshot-id,
-    "transitionId": transition-identifier,
+    "sessionId": "${session-identifier}",
+    "snapshotId": "${new-snapshot-id}",
+    "transitionId": "${integer-transition-identifier}",
     "status": "ENABLED|DISABLED|UNKNOWN"
   }
 }
@@ -381,7 +390,7 @@ new constraints, `nextStep` takes a new snapshot.
 {
   "method": "nextState",
   "params": {
-    "sessionId": "session-identifier"
+    "sessionId": "${session-identifier}"
   }
 }
 ```
@@ -391,9 +400,9 @@ new constraints, `nextStep` takes a new snapshot.
 ```json
 {
   "result": {
-    "sessionId": "session-identifier",
-    "snapshotId": new-snapshot-id,
-    "newStepNo": new-step-number
+    "sessionId": "${session-identifier}",
+    "snapshotId": "${new-snapshot-id}",
+    "newStepNo": "${new-step-number}"
   }
 }
 ```
@@ -446,10 +455,10 @@ checking the invariant, the context is rolled back to the state before the call.
 {
   "method": "checkInvariant",
   "params": {
-    "sessionId": "session-identifier",
-    "invariantId": invariant-identifier,
+    "sessionId": "${session-identifier}",
+    "invariantId": "${integer-invariant-identifier}",
     "kind": "STATE|ACTION",
-    "timeoutSec": timeout-in-seconds-or-0
+    "timeoutSec": "${timeout-in-seconds-or-0}"
   }
 }
 ```
@@ -459,9 +468,9 @@ checking the invariant, the context is rolled back to the state before the call.
 ```json
 {
   "result": {
-    "sessionId": "session-identifier",
+    "sessionId": "${session-identifier}",
     "invariantStatus": "SATISFIED|VIOLATED|UNKNOWN",
-    "trace": trace-in-itf-or-null,
+    "trace": "${trace-in-itf-or-null}"
   }
 }
 ```
@@ -520,10 +529,10 @@ set, or it is set to `0`, then the timeout is infinite.
 {
   "method": "query",
   "params": {
-    "sessionId": "session-identifier",
-    "kinds": [ kind1, kind2, ... ],
-    "operator": optional-operator-name,
-    "timeoutSec": timeout-in-seconds-or-0
+    "sessionId": "${session-identifier}",
+    "kinds": [ "${kind1}", "${kind2}", "..." ],
+    "operator": "${optional-operator-name}",
+    "timeoutSec": "${timeout-in-seconds-or-0}"
   }
 }
 ```
@@ -537,9 +546,9 @@ and `expr` are in the [ITF Format][].
 ```json
 {
   "result": {
-    "sessionId": "session-identifier",
-    "trace": trace-in-itf-or-null,
-    "operatorValue": expr-in-itf-or-null
+    "sessionId": "${session-identifier}",
+    "trace": "${trace-in-itf-or-null}",
+    "operatorValue": "${expr-in-itf-or-null}"
   }
 }
 ```
@@ -592,9 +601,9 @@ returned by `nextState`).
 {
   "method": "nextModel",
   "params": {
-    "sessionId": "session-identifier",
-    "operator": <operator-name>,
-    "timeoutSec": timeout-in-seconds-or-0
+    "sessionId": "${session-identifier}",
+    "operator": "${operator-name}",
+    "timeoutSec": "${timeout-in-seconds-or-0}"
   }
 }
 ```
@@ -619,10 +628,10 @@ The output contains the following fields:
 ```json
 {
   "result": {
-    "sessionId": "session-identifier",
-    "oldValue": expr-in-itf-or-null,
-    "hasOld": (TRUE|FALSE|UNKNOWN),
-    "hasNext": (TRUE|FALSE|UNKNOWN)
+    "sessionId": "${session-identifier}",
+    "oldValue": "${expr-in-itf-or-null}",
+    "hasOld": "TRUE|FALSE|UNKNOWN",
+    "hasNext": "TRUE|FALSE|UNKNOWN"
   }
 }
 ```
@@ -658,6 +667,73 @@ The output is as follows:
 }
 ```
 
+### 2.9. Method assumeState
+
+Given a session identifier and concrete equalities `x = e` over a subset of the state
+variables, add the equality constraints to the SMT context. The expressions in the
+right-hand sides are given as expressions in the [ITF Format][].
+
+Additionally, if `checkEnabled` is set to `true`, the server checks, whether there is a
+state that is reachable via the current transition prefix, including the added
+constraints. The parameter `timeoutSec` sets the timeout for this check in seconds.
+If `timeout` is not set, or it is set to `0`, then the timeout is infinite.
+
+**Precondition.** The call to `assumeState` can be made only after at least single
+call to `assumeTransition` and `nextStep`.
+
+**Effect.** The concrete equalities are translated as SMT equality constraints in
+the current context against the current symbolic state (sometimes, called a frame).
+These constraints do not override the existing assignments in the context. Rather,
+they pose additional constraints on top of the existing ones.
+
+**Input:**
+
+```json
+{
+  "method": "assumeState",
+  "params": {
+    "sessionId": "${session-identifier}",
+    "checkEnabled": "${boolean-flag}",
+    "timeoutSec": "${timeout-in-seconds-or-0}",
+    "equalities": {
+      "${var-1}": "${expr-in-itf}",
+      "...": "...",
+      "${var-k}": "${expr-in-itf}"
+    }
+  }
+}
+```
+
+**Output:**
+
+```json
+{
+  "result": {
+    "sessionId": "${session-identifier}",
+    "snapshotId": "${new-snapshot-id}",
+    "status": "ENABLED|DISABLED|UNKNOWN"
+  }
+}
+```
+
+**Example**:
+
+Execute the following command:
+
+```sh
+$ curl -X POST http://localhost:8822/rpc \
+  -H "Content-Type: application/json" \
+  -d '{"jsonrpc":"2.0","method":"assumeState",
+       "params":{"sessionId":"1","checkEnabled":true,"equalities": {"x":{"#bigint":"1"}}},"id":4}'
+```
+
+It produces the following output:
+
+```json  
+{"jsonrpc":"2.0","id":2,"result":{"sessionId":"1","snapshotId":3,"status":"ENABLED"}}
+```
+
+
 [Jetty Server]: https://jetty.org/
 
 [Jackson]: https://github.com/FasterXML/jackson
@@ -672,4 +748,6 @@ The output is as follows:
 
 [Apalache IR]: https://apalache-mc.org/docs/adr/005adr-json.html
 
-[SMT randomization]: https://apalache-mc.org/docs/apalache/tuning.html#randomization
+[SMT randomization]: https://apalache-mc.org/docs/apalache/tuning.html#randomization
+
+[itf-py]: https://github.com/konnov/itf-py/

json-rpc/src/main/scala/com/github/apalachemc/apalache/jsonrpc/ExplorationServiceParams.scala

@@ -1,5 +1,7 @@
 package com.github.apalachemc.apalache.jsonrpc
 
+import com.fasterxml.jackson.databind.JsonNode
+
 sealed abstract class ExplorationServiceParams
 
 /**
@@ -161,3 +163,33 @@ case class NextModelParams(
     operator: String = "",
     timeoutSec: Int = 0)
     extends ExplorationServiceParams
+
+/**
+ * Parameters for preparing a symbolic transition in the solver context.
+ * @param sessionId
+ *   the ID of the previously loaded specification
+ * @param equalities
+ *   a JSON-encoded list of equalities to assume in the current state (in the ITF format)
+ * @param checkEnabled
+ *   whether to check if the transition is enabled. If `false`, the transition is prepared and assumed, but no
+ *   satisfiability is checked
+ * @param timeoutSec
+ *   the timeout in seconds for checking satisfiability. If `0`, the default timeout is used. This parameter is ignored
+ *   if `checkEnabled` is `false`.
+ */
+case class AssumeStateParams(
+    sessionId: String,
+    equalities: JsonNode,
+    checkEnabled: Boolean,
+    timeoutSec: Int = 0)
+    extends ExplorationServiceParams
+
+object AssumeStateParams {
+  def apply(
+      sessionId: String,
+      equalities: JsonNode,
+      checkEnabled: Boolean = true,
+      timeoutSec: Int = 0): AssumeStateParams = {
+    new AssumeStateParams(sessionId, equalities, checkEnabled, timeoutSec)
+  }
+}