Using ProB with KODKOD: Difference between revisions

No edit summary
 
(10 intermediate revisions by the same user not shown)
Line 2: Line 2:
[[Category:Stubs]]
[[Category:Stubs]]


As of version 1.3.5 ProB can make use of [http://alloy.mit.edu/kodkod/ Kodkod] as an alternate way of solving constraints.
As of version 1.3.5 ProB can make use of [https://emina.github.io/kodkod/ Kodkod] as an alternate way of solving constraints.
Kodkod provides a relational interface to SAT solvers and is also by the [http://alloy.mit.edu/alloy/ Alloy]  tool.
Kodkod provides a relational interface to SAT solvers and is the heart of the [https://alloytools.org Alloy]  tool.


= How to enable Kodkod =
= How to enable Kodkod =
Line 49: Line 49:
= SAT solver =
= SAT solver =
By default Kodkod in ProB uses the bundled SAT4J solver.
By default Kodkod in ProB uses the bundled SAT4J solver.
You can switch to using minisat by putting a current version of <tt>libminisat.jnilib</tt> into ProB's <tt>lib</tt> directory.
You can switch to using <b>minisat</b> by putting a current version of <tt>libminisat.jnilib</tt> into ProB's <tt>lib</tt> directory.
 
Similarly, as of ProB 1.6.1-beta5 you can also use the Solver <b>[http://fmv.jku.at/lingeling/ lingeling]</b> or <b>[http://www.labri.fr/perso/lsimon/glucose/ glucose]</b> by dropping <tt>liblingeling.dylib</tt> or <tt>libglucose.dylib</tt>  into ProB's lib folder (for Mac OS X; for Linux the extension will be different).
You can control the solver being used using the <tt>KODKOD_SAT_SOLVER</tt> preference (which has four possible values: sat4j, minisat, lingeling, glucose).
 
These files can be downloaded from the [https://emina.github.io/kodkod/ Kodkod download site].
 
= More Preferences =
 
If you set <tt>KODKOD_ONLY_FULL</tt> to <tt>FALSE</tt>, then the Kodkod translation can be applied to part of a predicate.
In other words, the predicate (such as the PROPERTIES) are partitioned into two parts: one that can be understood by Kodkod and the rest which will be dealt with by ProB's solver.
 
You can also enable symmetry by using the preference <tt>KODKOD_SYMMETRY</tt>.
By default, ProB will set this value to 0, i.e., symmetry is off.
This means that Kodkod can also be used within set comprehensions.
By setting the preference to a value higher than 0 you will enable symmetry within Kodkod, which may mean that not all solutions will be returned.
Setting the value too high may be counter productive; Kodkod's recommended default is 20.
 
Finally, you can control the number of solutions that Kodkod computes in one go using the preference <tt>KODKOD_MAX_NR_SOLS</tt>.
E.g., if you are interested in only one solution and <tt>KODKOD_ONLY_FULL</tt> is <tt>TRUE</tt>, then you should set this value to 1.


= More details =
= More details =


* [http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Plagge, Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. FM'2012, LNCS 7436].
* [https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf Plagge, Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. In Proceedings FM'2012, Dimitra Giannakopoulou and Dominique Méry, LNCS 7436, Springer, 372--386, 2012. (pdf)]
 
You can also have a look at these Wiki pages:
* [[Proving_Theorems_in_the_ProB_REPL]]
* [[Argumentation_Theory|Argumentation Theory Example]]

Latest revision as of 16:37, 27 January 2021


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 the heart of 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). You can control the solver being used using the KODKOD_SAT_SOLVER preference (which has four possible values: sat4j, minisat, lingeling, glucose).

These files can be downloaded from the Kodkod download site.

More Preferences

If you set KODKOD_ONLY_FULL to FALSE, then the Kodkod translation can be applied to part of a predicate. In other words, the predicate (such as the PROPERTIES) are partitioned into two parts: one that can be understood by Kodkod and the rest which will be dealt with by ProB's solver.

You can also enable symmetry by using the preference KODKOD_SYMMETRY. By default, ProB will set this value to 0, i.e., symmetry is off. This means that Kodkod can also be used within set comprehensions. By setting the preference to a value higher than 0 you will enable symmetry within Kodkod, which may mean that not all solutions will be returned. Setting the value too high may be counter productive; Kodkod's recommended default is 20.

Finally, you can control the number of solutions that Kodkod computes in one go using the preference KODKOD_MAX_NR_SOLS. E.g., if you are interested in only one solution and KODKOD_ONLY_FULL is TRUE, then you should set this value to 1.

More details

You can also have a look at these Wiki pages: