Line 16: | Line 16: | ||

= What can be translated = | = 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 | |||

Generally only complete | * 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 = | = When is the Kokod translation used = |

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

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

- 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.

- 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`)