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

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.

When is the Kokod translation used

• for solving PROPERTIES
• in the Eval console in Tcl/Tk
• for the REPL in probcli (probcli -p KODKOD TRUE -repl)

More details

• Link to FM'2012 paper