Mode/FT Views - Revision history

imported>Hobbs: /* Run a static check / build POs */

2015-06-26T20:32:26Z

Run a static check / build POs

← Older revision		Revision as of 20:32, 26 June 2015
Line 167:		Line 167:

	If the static check is successful, a number of POs will be generated for the referenced machine. Even if there are SC errors, the POs which are related to the statically correct elements will still be generated.		If the static check is successful, a number of POs will be generated for the referenced machine. Even if there are SC errors, the POs which are related to the statically correct elements will still be generated.

			==== FAQs ====

			# How do I get my <tt>.mode</tt> file into a particular machine? When a mode diagram is created, it appears in the project explorer at the project level, rather than within a particular machine. No amount of dragging and dropping in the project explorer will move it, but the move is very simple. Simply select the mode diagram and edit the "Machine" valid in its "Core" properties. This is a pull-down list containing all the possible machines.

	== Version changes ==		== Version changes ==

imported>Ilya.lopatkin: /* Version changes */

2013-07-01T13:02:30Z

Version changes

← Older revision		Revision as of 13:02, 1 July 2013
Line 170:		Line 170:
	== Version changes ==		== Version changes ==

	~~''' Current issues '''~~		'''Version 1.0.1''' is compatible with Rodin 2.1 and later versions
	~~----~~
	<span style="text-decoration: line-through;">* No modal SC or POs are performed when one changes the Event-B model retaining the mode view. This is because of SC not being integrated into the Rodin builder. The initial idea is to keep modes outside of the Rodin database, but then we cannot properly hook the Rodin SC tool.</span>
	* Copy/paste is not working as one would expect. Pasting adds references to the GMF elements from the source document rather than creating new elements and copying data. This is a default GMF behaviour.
	<span style="text-decoration: line-through;">* Mode views might not be seen from the Event-B explorer if a project has been just opened, or a view just created. Please, use the usual eclipse file explorer to open diagrams.</span>

	'''Version 1.0.1''' is compatible with Rodin 2.1
	----		----

imported>Ilya.lopatkin: /* References */

2012-09-27T13:15:27Z

References

← Older revision		Revision as of 13:15, 27 September 2012
Line 207:		Line 207:
	* [http://rodinmodeftview.sourceforge.net/examples/train.zip Toy train example]		* [http://rodinmodeftview.sourceforge.net/examples/train.zip Toy train example]
	* [http://rodinmodeftview.sourceforge.net/examples/aocs.zip AOCS case study]		* [http://rodinmodeftview.sourceforge.net/examples/aocs.zip AOCS case study]
			Complete developments:
			* [http://rodinmodeftview.sourceforge.net/examples/sluice_20120927.zip Sluice gate case study]. Thesis version
			* [http://rodinmodeftview.sourceforge.net/examples/aocs_20120927.zip AOCS case study]. Thesis version


	[[Category:Plugin]]		[[Category:Plugin]]
	[[Category:User documentation]]		[[Category:User documentation]]

imported>Ilya.lopatkin: /* Proof obligations */ EVT_G and EVT_A changes, PRESERVE removed

2011-10-31T10:44:09Z

Proof obligations: EVT_G and EVT_A changes, PRESERVE removed

← Older revision		Revision as of 10:44, 31 October 2011
Line 89:		Line 89:
	\| <math>I(v) \land A(v) \land G(v,v') \implies I(v')</math>		\| <math>I(v) \land A(v) \land G(v,v') \implies I(v')</math>
	\| Mode guarantee preserves the invariant		\| Mode guarantee preserves the invariant
	\|-
	~~\| view_name/mode_name/PRESERVE~~
	~~\| <math>I(v) \land G(v,v') \implies A(v')</math>~~
	~~\| Internal transition condition. Mode guarantee preserves the mode assumption~~
	\|-		\|-
	\| event_name/view_name/transition_name/INITIALISATION		\| event_name/view_name/transition_name/INITIALISATION
Line 99:		Line 95:
	\|-		\|-
	\| event_name/view_name/mode_name/EVT_G		\| event_name/view_name/mode_name/EVT_G
	\| <math>I(v) \land A(v) \land H(v) \land S(v,v') \implies G(v,v') \lor A_1(v') \lor ... A_n(v') </math>		\| <math>I(v) \land A(v) \land H(v) \land S(v,v') \implies [G(v,v') \land A(v')] \lor [\lnot A(v') \land (A_1(v') \lor ... A_n(v'))] </math>
	\| All the events of a mode must satisfy the mode guarantee. If the same event is used for outgoing transitions - the assumptions of ~~new~~ modes ~~must also be satisfied~~		\| All the events of a mode must satisfy the mode guarantee and reestablish the assmumption. If the same event is used for outgoing transitions - it must satisfy the assumptions of one of the target modes and invalidate the source assumption
	\|-		\|-
	\| event_name/view_name/EVT_A		\| event_name/view_name/EVT_A
	\| <math>I(v) \land H(v) \implies A_1(v) \lor \dots \lor A_k(v)</math>		\| <math>I(v) \land H(v) \implies A_1(v) \lor \dots \lor A_k(v) \lor A_{tr1} \lor \dots \lor A_{trn}</math>
	\| The partitioning of the events into modes must be in agreement with the event guards. <math>A_1 - A_k</math> are assumptions of the modes associated with the event		\| The partitioning of the events into modes must be in agreement with the event guards. <math>A_1 - A_k</math> are assumptions of the modes associated with the event, <math>A_{tr1} - A_{trn}</math> are assumptions of the modes of which outgoing transitions are associated with the event
	\|-		\|-
	\| view_name/mode_name/ENBL		\| view_name/mode_name/ENBL

imported>Mathieu: /* References */ Category:Plugin Category:User documentation

2011-08-01T07:03:18Z

References: Category:Plugin Category:User documentation

← Older revision		Revision as of 07:03, 1 August 2011
Line 211:		Line 211:
	* [http://rodinmodeftview.sourceforge.net/examples/train.zip Toy train example]		* [http://rodinmodeftview.sourceforge.net/examples/train.zip Toy train example]
	* [http://rodinmodeftview.sourceforge.net/examples/aocs.zip AOCS case study]		* [http://rodinmodeftview.sourceforge.net/examples/aocs.zip AOCS case study]


			[[Category:Plugin]]
			[[Category:User documentation]]

imported>Ilya.lopatkin: /* References */

2011-06-03T19:44:23Z

References

← Older revision		Revision as of 19:44, 3 June 2011
Line 210:		Line 210:
	Examples:		Examples:
	* [http://rodinmodeftview.sourceforge.net/examples/train.zip Toy train example]		* [http://rodinmodeftview.sourceforge.net/examples/train.zip Toy train example]
			* [http://rodinmodeftview.sourceforge.net/examples/aocs.zip AOCS case study]

imported>Ilya.lopatkin: /* Proof obligations */

2011-05-30T16:44:44Z

Proof obligations

← Older revision		Revision as of 16:44, 30 May 2011
Line 99:		Line 99:
	\|-		\|-
	\| event_name/view_name/mode_name/EVT_G		\| event_name/view_name/mode_name/EVT_G
	\| <math>I(v) \land A(v) \land H(v) \land S(v,v') \implies ~~G_1~~(v,~~v') \lor ... \lor G_k(~~v') \lor A_1(v') \lor ... A_n(v') </math>		\| <math>I(v) \land A(v) \land H(v) \land S(v,v') \implies G(v,v') \lor A_1(v') \lor ... A_n(v') </math>
	\| All the events of a mode must satisfy the mode guarantee. If the same event is used for outgoing transitions - the assumptions of new modes must also be satisfied		\| All the events of a mode must satisfy the mode guarantee. If the same event is used for outgoing transitions - the assumptions of new modes must also be satisfied
	\|-		\|-

imported>Ilya.lopatkin: /* Current issues */

2011-02-08T19:33:19Z

Current issues

← Older revision		Revision as of 19:33, 8 February 2011
Line 172:		Line 172:
	If the static check is successful, a number of POs will be generated for the referenced machine. Even if there are SC errors, the POs which are related to the statically correct elements will still be generated.		If the static check is successful, a number of POs will be generated for the referenced machine. Even if there are SC errors, the POs which are related to the statically correct elements will still be generated.

	== Current issues ==		== Version changes ==

			''' Current issues '''
			----
	<span style="text-decoration: line-through;">* No modal SC or POs are performed when one changes the Event-B model retaining the mode view. This is because of SC not being integrated into the Rodin builder. The initial idea is to keep modes outside of the Rodin database, but then we cannot properly hook the Rodin SC tool.</span>		<span style="text-decoration: line-through;">* No modal SC or POs are performed when one changes the Event-B model retaining the mode view. This is because of SC not being integrated into the Rodin builder. The initial idea is to keep modes outside of the Rodin database, but then we cannot properly hook the Rodin SC tool.</span>
	* Copy/paste is not working as one would expect. Pasting adds references to the GMF elements from the source document rather than creating new elements and copying data. This is a default GMF behaviour.		* Copy/paste is not working as one would expect. Pasting adds references to the GMF elements from the source document rather than creating new elements and copying data. This is a default GMF behaviour.
	<span style="text-decoration: line-through;">* Mode views might not be seen from the Event-B explorer if a project has been just opened, or a view just created. Please, use the usual eclipse file explorer to open diagrams.</span>		<span style="text-decoration: line-through;">* Mode views might not be seen from the Event-B explorer if a project has been just opened, or a view just created. Please, use the usual eclipse file explorer to open diagrams.</span>

			'''Version 1.0.1''' is compatible with Rodin 2.1
			----

	'''Version 1.0.1''' for Rodin 2.0.1		'''Version 1.0.1''' for Rodin 2.0.1

imported>Ilya.lopatkin: /* Current issues */

2011-01-03T16:21:42Z

Current issues

← Older revision		Revision as of 16:21, 3 January 2011
Line 176:		Line 176:
	* Copy/paste is not working as one would expect. Pasting adds references to the GMF elements from the source document rather than creating new elements and copying data. This is a default GMF behaviour.		* Copy/paste is not working as one would expect. Pasting adds references to the GMF elements from the source document rather than creating new elements and copying data. This is a default GMF behaviour.
	<span style="text-decoration: line-through;">* Mode views might not be seen from the Event-B explorer if a project has been just opened, or a view just created. Please, use the usual eclipse file explorer to open diagrams.</span>		<span style="text-decoration: line-through;">* Mode views might not be seen from the Event-B explorer if a project has been just opened, or a view just created. Please, use the usual eclipse file explorer to open diagrams.</span>

			'''Version 1.0.1''' for Rodin 2.0.1
			----

	'''Version 1.0.0''' for Rodin 2.0		'''Version 1.0.0''' for Rodin 2.0
	----		----
	Dependencies between views and models ~~are~~ resolved ~~ok now~~. Changing the model leads to SC of views.		Dependencies between views and models resolved. Changing the model leads to SC of views.

	~~Models are not "poluted" with many mode stubs, but with a single one~~.

	~~The tool adds and removes builder configurations properly. Now also cleans the configurations of models when views are deleted~~.		Model keeps a single stub telling that it has at least one view.

	~~Generally usable now~~.		The tool adds and removes builder configurations properly. Cleans the configurations of models when views are deleted.

	'''Version 0.2.1'''		'''Version 0.2.1'''

imported>Ilya.lopatkin: /* Run a static check / build POs */

2010-11-08T19:28:43Z

Run a static check / build POs

← Older revision		Revision as of 19:28, 8 November 2010
Line 168:		Line 168:

	==== Run a static check / build POs ====		==== Run a static check / build POs ====
	~~Currently, a~~ static check ~~is performed during a file save operation. This is ok while editing modes, however it~~ will ~~have to~~ be ~~changed: the checks~~ run ~~against a statically checked Event-B models, and changes to the models currently do not trigger~~ the ~~mode views check. If you already have a mode~~ view~~, and you make changes to the model and want to static-check the view again - please make a slight change to the view (move a mode) and save it. This~~ is ~~a simple solution sufficient at~~ the ~~current stage.~~		A static check of the view will be run each time the view is saved or the abstract view is saved. Errors if any will appear under the usual Eclipse "Problems" view. Additionally, any error concerned with specific diagram element will be shown on the element as a red cross at the corner. If you point the mouse to that cross and hold a second, you will see the same error message as in the "Problems" log. The errors messages are generally comprehensible and reflect the rules for building modal views. However, currently they do not show the unproved POs.
	~~Saving a mode~~ view ~~also makes a change to the model which triggers the model static check and (if automatic build~~ is ~~enabled) Event-B PO generation~~. ~~Mode view PO modules are properly integrated into the Rodin builder.~~
	~~POs are generated only~~ if ~~the static check has succeeded. If not - there~~ will ~~be a number of errors in~~ the usual Eclipse "Problems" view. Additionally, any error concerned with specific diagram element will be shown on the element as a red cross in the corner. If you point the mouse to that cross and hold a ~~moment~~, you will see the same error message as in the "Problems" log. The errors messages are generally comprehensible and reflect the rules for building modal views. However, currently they do not show the unproved POs.		If the static check is successful, a number of POs will be generated for the referenced machine. Even if there are SC errors, the POs which are related to the statically correct elements will still be generated.

	== Current issues ==		== Current issues ==