Event-B Qualitative Probability User Guide - Revision history

imported>Son: /* Introduction */

2018-03-21T17:54:01Z

Introduction

← Older revision		Revision as of 17:54, 21 March 2018
Line 4:		Line 4:
	== Introduction ==		== Introduction ==
	Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).		Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).
	For more details about the principles on ~~XEvent~~-B, see the [[Qualitative Probability \| Qualitative Probability page]].		For more details about the principles on Event-B Qualitative Probability, see the [[Qualitative Probability \| Qualitative Probability page]].

	== Installing and Updating ==		== Installing and Updating ==

2017-07-25T20:51:03Z

Technical References

@@ Line 18: / Line 18: @@
 == Technical References ==
 * S. Hallerstede, T.S. Hoang. '''Qualitative Probabilistic Modelling in Event-B'''. In ''IFM 2007: Integrated Formal Methods, 6th International Conference Proceedings'', Oxford, UK, July 2-5, 2007, volume 4591 of LNCS © Springer-Verlag. [http://dx.doi.org/10.1007/978-3-540-73210-5_16 Springer website]
 ** Initial idea about probabilistic convergence event.
@@ Line 23: / Line 34: @@
 ** New proof obligations: '''PRV''', '''BND''', '''FINACT'''.
 ** Example: Resolve contention in IEEE 1395 (Firewire protocol).
 == Usage ==

2017-07-25T20:14:45Z

News

← Older revision		Revision as of 20:14, 25 July 2017
Line 13:		Line 13:
	* 10.04.2012: Version 0.2.1 is compatible with Rodin 2.4.*		* 10.04.2012: Version 0.2.1 is compatible with Rodin 2.4.*
	* 14.05.2012: Version 0.2.1 is compatible with Rodin 2.5.*		* 14.05.2012: Version 0.2.1 is compatible with Rodin 2.5.*
	* 09.03.2015: Version 0.2.2 is ~~compatible~~ with Rodin 3.x.x		* 09.03.2015: Version 0.2.2 is released with Rodin 3.x.x
			* 09.10.2015: Version 0.2.3 is released
			* 23.07.2017: Version 0.2.4 is released

	== Technical References ==		== Technical References ==

2017-07-25T20:13:26Z

Introduction

← Older revision		Revision as of 20:13, 25 July 2017
Line 4:		Line 4:
	== Introduction ==		== Introduction ==
	Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).		Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).
			For more details about the principles on XEvent-B, see the [[Qualitative Probability \| Qualitative Probability page]].

	== Installing and Updating ==		== Installing and Updating ==

2015-03-09T00:57:28Z

← Older revision		Revision as of 00:57, 9 March 2015
Line 1:		Line 1:
	[[User:Son]] ~~at '''ETH Zurich'''~~ is in charge of the plug-in.		[[User:Son]] is in charge of the plug-in.
	{{TOCright}}		{{TOCright}}

2015-03-09T00:56:27Z

News

← Older revision		Revision as of 00:56, 9 March 2015
Line 13:		Line 13:
	* 10.04.2012: Version 0.2.1 is compatible with Rodin 2.4.*		* 10.04.2012: Version 0.2.1 is compatible with Rodin 2.4.*
	* 14.05.2012: Version 0.2.1 is compatible with Rodin 2.5.*		* 14.05.2012: Version 0.2.1 is compatible with Rodin 2.5.*
			* 09.03.2015: Version 0.2.2 is compatible with Rodin 3.x.x

	== Technical References ==		== Technical References ==

2012-05-14T13:13:41Z

Explanations for some warning and error messages

← Older revision		Revision as of 13:13, 14 May 2012
Line 63:		Line 63:

	* '''Missing variant''' warning		* '''Missing variant''' warning
	** Problem: [[Image:contention-novariant.jpg]]		** Problem: [[Image:contention-novariant.jpg\|500px\|alt=Alt\|Missing variant]]
	** Explanation: User needs to provide a variant for probabilistic convergence events.		** Explanation: User needs to provide a variant for probabilistic convergence events.
	** Solution: Add a variant to the model		** Solution: Add a variant to the model

2012-05-14T13:11:08Z

Explanations for some warning and error messages

← Older revision		Revision as of 13:11, 14 May 2012
Line 69:		Line 69:

	* '''Missing bound''' error		* '''Missing bound''' error
	** Problem: [[Image:contention-nobound.jpg\|~~100px~~\|alt=Alt\|Missing bound]]		** Problem: [[Image:contention-nobound.jpg\|400px\|alt=Alt\|Missing bound]]
	** Explanation: The variant for probabilistic events need to be bounded above.		** Explanation: The variant for probabilistic events need to be bounded above.
	** Solution: Add a bound to the model (using Edit page of the standard Rodin editor).		** Solution: Add a bound to the model (using Edit page of the standard Rodin editor).

2012-05-14T13:10:28Z

Explanations for some warning and error messages

← Older revision		Revision as of 13:10, 14 May 2012
Line 69:		Line 69:

	* '''Missing bound''' error		* '''Missing bound''' error
	** Problem: [[Image:contention-nobound.jpg]]		** Problem: [[Image:contention-nobound.jpg\|100px\|alt=Alt\|Missing bound]]
	** Explanation: The variant for probabilistic events need to be bounded above.		** Explanation: The variant for probabilistic events need to be bounded above.
	** Solution: Add a bound to the model (using Edit page of the standard Rodin editor).		** Solution: Add a bound to the model (using Edit page of the standard Rodin editor).

2012-05-14T13:06:16Z

Probabilistic Modelling

← Older revision		Revision as of 13:06, 14 May 2012
Line 46:		Line 46:

	* Create a new bound element (right-click on the machine name and choose ''Add Child''/Event-B Bound Element).		* Create a new bound element (right-click on the machine name and choose ''Add Child''/Event-B Bound Element).
	[[Image:contention-bound-create.jpg\|~~100px~~\|alt=Alt\|Create the bound element]]		[[Image:contention-bound-create.jpg\|500px\|alt=Alt\|Create the bound element]]


	* Set <math>\Bool</math> as the bound of the model		* Set <math>\Bool</math> as the bound of the model