Using ProB with KODKOD - Revision history

Michael Leuschel at 16:37, 27 January 2021

2021-01-27T16:37:11Z

← Older revision		Revision as of 16:37, 27 January 2021
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 the heart of 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 54:		Line 54:
	You can control the solver being used using the <tt>KODKOD_SAT_SOLVER</tt> preference (which has four possible values: sat4j, minisat, lingeling, glucose).		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 [~~http~~://~~alloy~~.~~mit~~.~~edu~~/kodkod/~~download.html~~ Kodkod download site].		These files can be downloaded from the [https://emina.github.io/kodkod/ Kodkod download site].

	= More Preferences =		= More Preferences =

Michael Leuschel at 14:40, 26 July 2017

2017-07-26T14:40:54Z

← Older revision		Revision as of 14:40, 26 July 2017
Line 3:		Line 3:

	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 [http://alloy.mit.edu/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 [http://alloy.mit.edu/alloy/ Alloy] tool.

	= How to enable Kodkod =		= How to enable Kodkod =

Michael Leuschel: /* More details */

2017-07-06T09:16:24Z

More details

← Older revision		Revision as of 09:16, 6 July 2017
Line 76:		Line 76:
	You can also have a look at these Wiki pages:		You can also have a look at these Wiki pages:
	* [[Proving_Theorems_in_the_ProB_REPL]]		* [[Proving_Theorems_in_the_ProB_REPL]]
	* [[Argumentation_Theory Argumentation Theory Example]]		* [[Argumentation_Theory\|Argumentation Theory Example]]

Michael Leuschel: /* More details */

2017-07-06T09:16:03Z

More details

← Older revision		Revision as of 09:16, 6 July 2017
Line 73:		Line 73:

	* [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)]		* [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]]

Michael Leuschel: /* More details */

2017-07-06T09:11:53Z

More details

← Older revision		Revision as of 09:11, 6 July 2017
Line 72:		Line 72:
	= 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)]

Michael Leuschel: /* More Preferences */

2016-10-06T10:52:13Z

More Preferences

← Older revision		Revision as of 10:52, 6 October 2016
Line 58:		Line 58:
	= More Preferences =		= More Preferences =

	If you set <tt>KODKOD_ONLY_FULL</tt> to <tt>FALSE</tt>, then		If you set <tt>KODKOD_ONLY_FULL</tt> to <tt>FALSE</tt>, then the Kodkod translation can be applied to part of a predicate.
	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>.		You can also enable symmetry by using the preference <tt>KODKOD_SYMMETRY</tt>.
Line 68:		Line 68:

	Finally, you can control the number of solutions that Kodkod computes in one go using the preference <tt>KODKOD_MAX_NR_SOLS</tt>.		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 TRUE, then you should set this value to 1.		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].		* [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].

Michael Leuschel: /* SAT solver */

2016-10-06T10:51:02Z

SAT solver

← Older revision		Revision as of 10:51, 6 October 2016
Line 55:		Line 55:

	These files can be downloaded from the [http://alloy.mit.edu/kodkod/download.html Kodkod download site].		These files can be downloaded from the [http://alloy.mit.edu/kodkod/download.html 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.

	You can also enable symmetry by using the preference <tt>KODKOD_SYMMETRY</tt>.		You can also enable symmetry by using the preference <tt>KODKOD_SYMMETRY</tt>.

Michael Leuschel: /* SAT solver */

2016-10-06T10:49:46Z

SAT solver

← Older revision		Revision as of 10:49, 6 October 2016
Line 52:		Line 52:

	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).		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 [http://alloy.mit.edu/kodkod/download.html Kodkod download site].		These files can be downloaded from the [http://alloy.mit.edu/kodkod/download.html Kodkod download site].

			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 TRUE, 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].		* [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].

Michael Leuschel: /* SAT solver */

2016-10-04T14:59:22Z

SAT solver

← Older revision		Revision as of 14:59, 4 October 2016
Line 51:		Line 51:
	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.		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>lingeling</b> or <b>~~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).		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).

	These files can be downloaded from the [[http://alloy.mit.edu/kodkod/download.html Kodkod download site]].		These files can be downloaded from the [http://alloy.mit.edu/kodkod/download.html Kodkod download site].

	= 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].		* [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].

Michael Leuschel: /* SAT solver */

2016-10-04T14:56:47Z

SAT solver

← Older revision		Revision as of 14:56, 4 October 2016
Line 51:		Line 51:
	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.		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>lingeling</b> or <b>Glucose</b> by dropping		Similarly, as of ProB 1.6.1-beta5 you can also use the Solver <b>lingeling</b> or <b>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).
	<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).

	These files can be downloaded from the [[http://alloy.mit.edu/kodkod/download.html Kodkod download site]].		These files can be downloaded from the [[http://alloy.mit.edu/kodkod/download.html Kodkod download site]].