Revision as of 13:50, 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.

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

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.

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 16: / Line 16: @@
 = What can be translated =
-First-order relations and sets, numbers, booleans.
+* 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
-Generally only complete predicate translated or nothing at all, unless you set the <tt>KODKOD_ONLY_FULL</tt> preference to FALSE.
+* 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 <tt>KODKOD_ONLY_FULL</tt> preference to FALSE.
 = When is the Kokod translation used =