Skip to content

Commit 17d1bdb

Browse files
committed
register assumeState and fix README
1 parent 37c395c commit 17d1bdb

File tree

2 files changed

+8
-2
lines changed

2 files changed

+8
-2
lines changed

json-rpc/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -724,13 +724,13 @@ Execute the following command:
724724
$ curl -X POST http://localhost:8822/rpc \
725725
-H "Content-Type: application/json" \
726726
-d '{"jsonrpc":"2.0","method":"assumeState",
727-
"params":{"sessionId":"1","checkEnabled":true,"equalities": {"x":{"#bigint":"1"}}},"id":4}'
727+
"params":{"sessionId":"1","checkEnabled":true,"equalities": {"x":{"#bigint":"0"}}},"id":4}'
728728
```
729729
730730
It produces the following output:
731731
732732
```json
733-
{"jsonrpc":"2.0","id":2,"result":{"sessionId":"1","snapshotId":3,"status":"ENABLED"}}
733+
{"jsonrpc":"2.0","id":4,"result":{"sessionId":"1","snapshotId":5,"status":"ENABLED"}}
734734
```
735735
736736

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -830,6 +830,12 @@ class JsonRpcServlet(service: ExplorationService) extends HttpServlet with LazyL
830830
.fold(errorMessage => Left(ServiceError(JsonRpcCodes.INVALID_PARAMS, errorMessage)),
831831
serviceParams => service.assumeTransition(serviceParams))
832832

833+
case "assumeState" =>
834+
new JsonParameterParser(mapper)
835+
.parseAssumeState(paramsNode)
836+
.fold(errorMessage => Left(ServiceError(JsonRpcCodes.INVALID_PARAMS, errorMessage)),
837+
serviceParams => service.assumeState(serviceParams))
838+
833839
case "nextStep" =>
834840
new JsonParameterParser(mapper)
835841
.parseNextStep(paramsNode)

0 commit comments

Comments
 (0)