(Created page with 'Category:User Manual Category:Stubs 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 comman…') |
No edit summary |
||
| Line 2: | Line 2: | ||
[[Category:Stubs]] | [[Category:Stubs]] | ||
As of version 1.3.5 ProB can make use of Kodkod as an alternate way of solving constraints. | As of version 1.3.5 ProB can make use of [http://alloy.mit.edu/kodkod/ Kodkod] as an alternate way of solving constraints. | ||
= How to enable Kodkod = | = How to enable Kodkod = | ||
| Line 18: | Line 18: | ||
* for solving PROPERTIES | * for solving PROPERTIES | ||
* in the Eval | * 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>) | ||
= 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]. | ||
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
For the ProB Tcl/Tk Version you should select the menu command "Enable Kodkod for Properties" in the Preferences menu.
First-order relations and sets, numbers, booleans.