|
|
| Line 39: |
Line 39: |
| * for solving PROPERTIES | | * for solving PROPERTIES |
| * constraint-based assertion checking (<tt>-cbc_assertions</tt> command for <tt>probcli</tt> or the "Check Assertions on Constants" command in the menu Verify -> Constraint-Based Checking) | | * constraint-based assertion checking (<tt>-cbc_assertions</tt> command for <tt>probcli</tt> 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 | | * in the [[Eval Console]] in the ProB Tcl/Tk version |
| * for the REPL in probcli (<tt>probcli -p KODKOD TRUE -repl</tt>) | | * for the REPL in probcli (<tt>probcli -p KODKOD TRUE -repl</tt>) |
Revision as of 13:51, 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.
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
- 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)
More details