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).
06:45, 24 July 2026Michael Leuscheltalkcontribs created page CNF(Created page with "As of version 1.16.0 ProB can directly open .cnf files encoding SAT problems in conjunctive normal form. These files get translated into a B model, which has an accompanying custom graph visualisation. The backend is also set to use B2SAT. The B translation also contains an encoding of the clauses. VisB can be used to visualise the solutions. You can use the console to examine the clauses and the solution.")
09:07, 10 July 2026Michael Leuscheltalkcontribs created page Strings(Created page with "ProB supports the <tt>STRING</tt> data type also provided by Atelier-B. However, ProB provides considerable additional features described below. == Literals == <pre> "astring" a specific (single-line) string value '''astring''' an alternate way of writing (multi-line) strings, no need to escape " ```tstring``` template strings, where ${Expr} or $«Expr» parts are evaluated and converted to string, you can provide options separated by commas i...")
13:31, 19 March 2026Michael Leuscheltalkcontribs created page B2ASP(Created page with "The current versions of ProB can make use the clingo ASP solver as an alternate way of solving constraints. This backend translates a subset of B formulas to SAT by encoding the formulas in ASP (Answer Set Programming) first and then using clingo to translate this to SAT and solve it. B2ASP solving consists of the following phases: * a CLP(FD) based bounds analysis to infer finite bounds for all variables, * a translation of set theory and B to ASP programs (aka Horn c...")
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...")
