07:1307:13, 28 March 2025diffhist+1,259 N
JSON and SocketsCreated 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..."
06:5506:55, 22 February 2025diffhist+492 N
Implication inside an Existential QuantifierCreated page with " With version 1.15 ProB produces a warning if you use an implication inside an existential quantifier. Here we explain why. Take a look at <pre> f: 1..3 --> NAT & f = [0,0,0] & #i.(i:dom(f) => f(i)>0) </pre> You may be surprised to learn that the existential quantifier on the third line is true, even though no element of the array f is greater than 0. Indeed, for i=0 or i=-1 or i=4 the body of the quantifier is true as <tt>i:dom(f)</tt> is false and hence the imp..."
