As of version 1.3.5 ProB can make use of Kodkod as an alternate way of solving constraints. Kodkod provides a relational interface to SAT solvers and is also by the Alloy tool.

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

If in addition you want see a graphical representation of the solutions found you can use the following command and open the out.dot file using dotty or GraphViz:

probcli -p KODKOD TRUE -repl -evaldot ~/out.dot

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

What can be translated

• Types:
  • Basic Types: Deferred Sets, enumerated sets, integers, booleans
  • Sets of basic types
  • Relations between basic types
  • Higher-order types (sets of sets) are not supported

• Operators:
  • Predicates: &, or, =>, <=>, not, !, #, =, /=
  • Booleans: TRUE, FALSE, BOOL, bool(...)
  • Sets: {..,...} {x|P}, POW, card, Cartesian product, \/, /\, -, :, /:, /<:, <<: /<<:
  • Numbers: n..m, >, <, >=, <=, +, -, *, SIGMA(x).(P|x)
  • Relations: <->, |->, dom, ran, id, <|, <<|, |>, |>>, ~, [...], <+, prj1, prj2, closure1
  • x : S+->T, x:S-->T, ..., lambda
  • currently no operations on sequences are supported

• Some limitations:
  • If integers are used, a predicate can only be translated if a static analysis can estimate the interval of its possible values.
  • Generally only complete predicates are translated or nothing at all, unless you set the KODKOD_ONLY_FULL preference to FALSE.

When is the Kokod translation used

Once enabled, the Kodkod translation will be used in the following circumstances:

• 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)
• constraint-based deadlock checking
• in the Eval Console in the ProB Tcl/Tk version
• for the REPL in probcli (probcli -p KODKOD TRUE -repl)

SAT solver

By default Kodkod in ProB uses the bundled SAT4J solver. You can switch to using minisat by putting a current version of libminisat.jnilib into ProB's lib directory.

Similarly, as of ProB 1.6.1-beta5 you can also use the Solver lingeling or glucose by dropping liblingeling.dylib or libglucose.dylib into ProB's lib folder (for Mac OS X; for Linux the extension will be different).

These files can be downloaded from the Kodkod download site.

More details

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