Adding Automatic Inference Reasoners - Revision history

imported>Nicolas at 17:34, 24 November 2010

2010-11-24T17:34:04Z

← Older revision		Revision as of 17:34, 24 November 2010
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
			''Please also have a look at'' [[How_To_Evolve_Reasoners\| How To Evolve Reasoners]].


	Beside the input sequent, reasoners of this type does not have any extra input and automatically applies an inference rule to the input sequent. As an example, consider the following inference rule (called ''IMP_R'').		Beside the input sequent, reasoners of this type does not have any extra input and automatically applies an inference rule to the input sequent. As an example, consider the following inference rule (called ''IMP_R'').

imported>Nicolas: /* Implement the Reasoner */ Added link to Versioned Reasoners

2009-10-06T18:03:44Z

Implement the Reasoner: Added link to Versioned Reasoners

← Older revision		Revision as of 18:03, 6 October 2009
Line 143:		Line 143:
	** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>.		** Tom is used here to do pattern matching. In our case, match the goal with <math>P \limp Q</math>.
	** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''.		** Methods for construct hypothesis actions, antecedent, etc. can be found in class ''org.eventb.core.seqprover.ProverFactory''.

			Note: in order to avoid problems with subsequent reasoner implementation evolutions, it would be wise to implement a [[Versioned Reasoners\|versioned reasoner]] (one more simple method).

	== Setting up Tom ==		== Setting up Tom ==

imported>Mathieu: cat + tocright

2008-09-17T16:54:46Z

cat + tocright

← Older revision		Revision as of 16:54, 17 September 2008
Line 1:		Line 1:
			{{TOCright}}
	Beside the input sequent, reasoners of this type does not have any extra input and automatically applies an inference rule to the input sequent. As an example, consider the following inference rule (called ''IMP_R'').		Beside the input sequent, reasoners of this type does not have any extra input and automatically applies an inference rule to the input sequent. As an example, consider the following inference rule (called ''IMP_R'').

Line 258:		Line 259:
	** The method return a list of strings.		** The method return a list of strings.
	** Each string represent an invalid input sequent for the reasoner.		** Each string represent an invalid input sequent for the reasoner.

			[[Category:Developer documentation]]
			[[Category:Rodin Platform]]

imported>Son: /* Test the Reasoner */

2008-09-16T12:38:55Z

Test the Reasoner

← Older revision		Revision as of 12:38, 16 September 2008
Line 254:		Line 254:
	** The constructor of ''SuccessfulTest'' has two arguments: A string represent the input sequent and a string to represent the output sequents.		** The constructor of ''SuccessfulTest'' has two arguments: A string represent the input sequent and a string to represent the output sequents.
	** The format of these sequents can be found in the class ''AbstractAutoInferenceTests''.		** The format of these sequents can be found in the class ''AbstractAutoInferenceTests''.


	* Lastly, by implementing the method ''getUnsuccessfulTests()'', clients test the reasoner against invalid input.		* Lastly, by implementing the method ''getUnsuccessfulTests()'', clients test the reasoner against invalid input.
	** The method return a list of strings.		** The method return a list of strings.
	** Each string represent an invalid input sequent for the reasoner.		** Each string represent an invalid input sequent for the reasoner.

imported>Son: /* Test the Reasoner */

2008-09-16T12:38:43Z

Test the Reasoner

← Older revision		Revision as of 12:38, 16 September 2008
Line 232:		Line 232:
	protected String[] getUnsuccessfulTests() {		protected String[] getUnsuccessfulTests() {
	return new String[] {		return new String[] {
	"x = 1 ⇒ y = 2 \|- z = 3",		"x = 1 ⇒ y = 2 ;H; x = 1 ⇒ y = 2 ;S; \|- z = 3",
	"z = 2 \|- z = 3 ∧ (x = 1 ⇒ y = 2)",		"x = 1 ⇒ y = 2 ;H; ;S; x = 1 ⇒ y = 2 \|- z = 3",
			"x = 1 ⇒ y = 2 ;H; ;S; \|- z = 3",
			"z = 2 ;H; z = 2 ;S; \|- z = 3 ∧ (x = 1 ⇒ y = 2)",
			"z = 2 ;H; ;S; z = 2 \|- z = 3 ∧ (x = 1 ⇒ y = 2)",
			"z = 2 ;H; ;S; \|- z = 3 ∧ (x = 1 ⇒ y = 2)"
	};		};
	}		}
Line 244:		Line 248:
	}		}

	* ~~First~~, by implementing the method ''getReasonerID()'', clients test the declaration of the reasoner.		* Firstly, by implementing the method ''getReasonerID()'', clients test the declaration of the reasoner.

	* ~~Second~~, by implementing the method ''getSuccessfulTests()'', clients test the successful application of the reasoner.		* Secondly, by implementing the method ''getSuccessfulTests()'', clients test the successful application of the reasoner.
	** The method return a list of ''SuccessfulTest''.		** The method return a list of ''SuccessfulTest''.
	** The constructor of ''SuccessfulTest'' has two arguments: A string represent the input sequent and a string to represent the output sequents.		** The constructor of ''SuccessfulTest'' has two arguments: A string represent the input sequent and a string to represent the output sequents.
	** The format of these sequents can be found in the class ''AbstractAutoInferenceTests''.		** The format of these sequents can be found in the class ''AbstractAutoInferenceTests''.


			* Lastly, by implementing the method ''getUnsuccessfulTests()'', clients test the reasoner against invalid input.
			** The method return a list of strings.
			** Each string represent an invalid input sequent for the reasoner.

imported>Son: /* Test the Reasoner */

2008-09-16T12:34:04Z

Test the Reasoner

@@ Line 211: / Line 211: @@
 * Create a package for the tests, e.g. ''org.eventb.internal.contributors.seqprover.implinference.tests''
-* Create a new class within the newly created package. This class will extend this abstract test class ''org.eventb.core.seqprover.rewriterTests.AbstractAutoInferenceTests''.
+* Create a new class within the newly created package. This class will extend this abstract test class ''org.eventb.core.seqprover.eventbExtentionTests.AbstractAutoInferenceTests''.
 * The content of the test class is as follows

imported>Son: /* Test the Reasoner */

2008-09-16T12:29:31Z

Test the Reasoner

← Older revision		Revision as of 12:29, 16 September 2008
Line 203:		Line 203:

	== Test the Reasoner ==		== Test the Reasoner ==
			Follow the steps below to create a test for declaration of the newly created reasoner.

			* Create a test plug-in project, e.g. ''org.eventb.contributors.seqprover.implinference.tests''

			* Create dependencies on ''org.eventb.core.seqprover.tests'' and the project under test (in our example, it is ''org.eventb.contributors.seqprover.implinference''.

			* Create a package for the tests, e.g. ''org.eventb.internal.contributors.seqprover.implinference.tests''

			* Create a new class within the newly created package. This class will extend this abstract test class ''org.eventb.core.seqprover.rewriterTests.AbstractAutoInferenceTests''.

			* The content of the test class is as follows

imported>Son: /* Setting up Tom */

2008-09-16T12:27:27Z

Setting up Tom

← Older revision		Revision as of 12:27, 16 September 2008
Line 183:		Line 183:

	The best way to create this file is to copy from org.eventb.core.seqprover project, and modify this accordingly.		The best way to create this file is to copy from org.eventb.core.seqprover project, and modify this accordingly.


	* Right click on the name of your project and choose Properties.		* Right click on the name of your project and choose Properties.
Line 202:		Line 201:

	* The Tom Builder should run and generate the Java implementation for AutoInference.java in the specified folder.		* The Tom Builder should run and generate the Java implementation for AutoInference.java in the specified folder.

			== Test the Reasoner ==

imported>Son: /* Setting up Tom */

2008-09-16T12:24:53Z

Setting up Tom

← Older revision		Revision as of 12:24, 16 September 2008
Line 181:		Line 181:

	</project>		</project>

			The best way to create this file is to copy from org.eventb.core.seqprover project, and modify this accordingly.


			* Right click on the name of your project and choose Properties.
			* Choose "Builders", then click on "New" and choose "Ant Build" and click OK. A dialog will open for new builder wizard.
			* At the ''Main'' tab:
			** Enter the name of the builder, e.g. ''Tom Builder''.
			** Buildfile: ''Browse Workspace'' to your ''build-tom.xml''.
			** Base Directory: ''Variables'' and choose ''build_project''.
			* At the ''Targets'' tab:
			** Auto Build: Click ''Set Targets'' and choose "tom" from the list.
			** During a "clean": Click "Set Targets" and choose ''clean'' (unchecked ''tom'').

			* At the ''Refresh'' tab: Choose "Refresh resource upon completion", and "Specific resources". Click "Specify Resources" and browse to the location of the folder contains the Tom file. In our example, it will be ''src/org/eventb/internal/contributors/seqprover/implinference''

			* At the ''Build Options'' tab: Click "Specify working set of relevant resources". Click "Specify Resources" and browse to the Tom file, i.e. "AutoInference.t".

			* Click Apply and OK to close the dialog.

			* The Tom Builder should run and generate the Java implementation for AutoInference.java in the specified folder.

imported>Son: /* Setting up Tom */

2008-09-16T12:21:20Z

Setting up Tom

← Older revision		Revision as of 12:21, 16 September 2008
Line 144:		Line 144:

	== Setting up Tom ==		== Setting up Tom ==
			* Create a file named build-tom.xml within your project. The content of the file looks like this.

			<project name="org.eventb.contributors.seqprover.implrewrites" default="tom" basedir=".">
			<description>
			Generates derived files in the Sequent Prover.
			</description>

			<!-- set global properties for this build -->
			<property name="src" location="src" />

			<property name="org.eventb.core.ast.home" location="../org.eventb.core.ast" />
			<import file="${org.eventb.core.ast.home}/tom/tom-task.xml"/>

			<property name="inference.src"
			location="${src}/org/eventb/internal/contributors/seqprover/implinference" />

			<target name="init" description="Create the initial time stamp">
			<tstamp />
			</target>

			<target name="tom" depends="init"
			description="Launch tom for all files">
			<tom config="${tom.home}/Tom.xml"
			srcdir="${src}"
			destdir="${src}"
			options="-I ${org.eventb.core.ast.home}/tom --static"
			pretty="true"
			optimize="true">
			<include name="*/.t" />
			</tom>
			</target>

			<target name="clean" description="clean up">
			<delete file="${inference.src}/AutoInference.java" />
			</target>

			</project>