ADVANCE D3.2 Model Checking - Revision history

imported>Tommy: /* Motivations / Decisions */

2012-06-26T09:47:42Z

Motivations / Decisions

← Older revision		Revision as of 09:47, 26 June 2012
Line 64:		Line 64:
	'''CSP and B'''<br>		'''CSP and B'''<br>
	ProB supports also other formalisms like CSP. CSP can also be used to guide B and Event-B models and can also be used for specifying scenarios or for model testing.		ProB supports also other formalisms like CSP. CSP can also be used to guide B and Event-B models and can also be used for specifying scenarios or for model testing.
	Within the project this feature of ProB was continuously maintained and improved. We have extended the implementation of the CSP interpreter and animator to be able to support more complex and larger data types (e.g. mixing of dot and non-associative tuples) as well as supporting more complicated pattern matching inside set ~~comprehensions~~ and function definitions. Some effort for supporting more of CSP built-in functions (like seq(-), set(-) and card(-))was made as well.		Within the project this feature of ProB was continuously maintained and improved. We have extended the implementation of the CSP interpreter and animator to be able to support more complex and larger data types (e.g. mixing of dot and non-associative tuples) as well as supporting more complicated pattern matching inside set comprehension formulas and function definitions. Some effort for supporting more of CSP built-in functions (like seq(-), set(-) and card(-))was made as well.
	Finally, ProB now supports checking LTL-assertions directly from the CSP model by using pragmas ({-# assert_ltl = … #-}). The syntax is the same as for LTL-assertions in ~~DEFINTION~~ clauses in B models.		Finally, ProB now supports checking LTL-assertions directly from the CSP model by using pragmas ({-# assert_ltl = … #-}). The syntax is the same as for LTL-assertions in DEFINITION clauses of B models.

	= Available Documentation =		= Available Documentation =

imported>Tommy: /* Available Documentation */

2012-06-26T09:42:30Z

Available Documentation

← Older revision		Revision as of 09:42, 26 June 2012
Line 71:		Line 71:
	'''Constraint Solving'''<br>		'''Constraint Solving'''<br>
	The improvements are available in the nightly builds of ProB.<br>		The improvements are available in the nightly builds of ProB.<br>
	Two specific pages ~~have been added to the ProB user manual:~~ <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Recursively_Defined_Functions Recursive functions entry in ProB user manual</ref>, <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/External_Functions External functions entry in ProB user manual</ref>.		Two specific pages<ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Recursively_Defined_Functions Recursive functions entry in ProB user manual</ref><ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/External_Functions External functions entry in ProB user manual</ref> have been added to the ProB user manual.

	'''TLA2B'''<br>		'''TLA2B'''<br>
	The TLA+ to B translation has been published at the iFM'2012 conference. A technical report is available<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 Translating TLA+ to B for Validation with ProB. Technical Report, 2012.</ref>		The TLA+ to B translation has been published at the iFM'2012 conference. A technical report is also available.<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 Translating TLA+ to B for Validation with ProB. Technical Report, 2012.</ref>
	A presentation at the FM'2012 TLA+ workshop will also be made.		A presentation at the FM'2012 TLA+ workshop will also be made, and a dedicated page<ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA TLA2B entry in ProB user manual</ref> has been added to the ProB user manual.
	A page ~~has been added to the ProB user manual:~~ <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA TLA2B entry in ProB user manual</ref>.

	'''Physical Units'''<br>		'''Physical Units'''<br>
	This work is still in progress. A first tutorial page ~~is available in the ProB online documentation~~ <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Unit_Plugin Unit Plug-in Tutorial entry in ProB user manual</ref>. Full documentation will be made available later in the project.		This work is still in progress. A first tutorial page<ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Unit_Plugin Unit Plug-in Tutorial entry in ProB user manual</ref> is available in the ProB online documentation. Full documentation will be made available later in the project.
	The latest nightly build of ProB contains an experimental version of the analysis.		The latest nightly build of ProB contains an experimental version of the analysis.

	'''Kodkod'''<br>		'''Kodkod'''<br>
	A technical report ~~has been published on the validation using ProB and Kodkod~~ <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Validating B,Z and TLA+ using ProB and Kodkod. Technical Report, 2012.</ref>. The paper has been accepted for FM'2012.		A technical report<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Validating B,Z and TLA+ using ProB and Kodkod. Technical Report, 2012.</ref> has been published on the validation using ProB and Kodkod. The paper has been accepted for FM'2012.

	'''LTL'''<br>		'''LTL'''<br>
	The concept and implemenation of the visualisation is described in <ref>http://www.stups.uni-duesseldorf.de/w/Visualisierung_von_LTL-Gegenbeispielen Andriy Tolstoy: Visualisierung von LTL-Gegenbeispielen, Master thesis, University of Düsseldorf, 2012</ref>.		The concept and implemenation of the visualisation is described in the master thesis of Andriy Tolstoy.<ref>http://www.stups.uni-duesseldorf.de/w/Visualisierung_von_LTL-Gegenbeispielen Andriy Tolstoy: Visualisierung von LTL-Gegenbeispielen, Master thesis, University of Düsseldorf, 2012</ref>

	'''BMotion Studio'''<br>		'''BMotion Studio'''<br>
	A developer-, user documentation, tutorial and examples are available at <ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref>.		A developer-, user documentation, tutorial and examples are available from a dedicated webpage<ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref> hosted by the University of Duesseldorf.

	= Planning =		= Planning =

imported>Tommy: /* Planning */

2012-06-26T09:36:01Z

Planning

← Older revision		Revision as of 09:36, 26 June 2012
Line 102:		Line 102:

	'''Constraint Solving'''<br>		'''Constraint Solving'''<br>

	During the further development of ProB's constraint solving it became apparent that it would be		During the further development of ProB's constraint solving it became apparent that it would be
	helpful to represent the cardinality of a set by a CLP(FD) variable.		helpful to represent the cardinality of a set by a CLP(FD) variable.

imported>Tommy: /* Planning */

2012-06-26T09:35:38Z

Planning

← Older revision		Revision as of 09:35, 26 June 2012
Line 93:		Line 93:
	= Planning =		= Planning =

	~~===~~ Physical Units ~~===~~		'''Physical Units'''<br>
	Physical units work will be completed.		Physical units work will be completed. First experiments with industrial models from Alstom are encouraging.
	First experiments with industrial models from Alstom are encouraging.

	== Kodkod ==		'''Kodkod'''<br>
	Currently the translation to Kodkod is only applied to axioms when trying to find values for the constants and during the constraint based deadlock check.		Currently the translation to Kodkod is only applied to axioms when trying to find values for the constants and during the constraint based deadlock check.
	We plan to restructure ProB's internal programming interfaces in a way that allows to apply Kodkod more easily and make it available for other checks (e.g. constraint-based invariant check, assertion checks).		We plan to restructure ProB's internal programming interfaces in a way that allows to apply Kodkod more easily and make it available for other checks (e.g. constraint-based invariant check, assertion checks).<br>

	We will evaluate how we can employ more SMT based techniques in ProB.		We will evaluate how we can employ more SMT based techniques in ProB.

	== Constraint Solving ==		'''Constraint Solving'''<br>

	During the further development of ProB's constraint solving it became apparent that it would be		During the further development of ProB's constraint solving it became apparent that it would be
	helpful to represent the cardinality of a set by a CLP(FD) variable.		helpful to represent the cardinality of a set by a CLP(FD) variable.
	We plan to change ProB's internal representation of sets in a way that its cardinality can		We plan to change ProB's internal representation of sets in a way that its cardinality can
	be accessed in this way.		be accessed in this way.<br>

	To allow a translation from ProB to Kodkod, we implemented an integer interval analysis.		To allow a translation from ProB to Kodkod, we implemented an integer interval analysis.
	We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB		We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB
Line 115:		Line 112:
	Currently a user must supply a size manually.		Currently a user must supply a size manually.

	== LTL ==		'''LTL'''<br>
	Fairness properties are very common when specifying LTL formula. Fairness can be encoded by using standard LTL, but it makes the formula significantly larger. The complexity of the model checking algorithm grows exponentially with the number of used LTL operators in a formula. We plan to incorporate support for fairness directly into the model checker which should lead to a drastic improvement in performance when fairness is used. Additionally, the usability of the model checker is improved by having the ability to specify fairness conditions seperatly from the rest of the LTL formula.		Fairness properties are very common when specifying LTL formula. Fairness can be encoded by using standard LTL, but it makes the formula significantly larger. The complexity of the model checking algorithm grows exponentially with the number of used LTL operators in a formula. We plan to incorporate support for fairness directly into the model checker which should lead to a drastic improvement in performance when fairness is used. Additionally, the usability of the model checker is improved by having the ability to specify fairness conditions seperatly from the rest of the LTL formula.

	== BMotion Studio ==		'''BMotion Studio'''<br>

	We will provide a way to link up other Java-based simulation tools with BMotion Studio. Furthermore, beside working on identified bugs and and rectifying usability issues, we want to create more visual elements to aid humans understand large-scale simulations.		We will provide a way to link up other Java-based simulation tools with BMotion Studio. Furthermore, beside working on identified bugs and and rectifying usability issues, we want to create more visual elements to aid humans understand large-scale simulations.

imported>Tommy: /* Available Documentation */

2012-06-26T09:34:12Z

Available Documentation

← Older revision		Revision as of 09:34, 26 June 2012
Line 69:		Line 69:
	= Available Documentation =		= Available Documentation =

	== Constraint Solving ==		'''Constraint Solving'''<br>
			The improvements are available in the nightly builds of ProB.<br>
	The improvements are available in the nightly builds of ProB.

	Two specific pages have been added to the ProB user manual: <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Recursively_Defined_Functions Recursive functions entry in ProB user manual</ref>, <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/External_Functions External functions entry in ProB user manual</ref>.		Two specific pages have been added to the ProB user manual: <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Recursively_Defined_Functions Recursive functions entry in ProB user manual</ref>, <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/External_Functions External functions entry in ProB user manual</ref>.

	== TLA2B ==		'''TLA2B'''<br>
	The TLA+ to B translation has been published at the iFM'2012 conference. A technical report is available<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 Translating TLA+ to B for Validation with ProB. Technical Report, 2012.</ref>		The TLA+ to B translation has been published at the iFM'2012 conference. A technical report is available<ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschelTLA2012 Translating TLA+ to B for Validation with ProB. Technical Report, 2012.</ref>
	A presentation at the FM'2012 TLA+ workshop will also be made.		A presentation at the FM'2012 TLA+ workshop will also be made.
	A page has been added to the ProB user manual: <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA TLA2B entry in ProB user manual</ref>.		A page has been added to the ProB user manual: <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/TLA TLA2B entry in ProB user manual</ref>.

	== Physical Units ==		'''Physical Units'''<br>
	This work is still in progress. A first tutorial page is available in the ProB online documentation <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Unit_Plugin Unit Plug-in Tutorial entry in ProB user manual</ref>. Full documentation will be made available later in the project.		This work is still in progress. A first tutorial page is available in the ProB online documentation <ref>http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Unit_Plugin Unit Plug-in Tutorial entry in ProB user manual</ref>. Full documentation will be made available later in the project.
	The latest nightly build of ProB contains an experimental version of the analysis.		The latest nightly build of ProB contains an experimental version of the analysis.

	== Kodkod ==		'''Kodkod'''<br>

	A technical report has been published on the validation using ProB and Kodkod <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Validating B,Z and TLA+ using ProB and Kodkod. Technical Report, 2012.</ref>. The paper has been accepted for FM'2012.		A technical report has been published on the validation using ProB and Kodkod <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/PlaggeLeuschel_Kodkod2012 Validating B,Z and TLA+ using ProB and Kodkod. Technical Report, 2012.</ref>. The paper has been accepted for FM'2012.

	== LTL ==		'''LTL'''<br>

	The concept and implemenation of the visualisation is described in <ref>http://www.stups.uni-duesseldorf.de/w/Visualisierung_von_LTL-Gegenbeispielen Andriy Tolstoy: Visualisierung von LTL-Gegenbeispielen, Master thesis, University of Düsseldorf, 2012</ref>.		The concept and implemenation of the visualisation is described in <ref>http://www.stups.uni-duesseldorf.de/w/Visualisierung_von_LTL-Gegenbeispielen Andriy Tolstoy: Visualisierung von LTL-Gegenbeispielen, Master thesis, University of Düsseldorf, 2012</ref>.

	== BMotion Studio ==		'''BMotion Studio'''<br>

	A developer-, user documentation, tutorial and examples are available at <ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref>.		A developer-, user documentation, tutorial and examples are available at <ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref>.

imported>Tommy: /* Motivations / Decisions */

2012-06-26T09:32:41Z

Motivations / Decisions

← Older revision		Revision as of 09:32, 26 June 2012
Line 31:		Line 31:
	The latter is particularly important in light of the Theory plug-in work.		The latter is particularly important in light of the Theory plug-in work.

	[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px]]		[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px\|center]]

	'''TLA2B'''<br>		'''TLA2B'''<br>

imported>Tommy: /* Motivations / Decisions */

2012-06-26T09:31:49Z

Motivations / Decisions

← Older revision		Revision as of 09:31, 26 June 2012
Line 46:		Line 46:
	In the ProB core, we have improved ProB to better deal with infinite and recursive functions.		In the ProB core, we have improved ProB to better deal with infinite and recursive functions.
	This can be used to provide formal specifications for mathematical extensions which can be animated and model checked by ProB.		This can be used to provide formal specifications for mathematical extensions which can be animated and model checked by ProB.
	Using the newly developed external function mechanism, it should also be possible to support floats or reals, which will be important for certain cyber-physical systems.		Using the newly developed external function mechanism, it should also be possible to support floats or reals, which will be important for certain cyber-physical systems.<br>

	On the technical side, we have extended the ProB internal representation of predicates and expressions to support the Theory plug-in. The implementation will be finalize as the Theory plug-in will allow access to definitions will be granted to ProB.		On the technical side, we have extended the ProB internal representation of predicates and expressions to support the Theory plug-in. The implementation will be finalize as the Theory plug-in will allow access to definitions will be granted to ProB.

Line 55:		Line 54:
	Our experiments have shown that the translation can be highly beneficial for certain kinds of constraints, and as such opens up new ways to analyze and validate formal specifications in Event-B. However, the experiments have also shown that the constraint logic programming approach of ProB can be superior in a considerable number of scenarios; the translation to Kodkod and down to SAT is not (yet) the panacea. The same can be said of the existing translations from B to SMT.		Our experiments have shown that the translation can be highly beneficial for certain kinds of constraints, and as such opens up new ways to analyze and validate formal specifications in Event-B. However, the experiments have also shown that the constraint logic programming approach of ProB can be superior in a considerable number of scenarios; the translation to Kodkod and down to SAT is not (yet) the panacea. The same can be said of the existing translations from B to SMT.
	As such, we believe that much more research required to reap the best of both worlds (SAT/SMT and constraint programming).		As such, we believe that much more research required to reap the best of both worlds (SAT/SMT and constraint programming).
	A side-effect of the translation to Kodkod is that the ProB toolset now provides a double-chain (relying on technology developed independently and using different programming languages and paradigms) of validation for first-order predicates, which should prove relevant in high safety integrity level contexts.		A side-effect of the translation to Kodkod is that the ProB toolset now provides a double-chain (relying on technology developed independently and using different programming languages and paradigms) of validation for first-order predicates, which should prove relevant in high safety integrity level contexts.<br>

	In comparision with other formalisms Kodkod has the advantage that is provides good support for relations and sets which play an essential role in Event-B's mathematical notation.		In comparision with other formalisms Kodkod has the advantage that is provides good support for relations and sets which play an essential role in Event-B's mathematical notation.

imported>Tommy: /* Motivations / Decisions */

2012-06-26T09:31:17Z

Motivations / Decisions

imported>Tommy: /* Improvements to Constraint-Solving */

2012-06-26T09:29:34Z

Improvements to Constraint-Solving

← Older revision		Revision as of 09:29, 26 June 2012
Line 30:		Line 30:
	In particular, we have continuously improved the performance of the kernel, as can be seen in the figure below showing the performance of ProB (in seconds) on the N-Queens problem for 100 queens.		In particular, we have continuously improved the performance of the kernel, as can be seen in the figure below showing the performance of ProB (in seconds) on the N-Queens problem for 100 queens.
	Other improvements lie in better expansion of universal and existential quantifiers, reification for the the <tt>bool</tt> operator and support for infinite and recursive functions.		Other improvements lie in better expansion of universal and existential quantifiers, reification for the the <tt>bool</tt> operator and support for infinite and recursive functions.
	The latter is particularly important in light of the Theory plug-in work ~~below~~.		The latter is particularly important in light of the Theory plug-in work.

	[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px]]		[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px]]

imported>Tommy at 09:28, 26 June 2012

2012-06-26T09:28:22Z

← Older revision		Revision as of 09:28, 26 June 2012
Line 30:		Line 30:
	In particular, we have continuously improved the performance of the kernel, as can be seen in the figure below showing the performance of ProB (in seconds) on the N-Queens problem for 100 queens.		In particular, we have continuously improved the performance of the kernel, as can be seen in the figure below showing the performance of ProB (in seconds) on the N-Queens problem for 100 queens.
	Other improvements lie in better expansion of universal and existential quantifiers, reification for the the <tt>bool</tt> operator and support for infinite and recursive functions.		Other improvements lie in better expansion of universal and existential quantifiers, reification for the the <tt>bool</tt> operator and support for infinite and recursive functions.
	The latter is particularly important in light of the Theory ~~Plug~~-In work below.		The latter is particularly important in light of the Theory plug-in work below.

	[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px]]		[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px]]

← Older revision		Revision as of 09:31, 26 June 2012
Line 24:		Line 24:
	= Motivations / Decisions =		= Motivations / Decisions =

	== Improvements to Constraint-Solving ==		'''Improvements to Constraint-Solving'''<br>

	ProB's constraint solving capabilities are at the core of many of ProB's features: animation of high-level models with complicated predicates, model-based testing, constraint-based invariant and deadlock checking, etc.		ProB's constraint solving capabilities are at the core of many of ProB's features: animation of high-level models with complicated predicates, model-based testing, constraint-based invariant and deadlock checking, etc.
	It is thus important to improve this aspect of ProB.		It is thus important to improve this aspect of ProB.
Line 34:		Line 33:
	[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px]]		[[Image:performance of ProB on the N-Queens problem for 100 queens.jpg\|240px]]

	== TLA2B ==		'''TLA2B'''<br>

	TLA+ and B share the common base of predicate logic, arithmetic and set theory.		TLA+ and B share the common base of predicate logic, arithmetic and set theory.
	However, there are still considerable differences, such as very different approaches to typing and modularization. Some features of TLA+ are interesting in the context of cyber-physical systems, such as real numbers.		However, there are still considerable differences, such as very different approaches to typing and modularization. Some features of TLA+ are interesting in the context of cyber-physical systems, such as real numbers.
	There is also considerable difference in the available tool support. In particular, we wanted to compare ProB with TLC and gain insights about performance.		There is also considerable difference in the available tool support. In particular, we wanted to compare ProB with TLC and gain insights about performance.

	== Physical Units ==		'''Physical Units'''<br>
	Formal models of cyber physical systems will contain variables which represent values with physical units.		Formal models of cyber physical systems will contain variables which represent values with physical units.
	We are thus exploring to use the ProB model checker as a tool to infer and validate physical units usage in formal models.		We are thus exploring to use the ProB model checker as a tool to infer and validate physical units usage in formal models.
	In particular, we want to make sure that the physical units in a model are used in a consistent way.		In particular, we want to make sure that the physical units in a model are used in a consistent way.

	== Theory Plug-in and Mathematical Extensions ==		'''Theory Plug-in and Mathematical Extensions'''<br>


	In the ProB core, we have improved ProB to better deal with infinite and recursive functions.		In the ProB core, we have improved ProB to better deal with infinite and recursive functions.
	This can be used to provide formal specifications for mathematical extensions which can be animated and model checked by ProB.		This can be used to provide formal specifications for mathematical extensions which can be animated and model checked by ProB.
Line 54:		Line 50:
	On the technical side, we have extended the ProB internal representation of predicates and expressions to support the Theory plug-in. The implementation will be finalize as the Theory plug-in will allow access to definitions will be granted to ProB.		On the technical side, we have extended the ProB internal representation of predicates and expressions to support the Theory plug-in. The implementation will be finalize as the Theory plug-in will allow access to definitions will be granted to ProB.

	== Kodkod ==		'''Kodkod'''<br>
	We have integrated a translation of B predicates to the relational logic solver "Kodkod" and evaluated how ProB's constraint solving compares to Kodkod's SAT solving.		We have integrated a translation of B predicates to the relational logic solver "Kodkod" and evaluated how ProB's constraint solving compares to Kodkod's SAT solving.
	The integration allows to apply SAT solving to predicates where a translation is possible and a fallback to constraint solving for the remaining predicates.		The integration allows to apply SAT solving to predicates where a translation is possible and a fallback to constraint solving for the remaining predicates.
Line 63:		Line 59:
	In comparision with other formalisms Kodkod has the advantage that is provides good support for relations and sets which play an essential role in Event-B's mathematical notation.		In comparision with other formalisms Kodkod has the advantage that is provides good support for relations and sets which play an essential role in Event-B's mathematical notation.

	== LTL ==		'''LTL'''<br>
	ProB supports LTL model checking. One problem when using LTL to validate a model is that counter-examples returned by the model checker are often hard to understand.		ProB supports LTL model checking. One problem when using LTL to validate a model is that counter-examples returned by the model checker are often hard to understand.
	A counter-example typically consists of a lasso-chaped sequence of states and events. Instead of just loading the sequence into the history of the animator, we have		A counter-example typically consists of a lasso-chaped sequence of states and events. Instead of just loading the sequence into the history of the animator, we have
	implemented a dedicated visualisation for LTL counter-examples. The visualisation which is now part of ProB's Rodin plug-in shows why an LTL operator is true or false in each state of the sequence.		implemented a dedicated visualisation for LTL counter-examples. The visualisation which is now part of ProB's Rodin plug-in shows why an LTL operator is true or false in each state of the sequence.

	== CSP and B ==		'''CSP and B'''<br>

	ProB supports also other formalisms like CSP. CSP can also be used to guide B and Event-B models and can also be used for specifying scenarios or for model testing.		ProB supports also other formalisms like CSP. CSP can also be used to guide B and Event-B models and can also be used for specifying scenarios or for model testing.
	Within the project this feature of ProB was continuously maintained and improved. We have extended the implementation of the CSP interpreter and animator to be able to support more complex and larger data types (e.g. mixing of dot and non-associative tuples) as well as supporting more complicated pattern matching inside set comprehensions and function definitions. Some effort for supporting more of CSP built-in functions (like seq(-), set(-) and card(-))was made as well.		Within the project this feature of ProB was continuously maintained and improved. We have extended the implementation of the CSP interpreter and animator to be able to support more complex and larger data types (e.g. mixing of dot and non-associative tuples) as well as supporting more complicated pattern matching inside set comprehensions and function definitions. Some effort for supporting more of CSP built-in functions (like seq(-), set(-) and card(-))was made as well.