D45 Model Checking - Revision history

imported>Tommy at 21:35, 20 April 2012

2012-04-20T21:35:25Z

← Older revision		Revision as of 21:35, 20 April 2012
Line 81:		Line 81:
	The research on further compression technique is ongoing and will be continued within the project ADVANCE[http://www.advance-ict.eu/].		The research on further compression technique is ongoing and will be continued within the project ADVANCE[http://www.advance-ict.eu/].
	The work on the Theory plug-in support is currently suspended until the Theory plug-in provides the features described earlier.		The work on the Theory plug-in support is currently suspended until the Theory plug-in provides the features described earlier.

			= References =
			<references/>

	[[Category:D45 Deliverable]]		[[Category:D45 Deliverable]]

imported>Tommy: /* Available Documentation */

2012-04-20T21:34:34Z

Available Documentation

← Older revision		Revision as of 21:34, 20 April 2012
Line 70:		Line 70:
	= Available Documentation =		= Available Documentation =

	* [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB ~~Command~~-~~Line Version~~ of ~~ProB]~~		* A manual is available on using command line version of ProB <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB</ref>
	* [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HaLe2011 Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011, Cambridge University Press, 2011.]		* A paper has been published on constraint-based deadlock checking of high-level specifications<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HaLe2011 Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011, Cambridge University Press, 2011.</ref>
	* [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 ~~Translating~~ TLA+ to B and experiments with TLC]		* A report<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012</ref> on the translation from TLA+ to B and experiments with TLC has been published.

	= Status =		= Status =

imported>Tommy: /* New Features */

2012-04-20T21:30:09Z

New Features

← Older revision		Revision as of 21:30, 20 April 2012
Line 23:		Line 23:

	== New Features ==		== New Features ==
	~~===~~ Experiments with Theory Plugin ~~===~~		''' Experiments with Theory Plugin '''

	Animating models that use the Theory plug-in is currently not possible. However, we prepared ProB's translation from Event-B into its internal representation in order to support user defined operators from the Theory plug-in. The work on the feature is currently suspended until the Theory plug-in supports accessing the definitions.		Animating models that use the Theory plug-in is currently not possible. However, we prepared ProB's translation from Event-B into its internal representation in order to support user defined operators from the Theory plug-in. The work on the feature is currently suspended until the Theory plug-in supports accessing the definitions.

	~~===~~ Improved detection of infinite functions, and improved support for them~~===~~		''' Improved detection of infinite functions, and improved support for them '''


Line 36:		Line 36:
	These warnings are not yet displayed in the Rodin version, but are visible in probcli and ProB Tcl/Tk.		These warnings are not yet displayed in the Rodin version, but are visible in probcli and ProB Tcl/Tk.

	~~===~~ Support of finite operator~~===~~		''' Support of finite operator '''

	The finite operator was previously ignored, as ProB only supported finite sets anyway.		The finite operator was previously ignored, as ProB only supported finite sets anyway.

imported>Tommy at 12:07, 19 April 2012

2012-04-19T12:07:35Z

← Older revision		Revision as of 12:07, 19 April 2012
Line 50:		Line 50:
	We also developed an integration of our translation into ProB.		We also developed an integration of our translation into ProB.
	ProB thus now provides a complementary tool to the explicit state model checker TLC, with convenient animation and constraint solving for TLA+.		ProB thus now provides a complementary tool to the explicit state model checker TLC, with convenient animation and constraint solving for TLA+.
	More importantly for ~~Deploy~~, we have conducted a series of case studies, highlighting the complementarity to TLC. In particular, we have highlighted the sometimes dramatic difference in performance when it comes to solving complicated constraints in TLA+. Also, the benchmarks have allowed us to pinpoint some areas where ProB could be further improved. This also led to some of the compression techniques mentioned earlier.		More importantly for DEPLOY, we have conducted a series of case studies, highlighting the complementarity to TLC. In particular, we have highlighted the sometimes dramatic difference in performance when it comes to solving complicated constraints in TLA+. Also, the benchmarks have allowed us to pinpoint some areas where ProB could be further improved. This also led to some of the compression techniques mentioned earlier.

	= Motivations =		= Motivations =

	The motivations for the state space compression arose from experiments in WP3 (space), and from applications of ProB outside of ~~Deploy~~.		The motivations for the state space compression arose from experiments in WP3 (space), and from applications of ProB outside of DEPLOY.

	The need for constraint-based deadlock checking arose in the automotive work package, more precisely during the elaboration of the cruise control system. Here, proving turned out to be impractical and ProB was used to find deadlocks and guide the development of the model.		The need for constraint-based deadlock checking arose in the automotive work package, more precisely during the elaboration of the cruise control system. Here, proving turned out to be impractical and ProB was used to find deadlocks and guide the development of the model.

imported>Tommy: /* Constraint-Based Checking */

2012-04-19T12:06:51Z

Constraint-Based Checking

← Older revision		Revision as of 12:06, 19 April 2012
Line 19:		Line 19:
	== Constraint-Based Checking ==		== Constraint-Based Checking ==

	Improved ~~Constraint~~-based checking for deadlocks, invariants and event sequences (used in MBT).		Improved constraint-based checking for deadlocks, invariants and event sequences (used in MBT).
	In addition, many improvements in constraint solving kernel were implemented.		In addition, many improvements in constraint solving kernel were implemented.

imported>Tommy: /* State Space Reduction, Compression and Hashing */

2012-04-19T12:06:09Z

State Space Reduction, Compression and Hashing

← Older revision		Revision as of 12:06, 19 April 2012
Line 9:		Line 9:
	A first step was to implement a first version of state compression, whereby we simplify stored states so that they require less memory. This was achieved without compromising speed and is now always activated.		A first step was to implement a first version of state compression, whereby we simplify stored states so that they require less memory. This was achieved without compromising speed and is now always activated.
	Furthermore, if the preference <tt>COMPRESSION</tt> is set to true, then ProB will also detect common (sub-)expressions in states and store the common expressions only once.		Furthermore, if the preference <tt>COMPRESSION</tt> is set to true, then ProB will also detect common (sub-)expressions in states and store the common expressions only once.
	~~E.g.~~, when several states have the same same value for a given variable <tt>x</tt> then its value will only be stored just once. This is particularly useful when complicated variables only change infrequently.		For example, when several states have the same same value for a given variable <tt>x</tt> then its value will only be stored just once. This is particularly useful when complicated variables only change infrequently.

	Related to this aspect, the hashing of ProB states was improved on 64-bit architectures, which is also important in the context of detecting common subexpressions for sharing (common subexpressions are detected by hashing).		Related to this aspect, the hashing of ProB states was improved on 64-bit architectures, which is also important in the context of detecting common subexpressions for sharing (common subexpressions are detected by hashing).

imported>Tommy: /* Status */

2012-03-27T15:18:19Z

Status

← Older revision		Revision as of 15:18, 27 March 2012
Line 79:		Line 79:
	For example, the improved hashing and light-weight state compression is available in the current release of ProB.		For example, the improved hashing and light-weight state compression is available in the current release of ProB.
	The SHA1 hash technique is not available in the current release.		The SHA1 hash technique is not available in the current release.
	The research on further compression technique is ongoing and will be continued within the project ADVANCE.		The research on further compression technique is ongoing and will be continued within the project ADVANCE[http://www.advance-ict.eu/].
	The work on the Theory plug-in support is currently suspended until the Theory plug-in provides the features described earlier.		The work on the Theory plug-in support is currently suspended until the Theory plug-in provides the features described earlier.

	[[Category:D45 Deliverable]]		[[Category:D45 Deliverable]]

imported>Tommy: /* Status */

2012-03-26T14:49:00Z

Status

← Older revision		Revision as of 14:49, 26 March 2012
Line 76:		Line 76:
	= Status =		= Status =

	All improvements, unless explicitly ~~state~~ below, are accessible in the latest release of ProB.		All improvements, unless explicitly stated below, are accessible in the latest release of ProB.
	For example, the improved hashing and light-weight state compression is available in the current release of ProB.		For example, the improved hashing and light-weight state compression is available in the current release of ProB.
	The SHA1 hash technique is not available in the current release.		The SHA1 hash technique is not available in the current release.

imported>Tommy: /* Experiments with Theory Plugin */

2012-03-26T14:42:55Z

Experiments with Theory Plugin

← Older revision		Revision as of 14:42, 26 March 2012
Line 26:		Line 26:

	Animating models that use the Theory plug-in is currently not possible. However, we prepared ProB's translation from Event-B into its internal representation in order to support user defined operators from the Theory plug-in. The work on the feature is currently suspended until the Theory plug-in supports accessing the definitions.		Animating models that use the Theory plug-in is currently not possible. However, we prepared ProB's translation from Event-B into its internal representation in order to support user defined operators from the Theory plug-in. The work on the feature is currently suspended until the Theory plug-in supports accessing the definitions.


	=== Improved detection of infinite functions, and improved support for them===		=== Improved detection of infinite functions, and improved support for them===

imported>Leuschel: /* Choices / Decisions */

2012-03-15T15:20:18Z

Choices / Decisions

← Older revision		Revision as of 15:20, 15 March 2012
Line 62:		Line 62:

	= Choices / Decisions =		= Choices / Decisions =
	~~{{TODO}} To be completed.~~

	Aggressive compression can also induce a performance penalty.		Aggressive compression can also induce a performance penalty.