BSynthesis - Revision history

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:55:40Z

Program Synthesis

← Older revision		Revision as of 17:55, 27 January 2021
Line 112:		Line 112:
	* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).		* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).

	The described example's code can be found here: [[https://github.com/Joshua27/ProBramSynthesis]]		The described example's code can be found here: [https://github.com/Joshua27/ProBramSynthesis ProBramSynthesis]

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:54:19Z

Program Synthesis

← Older revision		Revision as of 17:54, 27 January 2021
Line 112:		Line 112:
	* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).		* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).

	The described example's code can be found here: [https://github.com/Joshua27/ProBramSynthesis~~\|ProBramSynthesis~~]		The described example's code can be found here: [[https://github.com/Joshua27/ProBramSynthesis]]

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:53:52Z

Program Synthesis

← Older revision		Revision as of 17:53, 27 January 2021
Line 112:		Line 112:
	* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).		* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).

	The described example's code can be found here: [https://github.com/Joshua27/ProBramSynthesis]		The described example's code can be found here: [https://github.com/Joshua27/ProBramSynthesis\|ProBramSynthesis]

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:52:43Z

Program Synthesis

← Older revision		Revision as of 17:52, 27 January 2021
Line 111:		Line 111:
	* <b>EXPLICIT</b>: Use explicit if-then-else expressions as supported by ProB (this might be slow depending on the problem at hand).		* <b>EXPLICIT</b>: Use explicit if-then-else expressions as supported by ProB (this might be slow depending on the problem at hand).
	* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).		* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).

			The described example's code can be found here: [https://github.com/Joshua27/ProBramSynthesis]

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:49:21Z

Program Synthesis

← Older revision		Revision as of 17:49, 27 January 2021
Line 89:		Line 89:
	}		}
	</pre>		</pre>
	Note, we do not provide any negative examples but pass an empty set. If we would provide negative input-output examples, an appropriate precondition would be synthesized for the machine operation. That is, the synthesized operation is enabled for the inputs of the positive examples and disabled for the inputs of the negative examples.		Note that we do not provide any negative examples but pass an empty set. If we would provide negative input-output examples, an appropriate precondition would be synthesized for the machine operation. That is, the synthesized operation is enabled for the inputs of the positive examples and disabled for the inputs of the negative examples.

	The employed synthesis technique is based on the combination of program components and, thus, requires a predefined set of library components. For instance, an integer addition is such a library component. If using synthesis as described above, a default library configuration is used. This default configuration tries to use as little components as possible and successively intermingles components or increases the amount of specific components if no solution can be found using the current library configuration. As this default library configuration is mainly selected randomly, synthesis possibly lacks for performance compared to using the exact library of components that is necessary to synthesize a program. To that effect, the user is also able to specify the exact library configuration to be considered during synthesis. We provide the class <b>BLibrary</b> to create a specific library configuration.		The employed synthesis technique is based on the combination of program components and, thus, requires a predefined set of library components. For instance, an integer addition is such a library component. If using synthesis as described above, a default library configuration is used. This default configuration tries to use as little components as possible and successively intermingles components or increases the amount of specific components if no solution can be found using the current library configuration. As this default library configuration is mainly selected randomly, synthesis possibly lacks for performance compared to using the exact library of components that is necessary to synthesize a program. To that effect, the user is also able to specify the exact library configuration to be considered during synthesis. We provide the class <b>BLibrary</b> to create a specific library configuration.

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:48:41Z

Program Synthesis

← Older revision		Revision as of 17:48, 27 January 2021
Line 47:		Line 47:
	negativeExamples.add(new Example().addf(new VariableExample("floor", "-2")));		negativeExamples.add(new Example().addf(new VariableExample("floor", "-2")));
	</pre>		</pre>
	~~Note that the~~ method <b>addf()</b> is just a wrapper for a Java set's <b>add()</b> method enabling a functional style.		The method <b>addf()</b> is just a wrapper for a Java set's <b>add()</b> method enabling a functional style.
	Afterwards, we are able to run synthesis using <b>synthesizePredicate()</b>:		Afterwards, we are able to run synthesis using <b>synthesizePredicate()</b>:
	<pre>		<pre>

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:48:23Z

Program Synthesis

← Older revision		Revision as of 17:48, 27 January 2021
Line 47:		Line 47:
	negativeExamples.add(new Example().addf(new VariableExample("floor", "-2")));		negativeExamples.add(new Example().addf(new VariableExample("floor", "-2")));
	</pre>		</pre>
	Note, the method <b>addf()</b> is just a wrapper for a Java set's <b>add()</b> method enabling a functional style.		Note that the method <b>addf()</b> is just a wrapper for a Java set's <b>add()</b> method enabling a functional style.
	Afterwards, we are able to run synthesis using <b>synthesizePredicate()</b>:		Afterwards, we are able to run synthesis using <b>synthesizePredicate()</b>:
	<pre>		<pre>

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:47:51Z

Program Synthesis

← Older revision		Revision as of 17:47, 27 January 2021
Line 47:		Line 47:
	negativeExamples.add(new Example().addf(new VariableExample("floor", "-2")));		negativeExamples.add(new Example().addf(new VariableExample("floor", "-2")));
	</pre>		</pre>
	Note, the method addf() is just a wrapper for a Java set's add() method enabling a functional style.		Note, the method <b>addf()</b> is just a wrapper for a Java set's <b>add()</b> method enabling a functional style.
	Afterwards, we are able to run synthesis using synthesizePredicate():		Afterwards, we are able to run synthesis using <b>synthesizePredicate()</b>:
	<pre>		<pre>
	try {		try {
Line 60:		Line 60:
	}		}
	</pre>		</pre>
	A BSynthesisResult is either a program or a distinguishing example depending on the selected synthesis mode.		A <b>BSynthesisResult</b> is either a program or a distinguishing example depending on the selected synthesis mode.
	If synthesis fails, an exception is thrown providing an appropriate error message.		If synthesis fails, an exception is thrown providing an appropriate error message.

Line 91:		Line 91:
	Note, we do not provide any negative examples but pass an empty set. If we would provide negative input-output examples, an appropriate precondition would be synthesized for the machine operation. That is, the synthesized operation is enabled for the inputs of the positive examples and disabled for the inputs of the negative examples.		Note, we do not provide any negative examples but pass an empty set. If we would provide negative input-output examples, an appropriate precondition would be synthesized for the machine operation. That is, the synthesized operation is enabled for the inputs of the positive examples and disabled for the inputs of the negative examples.

	The employed synthesis technique is based on the combination of program components and, thus, requires a predefined set of library components. For instance, an integer addition is such a library component. If using synthesis as described above, a default library configuration is used. This default configuration tries to use as little components as possible and successively intermingles components or increases the amount of specific components if no solution can be found using the current library configuration. As this default library configuration is mainly selected randomly, synthesis possibly lacks for performance compared to using the exact library of components that is necessary to synthesize a program. To that effect, the user is also able to specify the exact library configuration to be considered during synthesis. We provide the class BLibrary to create a specific library configuration.		The employed synthesis technique is based on the combination of program components and, thus, requires a predefined set of library components. For instance, an integer addition is such a library component. If using synthesis as described above, a default library configuration is used. This default configuration tries to use as little components as possible and successively intermingles components or increases the amount of specific components if no solution can be found using the current library configuration. As this default library configuration is mainly selected randomly, synthesis possibly lacks for performance compared to using the exact library of components that is necessary to synthesize a program. To that effect, the user is also able to specify the exact library configuration to be considered during synthesis. We provide the class <b>BLibrary</b> to create a specific library configuration.

	The enum LibraryComponentName provides all B components that are supported by the synthesis backend. Constructing a BLibrary object provides an empty library ~~considerings~~ the default configuration. We thus have to state that we want to use a specific library of components only and add the desired components using their names. For instance, we want to create a component library using an integer addition and subtraction:		The enum <b>LibraryComponentName</b> provides all B components that are supported by the synthesis backend. Constructing a BLibrary object provides an empty library considering the default configuration. We thus have to state that we want to use a specific library of components only and add the desired components using their names. For instance, we want to create a component library using an integer addition and subtraction:
	<pre>		<pre>
	BLibrary lib = new BLibrary();		BLibrary lib = new BLibrary();
Line 100:		Line 100:
	lib.addLibraryComponent(LibraryComponentName.MINUS);		lib.addLibraryComponent(LibraryComponentName.MINUS);
	</pre>		</pre>
	A BLibrary object can be passed as the third argument for synthesizePredicate() and synthesizeOperation() respectively.		A BLibrary object can be passed as the third argument for <b>synthesizePredicate()</b> and <b>synthesizeOperation()</b> respectively.

	The employed synthesis technique is based on constraint solving and, thus, each component has a unique output within a synthesized program. For instance, to synthesize the predicate "x + y + z > 2" we need two addition components. There are three ways to adapt the amount how often a specific component should be considered:		The employed synthesis technique is based on constraint solving and, thus, each component has a unique output within a synthesized program. For instance, to synthesize the predicate "x + y + z > 2" we need two addition components. There are three ways to adapt the amount how often a specific component should be considered:
	* Use addLibraryComponent(LibraryComponentName) several times.		* Use <b>addLibraryComponent(LibraryComponentName) </b>several times.
	* Use updateComponentAmount(LibraryComponentName,AddAmount) adding the second argument to the amount of the specific component.		* Use <b>updateComponentAmount(LibraryComponentName,AddAmount)</b> adding the second argument to the amount of the specific component.
	* Use setComponentAmount(LibraryComponentName,Amount) explicitly setting a component's amount.		* Use <b>setComponentAmount(LibraryComponentName,Amount)</b> explicitly setting a component's amount.
	Moreover, one can define whether synthesis should consider constants that have to be enumerated by the solver by using the method setEnumerateConstants(). If is false, only constants that are in the scope of the currently loaded machine are considered. For instance, if the current machine does not define any integer constant and we want to synthesize a predicate "x + 1 > y" the constraint solver needs to enumerate an integer constant to the value of 1 to achieve the desired behavior.		Moreover, one can define whether synthesis should consider constants that have to be enumerated by the solver by using the method <b>setEnumerateConstants()</b>. If is false, only constants that are in the scope of the currently loaded machine are considered. For instance, if the current machine does not define any integer constant and we want to synthesize a predicate "x + 1 > y" the constraint solver needs to enumerate an integer constant to the value of 1 to achieve the desired behavior.
	If synthesizing an operation, one can further define whether if-statements should be considered during synthesis represented by the enum ConsiderIfType. There are three possibilities:		If synthesizing an operation, one can further define whether if-statements should be considered during synthesis represented by the enum <b>ConsiderIfType</b>. There are three possibilities:
	* NONE: Do not consider if-statements.		* <b>NONE</b>: Do not consider if-statements.
	* EXPLICIT: Use explicit if-then-else expressions as supported by ProB (this might be slow depending on the problem at hand).		* <b>EXPLICIT</b>: Use explicit if-then-else expressions as supported by ProB (this might be slow depending on the problem at hand).
	* IMPLICIT: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).		* <b>IMPLICIT</b>: Do not use explicit if-statements but possibly synthesize several machine operations with appropriate preconditions instead (semantically equivalent to using explicit if-statements in a single machine operation).

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:44:54Z

Program Synthesis

← Older revision		Revision as of 17:44, 27 January 2021
Line 23:		Line 23:
	** If we find another non-equivalent program, we search for an example distinguishing both programs referred to as a distinguishing example. That is, an input state for which both programs yield different outputs. This example can be validated by the user and be considered in the set of examples for another run of synthesis possibly guiding synthesis to a unique solution. For instance, assume we want to synthesize a B predicate by providing a set of positive and negative examples and synthesis has found the predicate "x > 0" first. Assuming the examples describe ambiguous behavior synthesis may find another non-equivalent predicate "x > 1". A distinguishing example would then be "x = 1" as the first predicate is true and the second one is false for this input.		** If we find another non-equivalent program, we search for an example distinguishing both programs referred to as a distinguishing example. That is, an input state for which both programs yield different outputs. This example can be validated by the user and be considered in the set of examples for another run of synthesis possibly guiding synthesis to a unique solution. For instance, assume we want to synthesize a B predicate by providing a set of positive and negative examples and synthesis has found the predicate "x > 0" first. Assuming the examples describe ambiguous behavior synthesis may find another non-equivalent predicate "x > 1". A distinguishing example would then be "x = 1" as the first predicate is true and the second one is false for this input.
	The synthesis mode can be set using the method <b>setSynthesisMode()</b>:		The synthesis mode can be set using the method <b>setSynthesisMode()</b>:
			<pre>
	synthesizer.setSynthesisMode(SynthesisMode.INTERACTIVE);		synthesizer.setSynthesisMode(SynthesisMode.INTERACTIVE);
			</pre>
	We provide three classes to create examples:		We provide three classes to create examples:
	* <b>VariableExample.java</b>: An example for a single machine variable consisting of the machine variable's name and its pretty printed B value.		* <b>VariableExample.java</b>: An example for a single machine variable consisting of the machine variable's name and its pretty printed B value.

Joshua Schmidt: /* Program Synthesis */

2021-01-27T17:36:52Z

Program Synthesis

← Older revision		Revision as of 17:36, 27 January 2021
Line 17:		Line 17:
	Using input-output examples to specify the behavior of a program is most comfortable for the user but most difficult for program synthesis itself. As input-output examples possibly describe ambiguous behavior we provide two modes for synthesis:		Using input-output examples to specify the behavior of a program is most comfortable for the user but most difficult for program synthesis itself. As input-output examples possibly describe ambiguous behavior we provide two modes for synthesis:

	* FIRST_SOLUTION: Return the first solution found.		* <b>FIRST_SOLUTION</b>: Return the first solution found.
	* INTERACTIVE: Search for another non-equivalent program after finding a solution. There are three possible outcomes:		* <b>INTERACTIVE</b>: Search for another non-equivalent program after finding a solution. There are three possible outcomes:
	* If the constraint solver finds a contradiction, we have found a unique solution and return the program synthesized so far.		** If the constraint solver finds a contradiction, we have found a unique solution and return the program synthesized so far.
	* If the constraint solver cannot find a solution because of exceeding the solver timeout, we return the program synthesized so far. On the one hand, this program might not be the one expected by the user if the examples describe ambiguous behavior. On the other hand, a synthesized program does always satisfy the provided examples. Thus, in practice, completeness depends on the selected solver timeout.		** If the constraint solver cannot find a solution because of exceeding the solver timeout, we return the program synthesized so far. On the one hand, this program might not be the one expected by the user if the examples describe ambiguous behavior. On the other hand, a synthesized program does always satisfy the provided examples. Thus, in practice, completeness depends on the selected solver timeout.
	* If we find another non-equivalent program, we search for an example distinguishing both programs referred to as a distinguishing example. That is, an input state for which both programs yield different outputs. This example can be validated by the user and be considered in the set of examples for another run of synthesis possibly guiding synthesis to a unique solution. For instance, assume we want to synthesize a B predicate by providing a set of positive and negative examples and synthesis has found the predicate "x > 0" first. Assuming the examples describe ambiguous behavior synthesis may find another non-equivalent predicate "x > 1". A distinguishing example would then be "x = 1" as the first predicate is true and the second one is false for this input.		** If we find another non-equivalent program, we search for an example distinguishing both programs referred to as a distinguishing example. That is, an input state for which both programs yield different outputs. This example can be validated by the user and be considered in the set of examples for another run of synthesis possibly guiding synthesis to a unique solution. For instance, assume we want to synthesize a B predicate by providing a set of positive and negative examples and synthesis has found the predicate "x > 0" first. Assuming the examples describe ambiguous behavior synthesis may find another non-equivalent predicate "x > 1". A distinguishing example would then be "x = 1" as the first predicate is true and the second one is false for this input.
	The synthesis mode can be set using the method <b>setSynthesisMode()</b>:		The synthesis mode can be set using the method <b>setSynthesisMode()</b>:
	synthesizer.setSynthesisMode(SynthesisMode.INTERACTIVE);		synthesizer.setSynthesisMode(SynthesisMode.INTERACTIVE);