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.

Example Machine

This is an excerpt from the B machine used to communicate with the Crazyflie drone.

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