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 either over regular sockets or ZMQ 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 protocol.

Despite their names the LibraryZMQ_RPC libraries can use both ZeroMQ library and native sockets.

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:

• ZMQ_RPC_INIT(endpoint)
  • Type Signature: STRING --> SOCKET
  • Creates a ZMQ socket for RPC with the ZMQ library and binds it to the given endpoint.
  • Warning: this function does external IO and should be guarded by a MAX_OPERATIONS == 0 definition
• SOCKET_RPC_INIT(port)
  • Type Signature: INTEGER --> SOCKET
  • Creates a native socket for RPC and binds it to the given port.
  • Warning: this function does external IO and should be guarded by a MAX_OPERATIONS == 0 definition
• ZMQ_RPC_DESTROY(socket)
  • Type Signature: SOCKET (substitution, no return value)
  • Closes the given ZMQ or native socket.
  • Note: despite its name this function works with both ZMQ and native sockets
  • Warning: this substitution does external IO and should be guarded by a MAX_OPERATIONS == 0 definition
• ZMQ_RPC_SEND(socket, name, args)
  • Type Signature: (SOCKET*STRING*(STRING+->JsonValue)) --> RpcResult
  • Sends a JSON-RPC request object over the given ZMQ or native socket.
  • Note: despite its name this function works with both ZMQ and native sockets
  • Warning: this function does external IO and should be guarded by a MAX_OPERATIONS == 0 definition
• SOCKET_RPC_ACCEPT(port)
  • Type Signature: INTEGER --> JsonValue
  • Open a native server socket, wait for a client to connect, receive a JSON-RPC request object and return it.
  • Warning: this function does external IO and should be guarded by a MAX_OPERATIONS == 0 definition
• 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
  • Warning: this function does external IO and should be guarded by a MAX_OPERATIONS == 0 definition

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.

Client-Server Example Machines

Here is a small example of a server that listens on a classical (non-ZMQ) 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) 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

Drone Example Machine

This is an excerpt from the B machine used to communicate with the Crazyflie drone. Parallel to this a Python script is running, which implements all the JSON-RPC methods and uses cflib to communicate with the drone over radio.

MACHINE DroneCommunicator USES LibraryJSON, LibraryZMQ_RPC
DEFINITIONS
  "LibraryZMQ_RPC.def";
  "LibraryReals.def";
  SET_PREF_MAX_OPERATIONS == 0;
CONSTANTS DRONE_URL
PROPERTIES DRONE_URL:STRING & DRONE_URL = "radio://0/80/2M/5700B500F7"
VARIABLES init, socket, cycle
INVARIANT
  init:BOOL &
  socket:SOCKET &
  cycle:INTEGER
INITIALISATION
  init := FALSE;
  socket := 0;
  cycle := 1

OPERATIONS
  Init = 
  SELECT init = FALSE THEN
    socket := ZMQ_RPC_INIT("tcp://localhost:22272");
    init := TRUE
  END;

  Destroy =
  SELECT init = TRUE THEN
    ZMQ_RPC_DESTROY(socket);
    init := FALSE
  END;

  register_sensors = 
  SELECT init = TRUE THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "register_log", {
        ("url" |-> JsonString(DRONE_URL)),
        ("name" |-> JsonString("Telemetry")),
        ("variables" |-> JsonArray([
          JsonString("stateEstimate.x"),
          JsonString("stateEstimate.y"),
          JsonString("stateEstimate.z"),
          JsonString("stateEstimate.roll"),
          JsonString("stateEstimate.pitch"),
          JsonString("stateEstimate.yaw")
        ]))}));
    END
  END;

  Drone_Takeoff = 
  SELECT init = TRUE THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "takeoff", {("url" |-> JsonString(DRONE_URL))}))
    END
  END;

  Drone_Land = 
  SELECT init = TRUE THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "land", {("url" |-> JsonString(DRONE_URL))}))
    END
  END;

  Drone_Left(dist) = 
  SELECT
    init = TRUE &
    dist : 0..2000
  THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "left", {("url" |-> JsonString(DRONE_URL)), ("distance" |-> JsonNumber(RDIV(real(dist), real(1000))))}))
    END
  END;

  Drone_Right(dist) = 
  SELECT
    init = TRUE &
    dist : 0..2000
  THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "right", {("url" |-> JsonString(DRONE_URL)), ("distance" |-> JsonNumber(RDIV(real(dist), real(1000))))}))
    END
  END;

  Drone_Up(dist) = 
  SELECT
    init = TRUE &
    dist : 0..2000
  THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "up", {("url" |-> JsonString(DRONE_URL)), ("distance" |-> JsonNumber(RDIV(real(dist), real(1000))))}))
    END
  END;

  Drone_Down(dist) = 
  SELECT
    init = TRUE &
    dist : 0..2000
  THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "down", {("url" |-> JsonString(DRONE_URL)), ("distance" |-> JsonNumber(RDIV(real(dist), real(1000))))}))
    END
  END;

  Drone_Forward(dist) = 
  SELECT
    init = TRUE &
    dist : 0..2000
  THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "forward", {("url" |-> JsonString(DRONE_URL)), ("distance" |-> JsonNumber(RDIV(real(dist), real(1000))))}))
    END
  END;

  Drone_Backward(dist) = 
  SELECT
    init = TRUE &
    dist : 0..2000
  THEN
    VAR res IN
      res := RpcSuccess~(ZMQ_RPC_SEND(socket, "backward", {("url" |-> JsonString(DRONE_URL)), ("distance" |-> JsonNumber(RDIV(real(dist), real(1000))))}))
    END
  END;

  out <-- Drone_GetX = 
  SELECT init = TRUE THEN
    out := floor(1000.0 * JsonNumber~(RpcSuccess~(ZMQ_RPC_SEND(socket, "get_log_var", {("url" |-> JsonString(DRONE_URL)), ("name" |-> JsonString("stateEstimate.x"))}))));
    cycle := cycle + 1
  END
END