Revision as of 12:33, 31 October 2012

As of version 1.3.5 ProB can make use of Kodkod as an alternate way of solving constraints.

How to enable Kodkod

For the command-line version you need to call prob as follows:

probcli -p KODKOD TRUE

Note: to experiment with Kodkod you may want to try out the command:

probcli -p KODKOD TRUE -repl

For the ProB Tcl/Tk Version you should select the menu command "Enable Kodkod for Properties" in the Preferences menu.

First-order relations and sets, numbers, booleans.

Generally only complete predicate translated or nothing at all, unless you set the KODKOD_ONLY_FULL preference to FALSE.

for solving PROPERTIES
constraint-based assertion checking (-cbc_assertions command for probcli or the "Check Assertions on Constants" command in the menu Verify -> Constraint-Based Checking)
in the Eval Console in the ProB Tcl/Tk version
for the REPL in probcli (probcli -p KODKOD TRUE -repl)

@@ Line 23: / Line 23: @@
 * for solving PROPERTIES
-* constraint-based assertion checking (<tt>-cbc_assertions</tt> command for <tt>probcli</tt> or the Assertion Checking command in the Verify menu)
+* constraint-based assertion checking (<tt>-cbc_assertions</tt> command for <tt>probcli</tt> or the "Check Assertions on Constants" command in the menu Verify -> Constraint-Based Checking)
 * in the [[Eval Console]] in the ProB Tcl/Tk version
 * for the REPL in probcli (<tt>probcli -p KODKOD TRUE -repl</tt>)