Extending the Static Checker - Revision history

imported>Renato: /* Before Starting */

2011-07-05T16:24:01Z

Before Starting

← Older revision		Revision as of 16:24, 5 July 2011
Line 21:		Line 21:
	****SubComponentElement (elements used to decompose: variables for shared event decomposition and events for shared variable decomposition)		****SubComponentElement (elements used to decompose: variables for shared event decomposition and events for shared variable decomposition)

	[[Image:Decomp file pretty print.png\|500x500px~~\|center~~]]		[[Image:Decomp file pretty print.png\|500x500px]]

	To extend the static checker, it is necessary to add a new content type (<tt>org.eclipse.core.contenttype.contentTypes</tt>) containing the checked version of the decompositionFile:		To extend the static checker, it is necessary to add a new content type (<tt>org.eclipse.core.contenttype.contentTypes</tt>) containing the checked version of the decompositionFile:

imported>Renato: /* Before Starting */

2011-07-05T16:23:38Z

Before Starting

← Older revision		Revision as of 16:23, 5 July 2011
Line 21:		Line 21:
	****SubComponentElement (elements used to decompose: variables for shared event decomposition and events for shared variable decomposition)		****SubComponentElement (elements used to decompose: variables for shared event decomposition and events for shared variable decomposition)

	[[Image:Decomp file pretty print.png]]		[[Image:Decomp file pretty print.png\|500x500px\|center]]

	To extend the static checker, it is necessary to add a new content type (<tt>org.eclipse.core.contenttype.contentTypes</tt>) containing the checked version of the decompositionFile:		To extend the static checker, it is necessary to add a new content type (<tt>org.eclipse.core.contenttype.contentTypes</tt>) containing the checked version of the decompositionFile:

imported>Pascal: /* Sequencing */

2010-08-25T15:28:13Z

Sequencing

← Older revision		Revision as of 15:28, 25 August 2010
Line 269:		Line 269:
	== Sequencing ==		== Sequencing ==

			=== Parent ===
			A module may be linked to a parent module. The parent module will be run before its children.
			It is for example useful if the purpose of this module is to add some post-processing operations to those performed by the parent module.

	~~=== Parent ===~~
	~~A module may be linked to a parent module.~~
	The parent module shall be a processor module.		The parent module shall be a processor module.

	=== Prerequisite ===		=== Prerequisite ===
			A module may rely on another module, which is not necessarily on the parent hierarchy, and the execution of the latter is a pre-requirement for the execution of the former. For instance, if a concrete event is refined, it is necessary to know the abstract machine defined in the refine machine section. Thus, the refine machine is a static check pre-requirement for the refinement of an event. To implement a pre-requirement, it is necessary to use the following extension point:
	~~Some static checks~~ rely on ~~already done static checks so they work as~~ pre-~~requirements~~. For instance, if a concrete event is refined, it is necessary to know the abstract machine defined in the refine machine section. So the refine machine is a static check pre-requirement for the refinement an event. To implement a pre-requirement, it is necessary to use the following extension point:

	<!ELEMENT prereq EMPTY>		<!ELEMENT prereq EMPTY>

imported>Pascal: /* Parent */

2010-08-25T15:08:12Z

Parent

← Older revision		Revision as of 15:08, 25 August 2010
Line 271:		Line 271:

	=== Parent ===		=== Parent ===
	~~{{TODO}}~~		A module may be linked to a parent module.
			The parent module shall be a processor module.

	=== Prerequisite ===		=== Prerequisite ===

imported>Pascal: /* Prerequisite */

2010-08-25T15:03:39Z

Prerequisite

← Older revision		Revision as of 15:03, 25 August 2010
Line 282:		Line 282:
	>		>
	id - the full ids of all (filter and processor) modules that must be run before this module		id - the full ids of all (filter and processor) modules that must be run before this module

			A pre-required module may be a filter module or a processor module.

	== Example ==		== Example ==

imported>Pascal: /* Programmatic usage */

2010-08-25T14:45:09Z

Programmatic usage

← Older revision		Revision as of 14:45, 25 August 2010
Line 186:		Line 186:

	== Programmatic usage ==		== Programmatic usage ==
	~~The~~ configuration ~~is programmatically set with~~ the <tt>org.eventb.core.IConfigurationElement.setConfiguration</tt> ~~dedicated~~ method.		It is possible to get the current configuration by invoking the <tt>org.eventb.core.IConfigurationElement.getConfiguration</tt> dedicated method.

			In the same manner, the configuration is programmatically set with the <tt>setConfiguration</tt> method. It is possible to set multiple configurations with the ";" separator. Note that it is generally preferable to add a new configuration to the existing ones (see example 1), instead of replacing the existing ones with a new one (see example 2). Only the first evolution is indeed backward compatible. The second case requires to have installed the plug-in defining the new configuration in order to be able to manage the elements associated with this configuration; these elements cannot be (partially) handled by the old configuration.

			* Example 1 (better)
			String conf = root.getConfiguration();
			root.setConfiguration(conf + ";" + NEW_CONF);
			: where <tt>root</tt> is a <tt>IConfigurationElement</tt> object.
			: and <tt>NEW_CONF</tt> is the name of the new configuration.

			* Example 2
			root.setConfiguration(NEW_CONF);

	= Modules =		= Modules =

imported>Pascal: /* Programmatic usage */

2010-08-25T14:10:27Z

Programmatic usage

← Older revision		Revision as of 14:10, 25 August 2010
Line 186:		Line 186:

	== Programmatic usage ==		== Programmatic usage ==
	~~{{TODO}}~~		The configuration is programmatically set with the <tt>org.eventb.core.IConfigurationElement.setConfiguration</tt> dedicated method.

	= Modules =		= Modules =

imported>Tommy: /* Processor */

2010-08-25T13:30:00Z

Processor

← Older revision		Revision as of 13:30, 25 August 2010
Line 216:		Line 216:
	== Processor ==		== Processor ==

	Processors literally process the elements, storing them in the static checked file, running sub-processors and adding states to the repository if required. To implement a processor, it is required to use the following extension :		Processors literally process the elements, storing them in the static checked file, running sub-processors and adding states to the repository if required. To implement a processor, it is required to use the following extension from the extension point <tt>org.eventb.core.scModuleTypes</tt>:

	<!ELEMENT processorType (prereq)*>		<!ELEMENT processorType (prereq)*>

imported>Tommy: /* Filter */

2010-08-25T13:29:47Z

Filter

← Older revision		Revision as of 13:29, 25 August 2010
Line 191:		Line 191:
	== Filter ==		== Filter ==

	Filters are used to validate inserted elements. After the successful validation of all elements, they can be processed and stored in the statically-checked file. In order to implement a filter, we use the following extension :		Filters are used to validate inserted elements. After the successful validation of all elements, they can be processed and stored in the statically-checked file. In order to implement a filter, we use the following extension from the extension point <tt>org.eventb.core.scModuleTypes</tt>:

	<!ELEMENT filterType (prereq)*>		<!ELEMENT filterType (prereq)*>

imported>Tommy: /* Processor */

2010-08-25T13:27:58Z

Processor

← Older revision		Revision as of 13:27, 25 August 2010
Line 216:		Line 216:
	== Processor ==		== Processor ==

	Processors literally process the elements, storing them in the static checked file, running sub-processors and adding states to the repository if required. To implement a processor, it is required to use the following extension ~~point~~:		Processors literally process the elements, storing them in the static checked file, running sub-processors and adding states to the repository if required. To implement a processor, it is required to use the following extension :

	<!ELEMENT processorType (prereq)*>		<!ELEMENT processorType (prereq)*>