Pattern - Revision history

imported>Laurent: Fixed Category User_manual

2012-01-24T15:07:09Z

Fixed Category User_manual

← Older revision		Revision as of 15:07, 24 January 2012
Line 311:		Line 311:

	[[Category:Work in progress]]		[[Category:Work in progress]]
	[[Category:User ~~Manual~~]]		[[Category:User manual]]
	[[Category:plugin]]		[[Category:plugin]]

imported>Afuerst at 14:20, 12 November 2009

2009-11-12T14:20:18Z

← Older revision		Revision as of 14:20, 12 November 2009
Line 1:		Line 1:
	[[User:afuerst]] at '''ETH Zurich''' is in charge of the [[Pattern]] ~~plugin~~.		[[User:afuerst]] at '''ETH Zurich''' is in charge of the [[Pattern]] plug-in.


Line 140:		Line 140:

	To support developers in using patterns, there exists a plug-in for Rodin[1.1.0]. The sources are available at the location <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern'''</tt> within the svn-trunk.		To support developers in using patterns, there exists a plug-in for Rodin[1.1.0]. The sources are available at the location <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern'''</tt> within the svn-trunk.
	You can also download the ~~plugin~~ within Rodin via update manager. For this, you have to add the update-site <tt>'''http://people.inf.ethz.ch/fuersta/update-site'''</tt>.		You can also download the plug-in within Rodin via update manager. For this, you have to add the update-site <tt>'''http://people.inf.ethz.ch/fuersta/update-site'''</tt>.

	There is also an example including cheat sheet and event-b sources available. At <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt> you find the package. When starting Rodin		There is also an example including cheat sheet and event-b sources available. At <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt> you find the package. When starting Rodin
	including this package you can start the cheat sheet with ''Help'' → ''Cheat Sheets...'' and then selecting ''Other'' → ''Pattern plug-in''.		including this package you can start the cheat sheet with ''Help'' → ''Cheat Sheets...'' and then selecting ''Other'' → ''Pattern plug-in''.

	In the menu ''Pattern Example'' you can generate machines as an example with the one-click command ''Generate Machine''. The machines are created using the API of the pattern ~~plugin~~ directly without wizard support.		In the menu ''Pattern Example'' you can generate machines as an example with the one-click command ''Generate Machine''. The machines are created using the API of the pattern plug-in directly without wizard support.


	For those interested in using the pattern ~~plugin~~ API directly rather than the wizard, the corresponding code snippets are presented at each step.		For those interested in using the pattern plug-in API directly rather than the wizard, the corresponding code snippets are presented at each step.

imported>Afuerst at 13:24, 12 November 2009

2009-11-12T13:24:22Z

← Older revision		Revision as of 13:24, 12 November 2009
Line 1:		Line 1:
	[[User:afuerst]] at [[ETH Zurich]] is in charge of the [[Pattern]] plugin.		[[User:afuerst]] at '''ETH Zurich''' is in charge of the [[Pattern]] plugin.

imported>Afuerst at 13:17, 12 November 2009

2009-11-12T13:17:12Z

← Older revision		Revision as of 13:17, 12 November 2009
Line 6:		Line 6:

	An example including cheat sheet and event-b sources is available at <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt>.		An example including cheat sheet and event-b sources is available at <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt>.

			Both packages are also available via update manager. For this, open ''Help'' → ''Software Updates'' in Rodin and add the update-site <tt>'''http://people.inf.ethz.ch/fuersta/update-site'''</tt>.

imported>Afuerst: /* Tool support */

2009-11-12T13:12:12Z

Tool support

← Older revision		Revision as of 13:12, 12 November 2009
Line 137:		Line 137:
	== Tool support ==		== Tool support ==

	To support developers in using patterns, there exists a plug-in for Rodin. ~~A first try-out version of the tool is~~ available at the location <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern'''</tt> within the svn-trunk.		To support developers in using patterns, there exists a plug-in for Rodin[1.1.0]. The sources are available at the location <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern'''</tt> within the svn-trunk.
			You can also download the plugin within Rodin via update manager. For this, you have to add the update-site <tt>'''http://people.inf.ethz.ch/fuersta/update-site'''</tt>.

	There is also an example including cheat sheet and event-b sources available. At <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt> you find the package. When starting Rodin		There is also an example including cheat sheet and event-b sources available. At <tt>'''_exploratory/fuersta/ch.ethz.eventb.pattern.example'''</tt> you find the package. When starting Rodin

imported>Afuerst: /* Tool support */

2009-11-09T16:22:07Z

Tool support

← Older revision		Revision as of 16:22, 9 November 2009
Line 279:		Line 279:
	*Enter the name for the new problem refinement machine.		*Enter the name for the new problem refinement machine.

	*The replacement for disappearing variables ~~have~~ to be set. To extract this information from the gluing invariant all the invariants are listed at the top of the wizard page.		*The replacement for disappearing variables has to be set. To extract this information from the gluing invariant all the invariants are listed at the top of the wizard page.

			<span style="color:darkgreen;">// SET REPLACEMENT FOR VARIABLES</span>
			data.updateForwardReplacementOf(patternVariable, replacement); <span style="color:darkgreen;">// patternVariable is of type IVariable, renaming is a String</span>


	*If there is a witness in an event of the pattern refinement, this witness is used to determine the replacement of the former parameters in the extra guards and extra actions.		*If there is a witness in an event of the pattern refinement, this witness is used to determine the replacement of the former parameters in the extra guards and extra actions.

			<span style="color:darkgreen;">// SET REPLACEMENT FOR PARAMETERS</span>
			data.updateReplacementOf(patternWitness, replacement); <span style="color:darkgreen;">// patternWitness is of type IWitness, renaming is a String</span>


	*It can be chosen whether the proof obligation should be generated or not.		*It can be chosen whether the proof obligation should be generated or not.

	*If all replacements are set, the ''Finish'' button is enables to start the generation of the problem refinement.		*If all replacements are set, the ''Finish'' button is enables to start the generation of the problem refinement.

			<span style="color:darkgreen;">// GENERATE MACHINE</span>
			IMachineGenerator generator = data.createNewMachineGenerator();
			problemMachine = generator.generateMachine(name, generatePO, monitor); <span style="color:darkgreen;">// name is is a String, generatePO is a boolean and monitor is of type IProgressMonitor</span>


	:[[Image:~~Pattern_incorporation~~.~~jpg~~]]		:[[Image:Pattern_incorporating.png]]

imported>Afuerst: /* Tool support */

2009-11-09T16:11:38Z

Tool support

← Older revision		Revision as of 16:11, 9 November 2009
Line 179:		Line 179:

	<span style="color:darkgreen;">// SET VARIABLE MATCHINGS</span>		<span style="color:darkgreen;">// SET VARIABLE MATCHINGS</span>
	data.addMatching(patternVariable, problemVariable); <span style="color:darkgreen;">// both ~~inputs~~ are of type IVariable</span>		data.addMatching(patternVariable, problemVariable); <span style="color:darkgreen;">// both parameters are of type IVariable</span>


Line 185:		Line 185:

	<span style="color:darkgreen;">// SET EVENT MATCHINGS</span>		<span style="color:darkgreen;">// SET EVENT MATCHINGS</span>
	data.addMatching(patternEvent, problemEvent); <span style="color:darkgreen;">// both ~~inputs~~ are of type IEvent</span>		data.addMatching(patternEvent, problemEvent); <span style="color:darkgreen;">// both parameters are of type IEvent</span>


Line 191:		Line 191:

	<span style="color:darkgreen;">// SET CONTEXT MATCHINGS</span>		<span style="color:darkgreen;">// SET CONTEXT MATCHINGS</span>
	data.updateMatching(carrierSetOrConstant, "PROPOSAL"); <span style="color:darkgreen;">// the first ~~input~~ is of type ICarrierSet or IConstant, the second ~~input~~ is a String</span>		data.updateMatching(carrierSetOrConstant, "PROPOSAL"); <span style="color:darkgreen;">// the first parameter is of type ICarrierSet or IConstant, the second parameter is a String</span>


Line 202:		Line 202:

	<span style="color:darkgreen;">// SET PARAMETERS</span>		<span style="color:darkgreen;">// SET PARAMETERS</span>
	data.addMatching(patternParameter, problemParameter); <span style="color:darkgreen;">// both ~~inputs~~ are of type IParameter</span>		data.addMatching(patternParameter, problemParameter); <span style="color:darkgreen;">// both parameters are of type IParameter</span>

	<span style="color:darkgreen;">// SET GUARDS</span>		<span style="color:darkgreen;">// SET GUARDS</span>
	data.addMatching(patternGuard, problemGuard); <span style="color:darkgreen;">// both ~~inputs~~ are of type IGuard</span>		data.addMatching(patternGuard, problemGuard); <span style="color:darkgreen;">// both parameters are of type IGuard</span>

	<span style="color:darkgreen;">// SET ACTIONS</span>		<span style="color:darkgreen;">// SET ACTIONS</span>
	data.addMatching(patternAction, problemAction); <span style="color:darkgreen;">// both ~~inputs~~ are of type IAction</span>		data.addMatching(patternAction, problemAction); <span style="color:darkgreen;">// both parameters are of type IAction</span>


Line 246:		Line 246:

	<span style="color:darkgreen;">// SET EVENT MERGINGS</span>		<span style="color:darkgreen;">// SET EVENT MERGINGS</span>
	data.addMerging(patternRefinementEvent, problemEvent) <span style="color:darkgreen;">// both ~~inputs~~ are of type IEvent</span>		data.addMerging(patternRefinementEvent, problemEvent); <span style="color:darkgreen;">// both parameters are of type IEvent</span>


Line 257:		Line 257:

	*In the case of more than one problem event being matched with the same pattern event, the pattern events can be distinguished by the name of the matched problem event in the parentheses.		*In the case of more than one problem event being matched with the same pattern event, the pattern events can be distinguished by the name of the matched problem event in the parentheses.

			<span style="color:darkgreen;">// RENAME THE VARIABLES</span>
			data.updateRenaming(patternRefinementVariable, renaming); <span style="color:darkgreen;">// patternRefinementVariable is of type IVariable, renaming is a String</span>

			<span style="color:darkgreen;">// RENAME THE MATCHED EVENTS</span>
			data.updateRenamingOfMatchedEvent(patternRefinementEvent, problemEvent, renaming); <span style="color:darkgreen;">// patternRefinementEvent and problemEvent are of type IEvent, renaming is a String</span>

			<span style="color:darkgreen;">// RENAME THE MERGED EVENTS</span>
			data.updateRenamingOfMergedEvent(problemEvent, renaming); <span style="color:darkgreen;">// problemEvent is of type IEvent, renaming is a String</span>

			<span style="color:darkgreen;">// RENAME THE NEW EVENTS</span>
			data.updateRenamingOfNewEvent(patternRefinementEvent, renaming); <span style="color:darkgreen;">// patternRefinementEvent is of type IEvent, renaming is a String</span>


	*If there are no duplicate names or names that already exist in the not-matched part of the problem, the ''Next'' button is enabled to proceed to the next step.		*If there are no duplicate names or names that already exist in the not-matched part of the problem, the ''Next'' button is enabled to proceed to the next step.

imported>Afuerst: /* Renaming page */

2009-11-09T15:57:37Z

Renaming page

← Older revision		Revision as of 15:57, 9 November 2009
Line 252:		Line 252:

	==== Renaming page ====		==== Renaming page ====
	*For every variable and every event of the pattern refinement that is copied to the generated problem refinement, a name can be chosen. For every item a name is proposed. If the pattern variable was matched with the problem, the original name within the problem machine is proposed. If the pattern event refines a matched event, the original name within the problem machine is proposed.		*For every variable and every event of the pattern refinement that is copied to the generated problem refinement, a name can be chosen. For every item a name is proposed. If the pattern variable was matched with the problem, the original name within the problem machine is proposed. If the pattern event refines a matched event or is merged with a problem event, the original name within the problem machine is proposed.

	*Otherwise the name within the pattern refinement is proposed.		*Otherwise the name within the pattern refinement is proposed.
Line 261:		Line 261:


	:[[Image:Pattern_renaming.~~jpg~~]]		:[[Image:Pattern_renaming.png]]

	==== Incorporating page ====		==== Incorporating page ====

imported>Afuerst: /* Tool support */

2009-11-09T15:53:00Z

Tool support

← Older revision		Revision as of 15:53, 9 November 2009
Line 237:		Line 237:

	==== Merging page ====		==== Merging page ====
			*Choose the refinement machine of the pattern that should be incorporated into the problem.

			<span style="color:darkgreen;">// SET PATTERN REFINEMENT MACHINE</span>
			data.changePatternRefinementMachine(patternRefinementMachine); <span style="color:darkgreen;">// patternRefinementMachine is of type IMachineRoot</span>


			*If there are new events in the pattern refinement they can be merged with not-matched events of the problem machine. A pattern event can be merged with only one problem event. But several pattern events can be merged with one and the same problem event.

			<span style="color:darkgreen;">// SET EVENT MERGINGS</span>
			data.addMerging(patternRefinementEvent, problemEvent) <span style="color:darkgreen;">// both inputs are of type IEvent</span>


			:[[Image:Pattern_merging.png]]

	==== Renaming page ====		==== Renaming page ====

imported>Afuerst: /* Renaming page */

2009-11-09T15:36:19Z

Renaming page

← Older revision		Revision as of 15:36, 9 November 2009
Line 235:		Line 235:
	:[[Image:Pattern_checking.jpg]]		:[[Image:Pattern_checking.jpg]]


			==== Merging page ====

	==== Renaming page ====		==== Renaming page ====
Line 247:		Line 249:

	:[[Image:Pattern_renaming.jpg]]		:[[Image:Pattern_renaming.jpg]]


	==== Incorporating page ====		==== Incorporating page ====