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.

What can be translated

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.

When is the Kokod translation used

• for solving PROPERTIES
• constraint-based assertion checking (-cbc_assertions command for probcli or the Assertion Checking command in the Verify menu)
• in the Eval Console in the ProB Tcl/Tk version
• for the REPL in probcli (probcli -p KODKOD TRUE -repl)

More details

• Plagge, Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. FM'2012, LNCS 7436.