Combined display of all available logs of ProB Documentation.
You can narrow down the view by selecting a log type, the username (case-sensitive), or the affected page (also case-sensitive).
07:13, 28 March 2025Michael Leuscheltalkcontribs created page JSON and Sockets(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...")
06:55, 22 February 2025Michael Leuscheltalkcontribs created page Implication inside an Existential Quantifier(Created 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...")
07:17, 8 February 2025Michael Leuscheltalkcontribs created page ProB REPL(Created page with "== The REPL of ProB == ProB provides various consoles, also called REPL (Read-Eval-Print-Loop). A REPL (Read-Eval-Print-Loop) or console can be used to evaluate formulas with ProB or issue other commands. ProB provides various REPLs, depending on which version of ProB you use: * The REPL in probcli can be started with the command <tt>-repl</tt> * The REPL in ProB Tcl/Tk is the Eval Console. * ProB2-UI also provides a console view Below we describe th...")
09:08, 23 April 2024Michael Leuscheltalkcontribs created page B2SAT(Created page with " The current versions of ProB can make use of the new B2SAT backend as an alternate way of solving constraints. It translates a subset of B formulas to SAT and for solving by an external SAT solver. == Using B2SAT == === B2SAT in the REPL === === B2SAT for PROPERTIES === The new preference SOLVER_FOR_PROPERTIES can be used to specify solver for PROPERTIES (axioms) when setting up constants. The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt...")
12:02, 22 April 2024Vellatalkcontribs created page Freetypes(Created page with "Freetypes exist in Z and in the Rodin theory plugin and are supported by ProB. You can also define new freetypes in classical B by adding a FREETYPES clause with equations separated by semicolon. Here is a definition of an inductive type IntList for lists of integers constructed using inil and icons: <pre> FREETYPES IntList = inil, icons(INTEGER*IntList) </pre>")
