JSON and Sockets

Introduction

ProB contains external functions to read and write JSON data and to communicate via sockets using JSON-RPC:

• LibraryJSON.def and LibraryJSON.mch providing the functions READ_JSON, READ_JSON_FROM_STRING, WRITE_JSON, WRITE_JSON_TO_STRING and the freetype JsonValue to read and write JSON data.

• LibraryZMQ_RPC.def and LibraryZMQ_RPC.mch: providing access to a JSON-RPC (Remote Procedure Call) protocol implementation over either TCP sockets using NDJSON or over ZeroMQ sockets.

We have used this library to control Crazyflie drones via ProB:

JSON Library

LibraryJSON.mch defines a FREETYPE to represent JSON data in a type-safe way:

  JsonValue = JsonNull,
              JsonBoolean(BOOL),
              JsonNumber(FLOAT),
              JsonString(STRING),
              JsonArray(seq(JsonValue)),
              JsonObject(STRING +-> JsonValue)

Free Types are inductive data types. They are not standard B, but stem from Z and Rodin's theory plug-in.

JsonValue maps quite naturally to the specification of JSON itself.

LibraryJSON.def contains the definitions for the the external functions to interact with JSON text data:

• READ_JSON(file)
  • Type Signature: STRING --> JsonValue
  • Reads a file path on the disk and parses the contained JSON data into the freetype representation.
  • Warning: this function does external IO and should be guarded by a MAX_OPERATIONS == 0 definition
• READ_JSON_FROM_STRING(contents)
  • Type Signature: STRING --> JsonValue
  • Parses the given JSON text into the freetype representation.
• WRITE_JSON(json, file)
  • Type Signature: JsonValue * STRING (predicate, always returns true)
  • Converts the given JSON data from the freetype representation into text and writes it to the given file path.
  • Warning: this function does external IO and should be guarded by a MAX_OPERATIONS == 0 definition
• WRITE_JSON_TO_STRING(json)
  • Type Signature: JsonValue --> STRING
  • Converts the given JSON data from the freetype representation into text.

You need to include both LibraryJson.def and LibraryJson.mch to interact with JSON. One contains the freetype definition, the other one the external function definitions.

JSON-RPC Library

Implements the JSON-RPC 2.0 protocol.

Despite their names, the LibraryZMQ_RPC libraries also support using NDJSON instead of ZeroMQ.

LibraryZMQ_RPC.mch defines a FREETYPE to represent JSON-RPC response object in a type-safe way:

 RpcResult = RpcSuccess(JsonValue), RpcError(STRING)

LibraryZMQ_RPC.def contains the definitions for the the external functions to interact with JSON RPC as a client or server.

Warning: all of the following functions/predicates/substitutions perform external IO and should be guarded by a MAX_OPERATIONS == 0 definition.

• ZMQ_RPC_INIT(endpoint)
  • Type Signature: STRING --> SOCKET
  • Creates a ZeroMQ client socket for JSON-RPC requests and binds it to the given ZeroMQ endpoint.
• SOCKET_RPC_INIT(port)
  • Type Signature: INTEGER --> SOCKET
  • Creates a plain TCP client socket for JSON-RPC over NDJSON and binds it to the given port.
• ZMQ_RPC_DESTROY(socket)
  • Type Signature: SOCKET (substitution, no return value)
  • Closes the given ZeroMQ or plain TCP socket.
  • Note: despite its name this function works with both ZeroMQ and plain TCP sockets
• ZMQ_RPC_SEND(socket, name, args)
  • Type Signature: (SOCKET*STRING*(STRING+->JsonValue)) --> RpcResult
  • Sends a JSON-RPC request object over the given ZeroMQ or plain TCP socket.
  • Note: despite its name this function works with both ZeroMQ and plain TCP sockets
• SOCKET_RPC_ACCEPT(port)
  • Type Signature: INTEGER --> JsonValue
  • Open a plain TCP server socket, wait for a client to connect, receive a JSON-RPC request object over NDJSON and return it.
• SOCKET_RPC_REPLY(port,rpcresult)
  • Type Signature: (INTEGER * RpcResult) --> BOOL
  • Respond to a previously received JSON-RPC request object with the given JSON-RPC response object. Will always return TRUE.
  • Note: must be called right after SOCKET_RPC_ACCEPT

LibraryZMQ_RPC.def will transitively include LibraryJson.def.

You need to include all of LibraryJson.mch, LibraryZMQ_RPC.def and LibraryZMQ_RPC.mch to interact with JSON-RPC, because the freetype definitions have to be separate from the external function definitions.

Drone Control Example

For a real-world example application, see our cf-srv project for controlling Crazyflie drones using ProB. The drones are radio-controlled using the manufacturer-provided Python library cflib, based on which we implemented a ZeroMQ server (cf_rpc.py) that provides a simple drone control API over JSON-RPC. The client is a B machine (DroneCommunicator.mch), which can then be used to control the drones from a B machine inside ProB.

Client-Server Example Machines

Here is a small example of a server that listens for NDJSON JSON-RPC messages on a plain (non-ZeroMQ) TCP socket. You can run the server by calling probcli Simple_RPC_JSON_Server.mch.

MACHINE Simple_RPC_JSON_Server
// start with probcli Simple_RPC_JSON_Server.mch
// other B Models can connect then to this server with socket := SOCKET_RPC_INIT(9999);
// and send JSON-RPC request to this server via
// result := ZMQ_RPC_SEND(socket, "prob_statistics", {("name" |-> JsonString("prolog-walltime"))})
INCLUDES LibraryZMQ_RPC, LibraryJSON
DEFINITIONS "LibraryZMQ_RPC.def"; "LibraryMeta.def"; "LibraryIO.def"
CONSTANTS Port
PROPERTIES
  Port:NATURAL &
  Port = 9999
VARIABLES
  request, terminated
INVARIANT
  request : JsonValue &
  terminated : BOOL
INITIALISATION
  request := JsonNull || terminated := FALSE
OPERATIONS
  GetRequest = SELECT request = JsonNull & terminated = FALSE THEN
    request := SOCKET_RPC_ACCEPT(Port);
    PRINTF("~nReceived request: ~w~n",[request])
  END;
  b <-- SendSuccessAnswer(Method) = SELECT request /= JsonNull & Method:STRING &
                                   "method"|->JsonString(Method) : JsonObject~(request) &
                                   Method : {"ping", "halt"}
                                   THEN
      b := SOCKET_RPC_REPLY(Port,RpcSuccess(JsonNull)) ||
      request := JsonNull ||
      terminated := bool(Method = "halt")
    END;
  b <-- SendNumberAnswer(Method,Params,Name) = SELECT request /= JsonNull & Method:STRING &
                                   "method"|->JsonString(Method) : JsonObject~(request) &
                                   "params"|->JsonObject(Params) : JsonObject~(request) &
                                   "name"|->JsonString(Name) : Params &
                                   Method : {"prob_statistics"}
                                   THEN
        IF Name:{"now-timestamp", "prolog-walltime", "prolog-runtime"} THEN
          b := SOCKET_RPC_REPLY(Port,RpcSuccess(JsonNumber(real(PROB_STATISTICS(Name)))))
        ELSE
          b := SOCKET_RPC_REPLY(Port,RpcError(```Not Implemented: ${Method}```))
        END
       ||
      request := JsonNull
    END;
  b <-- SendNotImplemented(Method) = SELECT request /= JsonNull & Method:STRING &
                                             "method"|->JsonString(Method) : JsonObject~(request)  &
                                             Method /: {"ping", "halt", "prob_statistics"} THEN
      b := SOCKET_RPC_REPLY(Port,RpcError(```Not Implemented: ${Method}```))
       ||
      request := JsonNull
    END
END

After starting the above server, you can start this client on the same machine, e.g., via probcli Simple_RPC_JSON_client.mch -p MAXINT

MACHINE Simple_RPC_JSON_client
INCLUDES LibraryZMQ_RPC, LibraryJSON
// A small demo client which alternatively sends PING and PROB_STATISTICS requests via JSON RPC to a server
DEFINITIONS "LibraryZMQ_RPC.def"; "LibraryIO.def";
 DRONE_URL == "none"
CONSTANTS Port
PROPERTIES
  Port:NATURAL &
  Port = 9999
VARIABLES socket, count
INVARIANT socket:INTEGER & count:NATURAL
INITIALISATION
   socket := SOCKET_RPC_INIT(9999) ||
   count := MAXINT
OPERATIONS
   result <-- Ping = SELECT count > 1 & count mod 2 = 0THEN
      PRINTF("~nSending PING request on socket ~w (~w left)~n",[socket,count-1]) ;
      result := ZMQ_RPC_SEND(socket, "ping", {}) ;
      PRINTF("Result = ~w~n",[result]) ;
      count := count -1
   END;
   result <-- GetStats = SELECT count > 1  & count mod 2 = 1 THEN
      PRINTF("~nSending PROB_STATISTICS request on socket ~w (~w left)~n",[socket,count-1]) ;
      result := ZMQ_RPC_SEND(socket, "prob_statistics", {("name" |-> JsonString("prolog-walltime"))}) ;
      PRINTF("Result = ~w~n",[result]) ;
      count := count -1
   END;
   result <-- Terminate = SELECT count = 1 THEN
      result := ZMQ_RPC_SEND(socket, "halt", {});
      count := 0;
      PRINTF("~nZMQ_RPC_DESTROY (~w)~n",[socket]) ;
      ZMQ_RPC_DESTROY(socket)
    END
END

Here is a sample log when running the server:

$ probcli Simple_RPC_JSON_Server.mch
% unused_constants(3,[JsonArray,JsonBoolean,RpcResult])
% Runtime for SOLUTION for SETUP_CONSTANTS: 1 ms (walltime: 1 ms)
Opened RPC-JSON socket (for ndjson, UTF8 streams) on port 9999
Client connected: 127.0.0.1
Received request line: {"jsonrpc":"2.0","method":"prob_statistics","params":{"name":"prolog-walltime"},"id":1}
 Prolog: [jsonrpc=string(2.0),method=string(prob_statistics),params=json([name=string(prolog-walltime)]),id=number(1)]

Received request: JsonObject({("id"|->JsonNumber(1.0)),("jsonrpc"|->JsonString("2.0")),("method"|->JsonString("prob_statistics")),("params"|->JsonObject({("name"|->JsonString("prolog-walltime"))}))})
Response for request 1 >>> {"jsonrpc":"2.0","result":3667.0,"id":1}

...

Received request: JsonObject({("id"|->JsonNumber(5.0)),("jsonrpc"|->JsonString("2.0")),("method"|->JsonString("halt")),("params"|->JsonObject({}))})
Response for request 5 >>> {"jsonrpc":"2.0","result":null,"id":5}
Deadlock reached after 12 steps (after SendSuccessAnswer).
VARIABLES (use -v to see constants or -silent to suppress output):
     ( request=JsonNull &
       terminated=TRUE )
% Runtime for -execute: 5 ms (with gc: 5 ms, walltime: 3144 ms); since start: 3 sec 671 ms

Here is a sample log when running the client (starting it after the above server):

$ probcli Simple_RPC_JSON_Client.mch -p MAXINT 5
% unused_constants(10,[JsonArray,JsonBoolean,JsonNull,JsonNumber,JsonObject,JsonValue,Port,RpcError,RpcResult,RpcSuccess])
% Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)

Sending PROB_STATISTICS request on socket -1 (4 left)
Result = RpcSuccess(JsonNumber(3667.0))

Sending PING request on socket -1 (3 left)
Result = RpcSuccess(JsonNull)

Sending PROB_STATISTICS request on socket -1 (2 left)
Result = RpcSuccess(JsonNumber(3669.0))

Sending PING request on socket -1 (1 left)
Result = RpcSuccess(JsonNull)

ZMQ_RPC_DESTROY (-1)
Deadlock reached after 7 steps (after Terminate).
VARIABLES (use -v to see constants or -silent to suppress output):
     ( count=0 &
       socket=-1 )
% Runtime for -execute: 2 ms (with gc: 2 ms, walltime: 70 ms); since start: 0 sec 431 ms