JSON and Sockets: Difference between revisions
(Created page with "ProB contains external functions to read and write JSON data and to communicate via sockets using JSON: * <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data. * <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON communication library either ov...") |
No edit summary |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 3: | Line 3: | ||
* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data. | * <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data. | ||
* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC | * <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON RPC (Remote Procedure Call) library either over regular sockets or ZMQ sockets. | ||
| Line 15: | Line 15: | ||
JsonObject(STRING +-> JsonValue) | JsonObject(STRING +-> JsonValue) | ||
</pre> | </pre> | ||
[[Free Types]] are inductive data types. | |||
They are not standard B, but stem from Z and Rodin's theory plug-in. | They are not standard B, but stem from Z and Rodin's theory plug-in. | ||
| Line 23: | Line 23: | ||
RpcResult = RpcSuccess(JsonValue), RpcError(STRING) | RpcResult = RpcSuccess(JsonValue), RpcError(STRING) | ||
</pre> | </pre> | ||
We have used this library to control Crazyflie drones via ProB: | |||
[[File:prob_drone.jpeg||800px]] | |||
Latest revision as of 07:18, 28 March 2025
ProB contains external functions to read and write JSON data and to communicate via sockets using JSON:
- 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) library either over regular sockets or ZMQ sockets.
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.
LibraryZMQ_RPC.mch defines a FREETYPE to represent RPC in a type-safe way:
RpcResult = RpcSuccess(JsonValue), RpcError(STRING)
We have used this library to control Crazyflie drones via ProB:
