1		:- module(b_synthesis, [start_synthesis_from_ui/11,
2		start_synthesis_from_ui/13,
3		start_synthesis_single_operation_from_ui/11,
4		reset_synthesis_context/0]).
5
6		:- use_module(synthesis(logging)).
7		:- use_module(synthesis(constraints)).
8		:- use_module(synthesis(library_setup)).
9		:- use_module(synthesis(location_vars_to_program)).
10		:- use_module(synthesis(synthesis_util)).
11
12		:- use_module(probsrc(bsyntaxtree)).
13		:- use_module(probsrc(bmachine), [b_get_machine_set/1,b_get_machine_set/2,b_get_machine_operation/4]).
14		:- use_module(probsrc(preferences), [set_preference/2]).
15		:- use_module(probsrc(module_information), [module_info/2]).
16		:- use_module(probsrc(solver_interface), [solve_predicate/3]).
17		:- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate/4]).
18
19		:- use_module(library(lists)).
20		:- use_module(library(sets), [intersection/3]).
21		:- use_module(library(terms), [term_size/2]).
22
23		:- use_module(extension('plspec/plspec/plspec_core')).
24
25		:- defspec(solution_bindings, one_of([list(compound(binding(any,any,any))),list(compound(bind(any,any)))])).
26		:- defspec(solution_compound, compound(solution(solution_bindings))).
27		:- defspec(ast_example, list(ast)).
28		:- defspec(ast_examples, list(ast_example)).
29		:- defspec(ast, compound(b(any,any,list(any)))).
30		:- defspec(pair(X,Y), compound(','(X,Y))).
31		% :- enable_all_spec_checks.
32		:- module_info(group, synthesis).
33		:- module_info(description, 'This module contains the synthesis workflow following the approach by Gulwani et.al. using SMT solving').
34
35		% The synthesis context storing the current state of synthesis when the workflow has been interrupted to interact with the user.
36		:- dynamic synthesis_context/9.
37		:- volatile synthesis_context/9.
38
39		% The solver to be used for synthesis which is either ProB (default) or Z3.
40		:- dynamic solver/1.
41		:- volatile solver/1.
42		solver(proB).
43
44		% Library components selected by the user or a specific default configuration like 'default:1' to parallelize library expansions
45		% from the Java UI. Default configuration is used if the predicate does not exist. If is 'default' the library is expanded successively
46		% in prolog using synthesis_callback/16 on a single instance.
47		:- dynamic library_from_ui/1.
48		:- volatile library_from_ui/1.
49
50		% The names of machine variables that we want to consider if-statements for.
51		:- dynamic consider_if_var_names/1.
52		:- volatile consider_if_var_names/1.
53
54		% Determines whether to use constants during synthesis that are assigned by the solver.
55		:- dynamic not_consider_constants/1.
56		:- volatile not_consider_constants/1.
57
58		% Additional machinevars for operation parameters when synthesizing a precondition.
59		:- dynamic additional_machinevars/1.
60		:- volatile additional_machinevars/1.
61		additional_machinevars([]).
62
63		% Synthesis mode is either first_solution or interactive.
64		:- dynamic synthesis_mode/1.
65		:- volatile synthesis_mode/1.
66		synthesis_mode(interactive).
67
68		% Expand library in case a solution has been found using the default library configuration.
69		% :- dynamic current_library_lookahead/1.
70		% :- volatile current_library_lookahead/1.
71		% max_library_lookahead(3).
72		max_library_expansion(30).
73
74		% TO DO: - use sets instead of lists
75		% - improve detection of variables taking part in an invariant violation
76		% -> keep the current analysis and filter those vars that have changed in the transition leading to the invariant violation
77		% - equal_object
78		% Start synthesis from the UI based on the ProB2 Java API. Returns the adapted machine code with
79		% the generated changes if synthesis succeeded. Otherwise, the unchanged machine code is returned or a distinguishing example in case two
80		% non equivalent programs have been synthesized.
81		start_synthesis_from_ui(SolverTimeOut, Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Operation, SynthesisType, Positive, Negative, NewMachineAtom, Distinguishing) :-
82		synthesis_mode(SynthesisMode),
83		start_synthesis_from_ui(SynthesisMode, yes, SolverTimeOut, Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Operation, SynthesisType, Positive, Negative, NewMachineAtom, Distinguishing).
84		start_synthesis_from_ui(SynthesisMode, AdaptMachineCode, SolverTimeOut, Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Operation, SynthesisType, Positive, Negative, NewMachineAtom, Distinguishing) :-
85		set_preference(time_out, SolverTimeOut),
86		logging:enable_logging,
87		set_synthesis_mode(SynthesisMode),
88		prepare_synthesis(Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Positive, Negative, PosInput, PosOutput, NegInput, NegOutput),
89		start_synthesis_from_ui_aux(Operation, SynthesisType, (PosInput,PosOutput), (NegInput,NegOutput), (_,Synthesized)),
90		!,
91		prepare_solution(AdaptMachineCode, Operation, SynthesisType, Synthesized, NewMachineAtom, Distinguishing),
92		retract_context_if_solution(Distinguishing).
93
94		set_synthesis_mode(SynthesisMode) :-
95		retractall(synthesis_mode(_)),
96		assert(synthesis_mode(SynthesisMode)).
97
98		% Implicitly consider if-statements, i.e., synthesize several operations describing the different semantics of the examples.
99		% Here, we start synthesize for a single example but consider more examples if synthesis has been suspended because of finding a distinguishing example.
100		start_synthesis_single_operation_from_ui(SolverTimeOut, Operations, Library, DoNotUseConstants, Solver, Operation, action, Positive, Negative, CacheOperationTuple, Distinguishing) :-
101		set_preference(time_out, SolverTimeOut),
102		% TODO: consider the other examples to check against distinguishing examples, this is not essential though and works as is
103		prepare_synthesis(Library, DoNotUseConstants, Solver, [], Positive, Negative, PosInput, PosOutput, NegInput, NegOutput),
104		( Operations = []
105		->
106		Result = no_match
107		; maplist(cache_operation_tuple_to_quadruple, Operations, OperationQuadruples),
108		PosInput = [Input],
109		PosOutput = [Output],
110		findall(UsedID, ( member(Value, Input),
111		get_texpr_info(Value, Info),
112		member(synthesis(machinevar,UsedID), Info)
113		), UsedIDs),
114		get_machinevars_by_name(UsedIDs, UsedIDNodes),
115		check_transition_against_machine_operations(OperationQuadruples, Input, Output, UsedIDNodes, Result)
116		),
117		start_synthesis_single_operation_from_ui_aux(Result, Operations, Operation, PosInput, PosOutput, NegInput, NegOutput, CacheOperationTuple, Distinguishing),
118		retract_context_if_solution(Distinguishing).
119
120		start_synthesis_single_operation_from_ui_aux((OperationName,done), _, _, _, _, _, _, done(OperationName,done), none).
121		start_synthesis_single_operation_from_ui_aux((OperationName,guard), Operations, _, PosInput, _, NegInput, _, FinalOperation, Distinguishing) :-
122		get_distinguishing_state_cache_from_operation_tuples(Operations, OperationName, (CachePos,CacheNeg), Operation),
123		append(PosInput, CachePos, Positive),
124		append(NegInput, CacheNeg, Negative),
125		start_synthesis_from_ui_aux(OperationName, guard, (Positive,_), (Negative,_), (_,SynthesizedGuard)),
126		!,
127		prepare_solution(yes, Operation, guard, SynthesizedGuard, _, Distinguishing),
128		( is_distinguishing(SynthesizedGuard) ->
129		FinalOperation = none
130		; replace_precondition_of_operation(Operation, SynthesizedGuard, FinalOperation)
131		).
132		start_synthesis_single_operation_from_ui_aux(no_match, _, Operation, PosInput, PosOutput, NegInput, NegOutput, CacheOperationTuple, Distinguishing) :-
133		start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,Synthesized)),
134		!,
135		prepare_solution(yes, Operation, action, Synthesized, _, Distinguishing),
136		( is_distinguishing(Synthesized) ->
137		CacheOperationTuple = none
138		; CacheOperationTuple = (DistStateCache,Synthesized)
139		).
140
141		prepare_synthesis(Library, DoNotUseConstants, Solver, ConsiderIfVarNames, Positive, Negative, PosInput, PosOutput, NegInput, NegOutput) :-
142		% retractall(current_library_lookahead(_)) ,
143		% asserta(current_library_lookahead(0)) ,
144		retractall(solver(_)),
145		asserta(solver(Solver)),
146		retractall(not_consider_constants(_)),
147		asserta(not_consider_constants(DoNotUseConstants)),
148		assert_library_configuration_from_ui(Library),
149		assert_if_statement_var_names(ConsiderIfVarNames),
150		% split examples that are tuples of input and output state
151		split_input_output_tuples(Positive, PosInput, PosOutput),
152		split_input_output_tuples(Negative, NegInput, NegOutput),
153		!.
154
155		/* filter_new_examples(Input,Output,OldInput,NewInput,NewOutput) :-
156		filter_new_examples(Input,Output,OldInput,[],[],NewInput,NewOutput).
157
158		filter_new_examples([],[],_,AccInput,AccOutput,AccInput,AccOutput).
159		filter_new_examples([Input|TI],[Output|TO],OldInput,AccInput,AccOutput,NewInput,NewOutput) :-
160		\+ contains_equivalent_state(Input,OldInput,_) , ! ,
161		filter_new_examples(TI,TO,OldInput,[Input|AccInput],[Output|AccOutput],NewInput,NewOutput).
162		filter_new_examples([_|TI],[_|TO],OldInput,AccInput,AccOutput,NewInput,NewOutput) :-
163		filter_new_examples(TI,TO,OldInput,AccInput,AccOutput,NewInput,NewOutput). */
164		start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,FinalAction)) :-
165		% synthesizing the action already succeeded but synthesizing an appropriate guard afterwards has been suspended by
166		% finding a distingushing state, the synthesized action is asserted and we just synthesize the guard here
167		on_exception(error(existence_error(_,_),_), synthesis_context(_, DistStateCache, _, PreCondVars, _, guard, OldPosInput, OldNegInput, Action), fail),
168		\+ on_exception(error(existence_error(_,_),_), synthesis_context(_, _, _, _, _, action, _, _, _), fail),
169		Action \== temp(_),
170		!,
171		( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, [Action], ExtendedPosInput, ExtendedNegInput)
172		; PosInput = ExtendedPosInput,
173		NegInput = ExtendedNegInput
174		),
175		keep_asserted_initial_examples(ExtendedPosInput, ExtendedNegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
176		post_synthesize_action(Operation, PreCondVars, NewPosInput, PosOutput, NewNegInput, NegOutput, [], Action, FinalAction).
177		start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (NewDistStateCache,FinalAction)) :-
178		% synthesis type is action but the simultaneous generation of a guard has been suspended by finding a distinguishing state,
179		% synthesizing the action has not succeeded yet
180		on_exception(error(existence_error(_,_),_), synthesis_context(_, PreDistStateCache, _, PreCondVars, ValidInvariantsOrGuards, guard, OldPosInput, OldNegInput, temp(Actions)), fail),
181		retractall(synthesis_context(_, _, _, _, ValidGuards, guard, _, _, _)),
182		( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, Actions, ExtendedPosInput, ExtendedNegInput)
183		; PosInput = ExtendedPosInput,
184		NegInput = ExtendedNegInput
185		),
186		keep_asserted_initial_examples(ExtendedPosInput, ExtendedNegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
187		maplist(get_varname_from_id_node, PreCondVars, PreVarNames),
188		% therefore we start/restart synthesis of a guard
189		synthesized_operation_uses_parameters(Actions, OperationUsesParameters),
190		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreVarNames, (ValidGuards,Operation), NewPosInput, NewNegInput, PrePositive, PreNegative, PreLibrary,
191		PreParameterAmount, PreM1, PreCurrentVars, PreBehavioralConstraint, PreLocationVars, PreSolution),
192		synthesis_from_examples(Operation, b(truth,pred,[]), PreDistStateCache, PreLibrary, 1, PreCurrentVars, PreCurrentVars, ValidInvariantsOrGuards, guard, PrePositive, PreNegative,
193		PreBehavioralConstraint, PreLocationVars, PreM1, PreParameterAmount, PreSolution, PreCondition, NewDistStateCache),
194		distinguishing_state_or_synthesize_action(Operation, PreCondition, NewDistStateCache, (PosInput,PosOutput), (NegInput,NegOutput), FinalAction).
195		start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (NewDistStateCache,FinalAction)) :-
196		% synthesizing an action has been suspended by a distinguishing transition, but the user validated the distinguishing example to be negative
197		\+ on_exception(error(existence_error(_,_),_), synthesis_context(_, _, _, _, _, guard, _, _, _), fail),
198		on_exception(error(existence_error(_,_),_), synthesis_context(_, DistStateCache, _, _, ValidInvariantsOrGuards, action, OldPosInput, OldNegInput, temp(Action)), fail),
199		length(OldPosInput, PLen),
200		length(PosInput, PLen),
201		length(OldNegInput, NLen),
202		length(NegInput, NLen),
203		NegInput \= [],
204		!,
205		( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, [Action], ExtendedPosInput, ExtendedNegInput)
206		; PosInput = ExtendedPosInput,
207		NegInput = ExtendedNegInput
208		),
209		keep_asserted_initial_examples(ExtendedPosInput, ExtendedNegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
210		ExtendedPosInput = [Example|_],
211		maplist(get_varname_from_node_info, Example, PreVarNames),
212		% therefore we start/restart synthesis of a guard
213		synthesized_operation_uses_parameters([Action], OperationUsesParameters),
214		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreVarNames, (ValidInvariantsOrGuards,Operation), NewPosInput, NewNegInput, PrePositive, PreNegative, PreLibrary,
215		PreParameterAmount, PreM1, PreCurrentVars, PreBehavioralConstraint, PreLocationVars, PreSolution),
216		synthesis_from_examples(Operation, b(truth,pred,[]), DistStateCache, PreLibrary, 1, PreCurrentVars, PreCurrentVars, ValidInvariantsOrGuards, guard, PrePositive, PreNegative,
217		PreBehavioralConstraint, PreLocationVars, PreM1, PreParameterAmount, PreSolution, PreCondition, NewDistStateCache),
218		distinguishing_state_or_synthesize_action(Operation, PreCondition, NewDistStateCache, (PosInput,PosOutput), (NegInput,NegOutput), FinalAction).
219		start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), ((PosDistInput,NegDistInput),FinalAction)) :-
220		% synthesizing an action has been suspended by a distinguishing transition, no guard
221		\+ on_exception(error(existence_error(_,_),_), synthesis_context(_, _, _, _, _, guard, _, _, _), fail),
222		on_exception(error(existence_error(_,_),_), synthesis_context(DistTransitionCache, DistStateCache, _, PreCondVars, ValidGuards, action, OldPosInput, OldPosOutput, _), fail),
223		retractall(synthesis_context(_, _, _, _, _, action, _, _, _)),
224		keep_asserted_initial_examples(PosInput, PosOutput, OldPosInput, OldPosOutput, NewPosInput, NewPosOutput),
225		prepare_synthesis_of_action_by_examples(Operation, NewPosInput, NewPosOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution),
226		DistStateCache = (PosDist,NegDist),
227		append(NegInput, NegDist, NewNegDist),
228		synthesis_from_examples(Operation, DistTransitionCache, (PosDist,NewNegDist), Library, 1, CurrentVars, PreCondVars, ValidGuards, action,
229		NewPosInput, NewPosOutput, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, Synthesized, (PosDistInput,NegDistInput)),
230		!,
231		Synthesized \= none,
232		post_synthesize_action(Operation, CurrentVars, NewPosInput, NewPosOutput, NegInput, NegOutput, NegDistInput, Synthesized, FinalAction).
233		start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,Synthesized)) :-
234		% no context asserted, start new synthesis instance for type action,
235		% check if the machine already satisfies the behavior and relax a guard or synthesize a new operation
236		!,
237		behavior_satisfied_or_extend_machine(Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized),
238		( on_exception(error(existence_error(_,_),_), synthesis_context(_, DistStateCache, _, _, _, _, _, _, _), fail)
239		->
240		true
241		; DistStateCache = ([],[])
242		).
243		start_synthesis_from_ui_aux(Operation, SynthesisType, (PosInput,_), (NegInput,_), (DistStateCache,Synthesized)) :-
244		SynthesisType \= action,
245		% go on synthesizing the guard/invariant using the validated distinguishing state
246		on_exception(error(existence_error(_,_),_), synthesis_context(_, PreDistStateCache, _, PreCondVars, ValidInvariantsOrGuards, SynthesisType, OldPosInput, OldNegInput, _), fail),
247		retractall(synthesis_context(_, _, _, _, _, SynthesisType, _, _, _)),
248		keep_asserted_initial_examples(PosInput, NegInput, OldPosInput, OldNegInput, NewPosInput, NewNegInput),
249		maplist(get_varname_from_id_node, PreCondVars, PreVarNames),
250		machine_operation_uses_parameters(Operation, OperationUsesParameters),
251		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreVarNames, (ValidInvariantsOrGuards,Operation), NewPosInput, NewNegInput, PrePositive, PreNegative, PreLibrary, PreParameterAmount, PreM1, PreCurrentVars,
252		PreBehavioralConstraint, PreLocationVars, PreSolution),
253		synthesis_from_examples(Operation, b(truth,pred,[]), PreDistStateCache, PreLibrary, 1, PreCurrentVars, PreCurrentVars, ValidInvariantsOrGuards, SynthesisType, PrePositive,
254		PreNegative, PreBehavioralConstraint, PreLocationVars, PreM1, PreParameterAmount, PreSolution, TSynthesized, DistStateCache),
255		TSynthesized \= none,
256		post_synthesize_predicate(SynthesisType, TSynthesized, Synthesized).
257		start_synthesis_from_ui_aux(Operation, SynthesisType, (PosInput,PosOutput), (NegInput,NegOutput), (DistStateCache,Synthesized)) :-
258		% no context asserted, we start a new synthesis instance
259		\+ on_exception(error(existence_error(_,_),_), synthesis_context(_, _, _, _, _, _, _, _, _), fail),
260		start_specific_synthesis(Operation, SynthesisType, PosInput, NegInput, PosOutput, NegOutput, TSynthesized),
261		!,
262		( on_exception(error(existence_error(_,_),_), synthesis_context(_, DistStateCache, _, _, _, _, _, _, _), fail)
263		->
264		true
265		; DistStateCache = ([],[])
266		),
267		TSynthesized \= none,
268		post_synthesize_predicate(SynthesisType, TSynthesized, Synthesized).
269
270		% Check if an operation already satisfies the provided behavior or if a precondition just has to be relaxed.
271		% Otherwise, synthesize a new operation.
272		behavior_satisfied_or_extend_machine(Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
273		PosInput = [Example|_],
274		get_current_vars_from_example(Example, CurrentVars),
275		check_transitions_against_machine_operations(CurrentVars, PosInput, PosOutput, Result),
276		behavior_satisfied_or_extend_machine_aux(Result, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).
277		% An operation satisfies the provided behavior and no negative input states conflict with the current precondition.
278		% We pass the term operation_satisfied/1 to the UI and no distinguishing example.
279		behavior_satisfied_or_extend_machine_aux((Operation,done), _, _, NegInput, _, _, operation_satisfied(Operation)) :-
280		check_negative_inputs_against_operation_precondition(Operation, NegInput),
281		!.
282		% An operation satisfies the provided behavior but there are negative input states that are valid for the current precondition.
283		% We thus need to synthesize a new precondition.
284		behavior_satisfied_or_extend_machine_aux((Operation,done), _, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
285		behavior_satisfied_or_extend_machine_aux2(guard, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).
286		% A precondition needs to be relaxed.
287		behavior_satisfied_or_extend_machine_aux((Operation,guard), _, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
288		behavior_satisfied_or_extend_machine_aux2(guard, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).
289		% No matching operation, we thus synthesize a new one.
290		behavior_satisfied_or_extend_machine_aux(no_match, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
291		behavior_satisfied_or_extend_machine_aux2(action, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized).
292		% Synthesize guard or action.
293		behavior_satisfied_or_extend_machine_aux2(SynthesisType, Operation, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
294		start_specific_synthesis(Operation, SynthesisType, PosInput, NegInput, PosOutput, NegOutput, Synthesized),
295		!,
296		Synthesized \= none.
297
298		% Synthesizing the action has been suspended and we synthesized a guard.
299		% We derived a distinguishing state.
300		distinguishing_state_or_synthesize_action(_, PreCondition, _, _, _, PreCondition) :-
301		is_distinguishing(PreCondition).
302		% Synthesizing the guard either succeded or failed. The latter means, we can't pass a guard. Thus, we use the old one.
303		% We cached the distinguishing transitions so we try to go on synthesizing the action and maybe
304		% find a guard later depending on the distinguishing interaction with the user.
305		distinguishing_state_or_synthesize_action(Operation, PreCondition, NewDistStateCache, (PosInput,PosOutput), (NegInput,NegOutput), Action) :-
306		% assert the synthesized precondition to the currently suspended synthesis context of the action and restart it
307		synthesis_context(DistTransitionCache, _, CurrentVars, PreCondVars, OldPreCond, action, Input, Output, _),
308		new_or_old_precondition(OldPreCond, PreCondition, NewPreCond),
309		retractall(synthesis_context(_, _, _, _, _, action, _, _, _)),
310		asserta(synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, NewPreCond, action, Input, Output, _)),
311		start_synthesis_from_ui_aux(Operation, action, (PosInput,PosOutput), (NegInput,NegOutput), Action).
312
313		new_or_old_precondition(OldPreCond, none, OldPreCond).
314		new_or_old_precondition(_, PreCond, PreCond) :-
315		PreCond \= none.
316
317		% When synthesizing a guard, we may need to consider operation parameters.
318		% Compute the values of operation parameters for each example and add the parameters to the examples like the other machine variables.
319		add_operation_parameter_values_to_examples([], [], [], [], _, [], []).
320		add_operation_parameter_values_to_examples(PosInput, PosOutput, [], [], Actions, NewPosInput, []) :-
321		add_operation_parameter_values_to_examples(PosInput, PosOutput, Actions, NewPosInput).
322		add_operation_parameter_values_to_examples([], [], NegInput, NegOutput, Actions, [], NewNegInput) :-
323		add_operation_parameter_values_to_examples(NegInput, NegOutput, Actions, NewNegInput).
324		add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, Actions, NewPosInput, NewNegInput) :-
325		add_operation_parameter_values_to_examples(PosInput, PosOutput, Actions, NewPosInput),
326		add_operation_parameter_values_to_examples(NegInput, NegOutput, Actions, NewNegInput).
327
328		add_operation_parameter_values_to_examples(Input, Output, Actions, NewInput) :-
329		Input = [Example|_],
330		maplist(get_varname_from_node_info, Example, CurrentVarNames),
331		maplist(parallel_to_conjunction, Actions, ActionPreds),
332		add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, Input, Output, ParamValues),
333		maplist(append, Input, ParamValues, NewInput).
334
335		add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, Input, Output, ParamValuesList) :-
336		add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, Input, Output, [], ParamValuesList).
337
338		add_operation_parameter_values_to_examples_aux(_, _, [], [], Acc, Acc).
339		add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, [Input|IT], [Output|OT], Acc, ParamValuesList) :-
340		create_before_after_equalities(Input, Output, BAEquality),
341		member(ActionPred, ActionPreds),
342		create_texpr(conjunct(ActionPred,BAEquality), pred, [], BeforeAfterWithEqualities),
343		solve_predicate(BeforeAfterWithEqualities, _, Solution),
344		Solution = solution(SolutionBindings),
345		!,
346		get_operation_parameter_values_from_before_after(CurrentVarNames, SolutionBindings, ParamValues),
347		append(Acc, [ParamValues], NewAcc),
348		add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, IT, OT, NewAcc, ParamValuesList).
349		add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, [Input|IT], [_|OT], Acc, ParamValuesList) :-
350		% we may not find a solution for the operation parameters for negative examples
351		create_equality_nodes_from_example(Input, BeforeEqualityList),
352		conjunct_predicates(BeforeEqualityList, BeforeEquality),
353		member(ActionPred, ActionPreds),
354		create_texpr(conjunct(ActionPred,BeforeEquality), pred, [], BeforeAfterWithEqualities),
355		solve_predicate(BeforeAfterWithEqualities, _, Solution),
356		Solution = solution(SolutionBindings),
357		!,
358		get_operation_parameter_values_from_before_after(CurrentVarNames, SolutionBindings, ParamValues),
359		append(Acc, [ParamValues], NewAcc),
360		add_operation_parameter_values_to_examples_aux(CurrentVarNames, ActionPreds, IT, OT, NewAcc, ParamValuesList).
361
362		get_operation_parameter_values_from_before_after(CurrentVarNames, SolutionBindings, ParamValues) :-
363		% only for those operation parameter that are not part of the current examples
364		findall(ParamBinding, ( member(ParamBinding, SolutionBindings),
365		ParamBinding = binding(TempIdName,_,_),
366		remove_prime(TempIdName, IdName),
367		\+ member(IdName, CurrentVarNames)
368		), ParamBindings),
369		get_operation_parameter_values_from_before_after_aux(ParamBindings, [], ParamValues).
370
371		get_operation_parameter_values_from_before_after_aux([], Acc, Acc).
372		get_operation_parameter_values_from_before_after_aux([binding(ParamName,_,Value)|T], Acc, ParamValues) :-
373		parse_and_typecheck_value(Value, TempValueAst),
374		add_texpr_infos(TempValueAst, [synthesis(initial_example),synthesis(machinevar,ParamName)], ValueAst),
375		create_machinevar(ValueAst),
376		get_operation_parameter_values_from_before_after_aux(T, [ValueAst|Acc], ParamValues).
377
378		% Create machinevars for operation parameters when synthesizing a precondition for an operation using parameters.
379		create_machinevar(b(identifier(IdName),Type,Info)) :-
380		member(synthesis(machinevar,IdName), Info),
381		!,
382		( on_exception(error(existence_error(_,_),_), additional_machinevars(AdditionalMachineVars), fail) ->
383		true
384		; AdditionalMachineVars = []
385		),
386		( \+ member(b(identifier(IdName),Type,Info), AdditionalMachineVars)
387		->
388		create_machinevar_aux(b(identifier(IdName),Type,Info), AdditionalMachineVars)
389		; true
390		).
391		create_machinevar(b(_,Type,Info)) :-
392		member(synthesis(machinevar,IdName), Info),
393		create_machinevar(b(identifier(IdName),Type,Info)).
394
395		create_machinevar_aux(IdNode, AdditionalMachineVars) :-
396		retractall(additional_machinevars(_)),
397		asserta(additional_machinevars([IdNode|AdditionalMachineVars])).
398
399		create_before_after_equalities(In, Out, Equality) :-
400		create_equality_nodes_from_example(In, EqIn),
401		create_equality_nodes_from_example(Out, EqOut),
402		maplist(prime_or_unprime_variables_in_ast(prime, []), EqOut, EqOutPrimed),
403		append(EqIn, EqOutPrimed, Eqs),
404		conjunct_predicates(Eqs, Equality),
405		!.
406
407		post_synthesize_predicate(guard, Synthesized, NewPreCondition) :-
408		find_typed_identifier_uses_with_info(Synthesized, TypedIdentifiers),
409		get_operation_params_from_ids(TypedIdentifiers, Params),
410		Params \= [],
411		!,
412		synthesis_util:set_operation_params_domain(Params, ParamTypeDefsPred),
413		conjunct_predicates([ParamTypeDefsPred,Synthesized], NewPreCondition).
414		post_synthesize_predicate(_, Synthesized, Synthesized).
415
416		% Synthesis returned a distinguishing transition.
417		post_synthesize_action(_, _, _, _, _, _, _, Synthesized, Synthesized) :-
418		is_distinguishing(Synthesized),
419		synthesis_log(solution(_,Synthesized)).
420		% example is given we generate an appropriate guard afterwards.
421		post_synthesize_action(Operation, _Vars, PosInput, PosOutput, NegInput, NegOutput, _NegDistInput, Synthesized, FinalAction) :-
422		\+ is_distinguishing(Synthesized),
423		Synthesized \= none,
424		( add_operation_parameter_values_to_examples(PosInput, PosOutput, NegInput, NegOutput, [Synthesized], NewPosInput, NewNegInput)
425		; PosInput = NewPosInput,
426		NegInput = NewNegInput
427		),
428		NewPosInput = [Example|_],
429		maplist(get_varname_from_node_info, Example, VarNames),
430		synthesize_guard_if_necessary(VarNames, NewPosInput, NewNegInput, Synthesized, Action),
431		post_synthesize_action_aux(Operation, Action, FinalAction).
432		post_synthesize_action_aux(_, Distinguishing, Distinguishing) :-
433		% synthesizing a guard afterwards returned a distinguishing state
434		% the synthesized action is asserted in synthesis_context/9 and will be reused
435		is_distinguishing(Distinguishing).
436		post_synthesize_action_aux(Operation, Action, FinalAction) :-
437		% synthesizing a guard afterwards succeeded or has already been sufficient beforehand, i.e.,
438		% a guard has been synthesized simultaneously when synthesizing the action
439		\+ is_distinguishing(Action),
440		finalize_synthesized_action(Operation, Action, FinalAction),
441		synthesis_log(solution(action,FinalAction)).
442
443		%% synthesize actions, invariants or guards
444		start_specific_synthesis(Operation, action, PosInput, NegInput, PosOutput, NegOutput, Action) :-
445		set_preference(randomise_enumeration_order, true),
446		% no context asserted
447		\+ on_exception(error(existence_error(_,_),_), synthesis_context(_, _, _, _, _, _, _, _, _), fail),
448		mark_examples_as_initial(PosInput, PosOutput, InitialInput, InitialOutput),
449		prepare_synthesis_of_action_by_examples(Operation, InitialInput, InitialOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution),
450		% use the negative input states for the distinguishing state cache
451		synthesis_from_examples(Operation, b(truth,pred,[]), ([],NegInput), Library, 1, CurrentVars, CurrentVars, any, action, InitialInput,
452		InitialOutput, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, Synthesized, (_,NegDistInput)),
453		!,
454		post_synthesize_action(Operation, CurrentVars, InitialInput, InitialOutput, NegInput, NegOutput, NegDistInput, Synthesized, Action).
455		start_specific_synthesis(Operation, action, PosInput, NegInput, PosOutput, _, Action) :-
456		set_preference(randomise_enumeration_order, true),
457		% context asserted, synthesis has been suspended
458		on_exception(error(existence_error(_,_),_), synthesis_context(DistTransitionCache, DistStateCache, CurrentVars, PreCondVars,
459		ValidInvariantsOrGuards, action, OldInput, OldOutput, _), fail),
460		keep_asserted_initial_examples(PosInput, PosOutput, OldInput, OldOutput, NewPosInput, NewPosOutput),
461		start_specific_synthesis_aux(Operation, action, NewPosInput, NegInput, NewPosOutput, _, DistTransitionCache, DistStateCache,
462		CurrentVars, PreCondVars, ValidInvariantsOrGuards, Action).
463
464		% the invariants are explicitly modified by the user, no operation is involved since no invariant violation has been found
465		start_specific_synthesis(null, invariant, PosInput, NegInput, PosOutput, NegOutput, SynthesizedInvariant) :-
466		set_preference(randomise_enumeration_order, true),
467		get_violated_and_valid_machine_invariants(PosOutput, _, _, ValidInvariants),
468		get_positive_and_negative_examples_for_invariant_synthesis(PosInput, PosOutput, NegInput, NegOutput, Positive, Negative),
469		Positive = [Example|_],
470		maplist(get_varname_from_node_info, Example, VarNames),
471		synthesis_log(involved_variables(VarNames)),
472		pre_library_setup(no, invariant, 1, Example, Library),
473		mark_examples_as_initial(Positive, Negative, InitialPositive, InitialNegative),
474		get_behavioral_constraint_from_input(Library, ([],_), InitialPositive, InitialNegative, BehavioralConstraint, LocationVars),
475		% open('synthesis_constraint_invariant.eval',write,Stream) , tell(Stream) ,
476		% translate:nested_print_bexpr_as_classicalb(BehavioralConstraint) , nl , nl, close(Stream) ,
477		solve_using_selected_solver(BehavioralConstraint, Solution),
478		get_line_amount(_, Library, Example, M),
479		M1 is M-1,
480		length(Example, ParameterAmount),
481		b_get_machinevars_with_operation_params(MachineVars),
482		synthesis_from_examples(null, b(truth,pred,[]), ([],[]), Library, 1, MachineVars, MachineVars, ValidInvariants, invariant, InitialPositive,
483		InitialNegative, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, SynthesizedInvariant, _).
484		% if we synthesize an invariant after finding an invariant violation, we reduce the examples to violating vars only
485		start_specific_synthesis(Operation, invariant, PosInput, NegInput, PosOutput, NegOutput, Synthesized) :-
486		set_preference(randomise_enumeration_order, true),
487		% use PosInput because at least one invariant violating state has been graduated as valid by the user
488		get_violated_and_valid_machine_invariants(PosOutput, ViolatedInvariants, ViolatingVars, ValidInvariants),
489		findall(Name, ( member(IDNode, ViolatingVars),
490		IDNode = b(identifier(Name),_,_)
491		), VarNames),
492		synthesis_log(involved_variables(VarNames)),
493		get_positive_and_negative_examples_for_invariant_synthesis(PosInput, PosOutput, NegInput, NegOutput, Pos, Neg),
494		maplist(reduce_input_to_violating_vars(VarNames), Pos, TRPositive),
495		maplist(reduce_input_to_violating_vars(VarNames), Neg, RNegative),
496		TRPositive = [Example|_],
497		pre_library_setup(no, invariant, 1, Example, Library),
498		get_valid_states(VarNames, 5, TValidStates),
499		maplist(reduce_input_to_violating_vars(VarNames), TValidStates, ValidStates),
500		append(TRPositive, ValidStates, RPositive),
501		remove_dups(RPositive, NRPositive),
502		% TODO: what about several invariant violating examples that are graduated to be valid?
503		% get the example that violates an invariant but has been graduated to be valid by the user
504		get_invariant_violating_example(ViolatedInvariants, PosInput, PosOutput, (In,Out)),
505		% get counter example
506		get_invariant_violating_transition(Operation, ViolatingVars, ViolatedInvariants, In, Out, Counter),
507		start_specific_synthesis_aux(Operation, invariant, ValidInvariants, VarNames, NRPositive, RNegative, ViolatingVars, Library, Counter, Synthesized).
508
509		start_specific_synthesis(Operation, guard, PosInput, NegInput, _, NegOutput, SynthesizedGuard) :-
510		set_preference(randomise_enumeration_order, true),
511		get_guard_list_from_operation(Operation, Guards),
512		get_involved_variables(Guards, PosInput, NegOutput, InvolvedVarNames),
513		% filter partial guards that are valid for the examples, and thus, do not need to be relaxed,
514		% these are conjuncted to the synthesized guard later on
515		findall(ValidGuard, ( member(ValidGuard, Guards),
516		find_identifier_uses(ValidGuard, [], UsedIDs),
517		intersection(UsedIDs, InvolvedVarNames, [])
518		), ValidGuards),
519		mark_examples_as_initial(PosInput, NegInput, InitialPosInput, InitialNegInput),
520		% TODO: handle operation parameters
521		% get_machinevars_by_name(InvolvedVarNames,InvolvedVarNodes) ,
522		% get_valid_transitions_for_operation(InvolvedVarNodes,3,Operation,ValidInput,_) ,
523		% append(InitialPosInput,ValidInput,ExtendedPosInput) ,
524		machine_operation_uses_parameters(Operation, OperationUsesParameters),
525		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, InvolvedVarNames, (ValidGuards,Operation), InitialPosInput, InitialNegInput, Positive, Negative, Library,
526		ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution),
527		synthesis_from_examples(Operation, b(truth,pred,[]), ([],[]), Library, 1, CurrentVars, CurrentVars, ValidGuards, guard, Positive, Negative,
528		BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, SynthesizedGuard, _),
529		synthesis_log(solution(guard,SynthesizedGuard)).
530
531		start_specific_synthesis_aux(Operation, action, NewPosInput, NegInput, NewPosOutput, NegOutput, DistTransitionCache, DistStateCache,
532		CurrentVars, PreCondVars, _, Action) :-
533		% synthesize guard if negative input states are given and synthesis has been suspended
534		NegInput \= [],
535		maplist(get_varname_from_id_node, PreCondVars, PreCondVarNames),
536		DistStateCache = (PosDist,NegDist),
537		append(NewPosInput, PosDist, GuardPositive),
538		append(NegInput, NegDist, GuardNegative),
539		% if neginput empty
540		use_operation_parameters_for_current_synthesis_type(Operation, guard, OperationUsesParameters),
541		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreCondVarNames, ([],_), GuardPositive, GuardNegative, PrePositive, PreNegative,
542		PreLibrary, PreParameterAmount, PreM1, _, PreBehavioralConstraint, PreLocationVars, Solution),
543		synthesis_from_examples(Operation, b(truth,pred,[]), (PrePositive,PreNegative), PreLibrary, 1, PreCondVars, PreCondVars,
544		any, guard, PrePositive, PreNegative, PreBehavioralConstraint, PreLocationVars, PreM1,
545		PreParameterAmount, Solution, Guards, PreDistStateCache),
546		( is_distinguishing(Guards)
547		->
548		Action = Guards
549		; prepare_synthesis_of_action_by_examples(Operation, NewPosInput, NewPosOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint,
550		LocationVars, Solution),
551		prepare_synthesized_guards_for_action(Guards, GuardsForAction),
552		synthesis_from_examples(Operation, DistTransitionCache, PreDistStateCache, Library, 1, CurrentVars, PreCondVars,
553		GuardsForAction, action, NewPosInput, NewPosOutput, BehavioralConstraint, LocationVars,
554		M1, ParameterAmount, Solution, Synthesized, (_,NegDistInput)),
555		!,
556		post_synthesize_action(Operation, CurrentVars, NewPosInput, NewPosOutput, NegInput, NegOutput, NegDistInput, Synthesized, Action)
557		).
558		start_specific_synthesis_aux(Operation, action, NewPosInput, [], NewPosOutput, _, DistTransitionCache, DistStateCache,
559		CurrentVars, PreCondVars, ValidInvariantsOrGuards, Action) :-
560		prepare_synthesis_of_action_by_examples(Operation, NewPosInput, NewPosOutput, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint,
561		LocationVars, Solution),
562		synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, Library, 1, CurrentVars, PreCondVars,
563		ValidInvariantsOrGuards, action, NewPosInput, NewPosOutput, BehavioralConstraint, LocationVars,
564		M1, ParameterAmount, Solution, Synthesized, (_,NegDistInput)),
565		!,
566		post_synthesize_action(Operation, CurrentVars, NewPosInput, NewPosOutput, [], [], NegDistInput, Synthesized, Action).
567
568		% Auxiliary predicate for synthesis of invariants to check if we can find a counter example.
569		start_specific_synthesis_aux(Operation, invariant, ValidInvariants, VarNames, Positive, TNegative, ViolatingVars, Library, (TCounterIn,TCounterOut), SynthesizedInvariant) :-
570		maplist(reduce_input_to_violating_vars(VarNames), [TCounterIn,TCounterOut], [CounterIn,CounterOut]),
571		% don't create contradiction by using the same example as positive and negative
572		findall(Counter, ( member(Counter, [CounterIn,CounterOut]),
573		\+ contains_equivalent_state(Counter, Positive, _)
574		), CounterStates),
575		append(CounterStates, TNegative, Negative),
576		mark_examples_as_initial(Positive, Negative, InitialPositive, InitialNegative),
577		get_behavioral_constraint_from_input(Library, ([],_), InitialPositive, InitialNegative, BehavioralConstraint, LocationVars),
578		solve_using_selected_solver(BehavioralConstraint, Solution),
579		get_line_amount(Operation, Library, CounterIn, M),
580		M1 is M-1,
581		length(CounterIn, ParameterAmount),
582		synthesis_from_examples(Operation, b(truth,pred,[]), ([],[]), Library, 1, ViolatingVars, ViolatingVars, ValidInvariants, invariant, InitialPositive,
583		InitialNegative, BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, SynthesizedInvariant, _),
584		synthesis_log(solution(invariant,SynthesizedInvariant)).
585		% We can't find any invariant violating transition (counter example), therefore we just remove the violating invariants.
586		% no invariant given
587		start_specific_synthesis_aux(_, invariant, [], _, _, _, _, _, _, b(truth,pred,[])) :-
588		synthesis_log(solution(invariant,b(truth,pred,[]))).
589		% print valid invariants
590		start_specific_synthesis_aux(_, invariant, ValidInvariants, _, _, _, _, _, _, Invariant) :-
591		conjunct_predicates(ValidInvariants, Invariant),
592		synthesis_log(solution(invariant,Invariant)).
593
594		get_positive_and_negative_examples_for_invariant_synthesis(PosInput, PosOutput, NegInput, NegOutput, Pos, Neg) :-
595		% for synthesizing invariants we also need output states
596		append(PosInput, PosOutput, TempPositive),
597		append(NegInput, NegOutput, TempNegative),
598		get_distinct_states(invariant, TempPositive, TempNegative, Positive, Negative),
599		% don't use an example more than one time, only possible for invariant synthesis
600		% because we split every transition in two examples (input,output)
601		remove_dups(Positive, Pos),
602		remove_dups(Negative, Neg).
603
604		prepare_synthesis_of_action_by_examples(Operation, Input, Output, Library, ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution) :-
605		!,
606		Input = [Example|_],
607		length(Example, ParameterAmount),
608		pre_library_setup(yes, action, 1, Example, Library),
609		get_current_vars_from_example(Example, CurrentVars),
610		get_behavioral_constraint(Library, ([],_), Input, Output, BehavioralConstraint, LocationVars),
611		% open('synthesis_constraint.eval',write,Stream) , tell(Stream) ,
612		% translate:nested_print_bexpr_as_classicalb(BehavioralConstraint) , nl , nl, close(Stream) ,
613		get_line_amount(Operation, Library, Example, M),
614		M1 is M-1,
615		solve_using_selected_solver(BehavioralConstraint, Solution).
616
617		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, VarNames, (ValidGuards,Operation), TPositive, TNegative, Positive, Negative, Library, ParameterAmount, M1,
618		CurrentVars, BehavioralConstraint, LocationVars, Solution) :-
619		!,
620		remove_dups(TPositive, TTPositive),
621		remove_dups(TNegative, TTNegative),
622		maplist(reduce_input_to_violating_vars(VarNames), TTPositive, TempPositive),
623		maplist(reduce_input_to_violating_vars(VarNames), TTNegative, TempNegative),
624		get_distinct_states(guard, TempPositive, TempNegative, Positive, Negative),
625		% at least one negative example is given since an invariant is violated
626		Negative = [Example|_],
627		length(Example, ParameterAmount),
628		pre_library_setup(OperationUsesParameters, guard, 1, Example, Library),
629		get_current_vars_from_example(Example, CurrentVars),
630		get_behavioral_constraint_from_input(Library, (ValidGuards,Operation), Positive, Negative, BehavioralConstraint, LocationVars),
631		% open('synthesis_constraint.eval',write,Stream) , tell(Stream) ,
632		% unsat_cores:unsat_core(BehavioralConstraint,UC) ,
633		% translate:nested_print_bexpr_as_classicalb(BehavioralConstraint) , nl , nl, close(Stream) ,
634		solve_using_selected_solver(BehavioralConstraint, Solution),
635		get_line_amount(Operation, Library, Example, M),
636		M1 is M-1.
637
638		synthesize_guard_if_necessary(_, _, NegativeInputStates, Synthesized, Synthesized) :-
639		( Synthesized = b(precondition(_,_),subst,_)
640		; NegativeInputStates = []
641		).
642		synthesize_guard_if_necessary(VarNames, PositiveInputStates, NegativeInputStates, SynthesizedBody, Synthesized) :-
643		synthesized_operation_uses_parameters([SynthesizedBody], OperationUsesParameters),
644		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, VarNames, ([],_), PositiveInputStates, NegativeInputStates, Positive, Negative, Library,
645		ParameterAmount, M1, CurrentVars, BehavioralConstraint, LocationVars, Solution),
646		synthesis_from_examples(_, b(truth,pred,[]), ([],[]), Library, 1, CurrentVars, CurrentVars, any, guard, Positive, Negative,
647		BehavioralConstraint, LocationVars, M1, ParameterAmount, Solution, SynthesizedGuard, _),
648		synthesize_guard_if_necessary_aux(PositiveInputStates, NegativeInputStates, CurrentVars, SynthesizedGuard, SynthesizedBody, Synthesized).
649		synthesize_guard_if_necessary_aux(PositiveInputStates, NegativeInputStates, CurrentVars, SynthesizedGuard, SynthesizedBody, SynthesizedGuard) :-
650		% return the distinguishing state derived from synthesizing a guard after synthesizing the action succeeded
651		is_distinguishing(SynthesizedGuard),
652		assert_synthesis_context(b(truth,pred,[]), ([],[]), CurrentVars, CurrentVars, any, guard, PositiveInputStates, NegativeInputStates, SynthesizedBody).
653		synthesize_guard_if_necessary_aux(_, _, _, SynthesizedGuard, SynthesizedBody, Synthesized) :-
654		% synthesizing the guard succeeded
655		\+ is_distinguishing(SynthesizedGuard),
656		SynthesizedGuard \= none,
657		Synthesized = b(precondition(SynthesizedGuard,SynthesizedBody),subst,[]).
658		% synthesizing the guard failed and we only return the synthesized action.
659		synthesize_guard_if_necessary_aux(_, _, _, none, SynthesizedBody, SynthesizedBody).
660
661		%% SYNTHESIS LOOP
662		%% Cache a predicate excluding already visited distinguishing transitions for each new run (see
663		%% get_distinguishing_state_or_trans/8).
664		%% Only for synthesis of an action (ignored otherwise):
665		%% When simultaneously synthesizing a guard to an action we synthesize a new guard each time so that
666		%% we also store each session's distinguishing states.
667		%% The sixth argument PreCondVars defines the variables that should be considered for the simultaneous
668		%% generation of a guard if known. Otherwise, 'PreCondVars = CurrentVars' holds.
669		% search for further solution
670		synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
671		ValidInvariantsOrGuards, Type, PosInput, NegInput, BehavioralConstraint, LocationVars,
672		M1, ParameterAmount, Solution, Synthesized, NewDistStateCache) :-
673		synthesis_log(start_synthesis_loop(DistTransitionCache,DistStateCache,Library,LibExpansion,CurrentVars,PreCondVars,
674		ValidInvariantsOrGuards,Type,PosInput,NegInput,LocationVars,M1,ParameterAmount,Solution)),
675		Solution = solution(SolutionBindings),
676		set_preference(randomise_enumeration_order, true),
677		location_vars_to_program(Library, Type, CurrentVars, LocationVars, M1, ParameterAmount, Solution, UsedLVars1, ProgramAST),
678		% extend the BehavioralConstraint by a constraint excluding specific location mappings that
679		% lead to just swapping equivalent components without changing the semantics
680		get_prevent_component_swap_constraint(UsedLVars1, SolutionBindings, LocationVars, ComponentSwapExclusion),
681		ExtendedBehavioralConstraint = b(conjunct(BehavioralConstraint,ComponentSwapExclusion),pred,[]),
682		% In UsedLVars we have the used location variables from the synthesized solution, so we are able
683		% to exclude those specific bindings when searching for a further solution (otherwise it would
684		% be enough to just change some deadcode).
685		find_further_solution(ProgramAST, LocationVars, UsedLVars1, Solution, ExtendedBehavioralConstraint, FurtherSolution, NewBehavioralConstraint),
686		synthesis_log(defective_further_solution_and_fail(Type,NewBehavioralConstraint,FurtherSolution,Library,CurrentVars,
687		PosInput,NegInput,LocationVars,M1,ParameterAmount)),
688		!,
689		add_distinguishing_states_from_cache(Type, DistStateCache, PosInput, NegInput, NewPosInput, NewPosOutput),
690		synthesis_from_examples_aux1(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
691		ValidInvariantsOrGuards, Type, NewPosInput, NewPosOutput, ExtendedBehavioralConstraint, LocationVars,
692		M1, ParameterAmount, Solution, FurtherSolution, NewBehavioralConstraint, Synthesized, NewDistStateCache).
693		% expand the library if no solution can be found
694		synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, OldLibrary, LibExpansion, CurrentVars, PreCondVars,
695		ValidInvariantsOrGuards, Type, PosInput, NegInput, _, _, M1, ParameterAmount, Solution,
696		Synthesized, NewDistStateCache) :-
697		Solution \= solution(_),
698		NewLibExpansion is LibExpansion+1,
699		PosInput = [Example|_],
700		use_operation_parameters_for_current_synthesis_type(Operation, Type, OperationUsesParameters),
701		pre_library_setup(OperationUsesParameters, Type, NewLibExpansion, Example, NewLibrary),
702		!,
703		% library has changed
704		synthesis_callback(Operation, DistTransitionCache, DistStateCache, OldLibrary, NewLibrary, NewLibExpansion,
705		CurrentVars, PreCondVars, ValidInvariantsOrGuards, M1, ParameterAmount, Type, NewLibrary, PosInput,
706		NegInput, Synthesized, NewDistStateCache).
707
708		% Synthesis failed if library has not changed, i.e., there is no library expansion step left.
709		synthesis_callback(_, _, DistStateCache, _, _, NewLibExpansion, _, _, _, _, _, _, _, _, _, Synthesized, NewDistStateCache) :-
710		% (subtract(NewLibrary,OldLibrary,[]) ;
711		max_library_expansion(MaxLibExpansion),
712		NewLibExpansion > MaxLibExpansion,
713		!,
714		Synthesized = none,
715		NewDistStateCache = DistStateCache.
716		% If an explicit library is asserted in library_from_ui/1 we do not expand the library. If 'default:_' is asserted
717		% we do not expand the library in prolog but use parallelization in Java.
718		synthesis_callback(_, _, DistStateCache, _, _, _, _, _, _, _, _, _, _, _, _, Synthesized, NewDistStateCache) :-
719		on_exception(error(existence_error(_,_),_), library_from_ui(Library), fail),
720		Library \= default,
721		!,
722		Synthesized = none,
723		NewDistStateCache = DistStateCache.
724		% Otherwise, restart synthesis with the expanded library. Either no library is asserted in library_from_ui/1 or
725		% 'default' is asserted and the library gets expanded successively in prolog using a single instance.
726		synthesis_callback(Operation, DistTransitionCache, DistStateCache, _, NewLibrary, NewLibExpansion, CurrentVars, PreCondVars,
727		ValidInvariantsOrGuards, _, ParameterAmount, Type, NewLibrary, PosInput, NegInput, Synthesized, NewDistStateCache) :-
728		synthesis_log(expand_library),
729		get_behavioral_constraint_aux((ValidInvariantsOrGuards,Operation), Type, NewLibrary, PosInput, NegInput, NewBehavioralConstraint, NewLocationVars),
730		solve_using_selected_solver(NewBehavioralConstraint, NewSolution),
731		!,
732		% compute the new amount of lines of the synthesized program using the expanded library
733		PosInput = [Input|_],
734		get_line_amount(Operation, NewLibrary, Input, M),
735		NewM1 is M-1,
736		synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, NewLibrary, NewLibExpansion, CurrentVars, PreCondVars,
737		ValidInvariantsOrGuards, Type, PosInput, NegInput, NewBehavioralConstraint, NewLocationVars,
738		NewM1, ParameterAmount, NewSolution, Synthesized, NewDistStateCache).
739
740		% TODO: search programs for a few further default library configurations --> obsolete if we use neural guided search
741		% done
742		% copy distinguishing state cache
743		synthesis_from_examples_aux1(_, _, DistStateCache, Library, _, CurrentVars, _, ValidInvariantsOrGuards, Type, PosInput, NegInput,
744		_, LocationVars, M1, ParameterAmount, Solution, none, _, Synthesized, NewDistStateCache) :-
745		location_vars_to_program(Library, Type, CurrentVars, LocationVars, M1, ParameterAmount, Solution, _, ProgramAST),
746		replace_preds_by_subst_if_neccessary(Type, ProgramAST, TSolutionAST),
747		% prime_or_unprime_variables_in_ast(unprime,[],TSolutionAST,SolutionAST) ,
748		synthesis_util:expand_state_cache_if_guard_and_solution(Type, Solution, DistStateCache, PosInput, NegInput, NewDistStateCache),
749		conjunct_previous_invariant_or_guard_if_necessary(Type, ValidInvariantsOrGuards, TSolutionAST, Synthesized).
750		% try to find a distinguishing input
751		synthesis_from_examples_aux1(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
752		ValidInvariantsOrGuards, Type, PosInput, NegInput, BehavioralConstraint, LocationVars,
753		M1, ParameterAmount, Solution, FurtherSolution, NewBehavioralConstraint, Synthesized, NewDistStateCache) :-
754		FurtherSolution \= none,
755		location_vars_to_program(Library, Type, CurrentVars, LocationVars, M1, ParameterAmount, Solution, _, ProgramAST),
756		location_vars_to_program(Library, Type, CurrentVars, LocationVars, M1, ParameterAmount, FurtherSolution, _, ProgramAST2),
757		synthesis_log(solution_tuple(ProgramAST,ProgramAST2)),
758		get_distinguishing_state_or_trans(DistTransitionCache, CurrentVars, Type, ValidInvariantsOrGuards,
759		ProgramAST, ProgramAST2, NewDistTransitionCache, Distinguishing),
760		synthesis_from_examples_aux2(Operation, NewDistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
761		ValidInvariantsOrGuards, Type, PosInput, NegInput, BehavioralConstraint, LocationVars,
762		M1, ParameterAmount, Solution, FurtherSolution, NewBehavioralConstraint, Distinguishing, ProgramAST, ProgramAST2,
763		Synthesized, NewDistStateCache).
764
765		% two non equivalent programs
766		synthesis_from_examples_aux2(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
767		ValidInvariantsOrGuards, Type, PosInput, NegInput, BehavioralConstraint, LocationVars, M1, ParameterAmount,
768		Solution, FurtherSolution, NewBehavioralConstraint, solution(Dist), ProgramAST, ProgramAST2, Synthesized, NewDistStateCache) :-
769		synthesis_log(two_non_equivalent_solutions(Type,Solution,FurtherSolution)),
770		synthesis_from_examples_aux3(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
771		ValidInvariantsOrGuards, Type, PosInput, NegInput, BehavioralConstraint, LocationVars, M1,
772		ParameterAmount, Solution, FurtherSolution, NewBehavioralConstraint, Dist, ProgramAST, ProgramAST2,
773		Synthesized, NewDistStateCache).
774		% or we choose the one with a lower term size since we know that both ASTs are equivalent
775		synthesis_from_examples_aux2(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
776		ValidInvariantsOrGuards, Type, PosInput, NegInput, BehavioralConstraint, LocationVars, M1,
777		ParameterAmount, Solution, FurtherSolution, FurtherBehavioralConstraint, Distinguishing, ProgramAST, ProgramAST2,
778		Synthesized, NewDistStateCache) :-
779		Distinguishing \= solution(_),
780		% No distinguishing input, no possible conclusion about examples.
781		% Therefore we pass the "new" behavioral constraint and start synthesis again, we keep the
782		% solution with the smaller term size.
783		synthesis_log(distinguishing_error(Distinguishing,ProgramAST,ProgramAST2)),
784		term_size(ProgramAST, TS1),
785		term_size(ProgramAST2, TS2),
786		( TS1 < TS2
787		->
788		get_new_behavioral_constraint(ProgramAST2, LocationVars, FurtherSolution, BehavioralConstraint, NewBehavioralConstraint),
789		Sol = Solution
790		; NewBehavioralConstraint = FurtherBehavioralConstraint,
791		Sol = FurtherSolution
792		),
793		synthesis_from_examples(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
794		ValidInvariantsOrGuards, Type, PosInput, NegInput, NewBehavioralConstraint, LocationVars, M1,
795		ParameterAmount, Sol, Synthesized, NewDistStateCache).
796
797		% distinguishing transition (actions)
798		synthesis_from_examples_aux3(Operation, DistTransitionCache, DistStateCache, Library, LibExpansion, CurrentVars, PreCondVars,
799		ValidInvariantsOrGuards, action, Input, Output, _, LocationVars, M1, ParameterAmount, Solution, FurtherSolution,
800		_, Distinguishing, ProgramAST, ProgramAST2, Synthesized, NewDistStateCache) :-
801		get_input_output_nodes_from_bindings(Distinguishing, TempDistIn, TempDistOut),
802		DistStateCache = (_,NegativeInputStates),
803		maplist(get_varname_from_id_node, CurrentVars, CurrentVarNames),
804		reduce_input_to_violating_vars(CurrentVarNames, TempDistIn, DistIn),
805		reduce_input_to_violating_vars(CurrentVarNames, TempDistOut, DistOut),
806		( contains_equivalent_state(DistIn, NegativeInputStates, _)
807		->
808		% synthesize guard for the action, the synthesis of the action is suspended for this time,
809		% the distinguishing transition's input is already part of the negative input states provided by the user
810		maplist(get_varname_from_id_node, PreCondVars, PreCondVarNames),
811		DistStateCache = (PosDist,NegDist),
812		append(PosDist, Input, PreInput),
813		append(NegDist, [DistIn], PreOutput),
814		synthesized_operation_uses_parameters([ProgramAST,ProgramAST2], OperationUsesParameters),
815		% TODO: assert context? to decide whether guard needs op params
816		prepare_synthesis_of_guard_by_examples(OperationUsesParameters, PreCondVarNames, (ValidInvariantsOrGuards,Operation), PreInput, PreOutput, PrePositive, PreNegative,
817		PreLibrary, PreParameterAmount, PreM1, _, PreBehavioralConstraint, PreLocationVars, PreSolution),
818		synthesis_from_examples(Operation, b(truth,pred,[]), (PrePositive,PreNegative), PreLibrary, 1, PreCondVars, PreCondVars,
819		any, guard, PrePositive, PreNegative, PreBehavioralConstraint, PreLocationVars, PreM1,
820		PreParameterAmount, PreSolution, Guards, PreDistStateCache),
821		( is_distinguishing(Guards)
822		->
823		Synthesized = Guards,
824		NewDistStateCache = PreDistStateCache,
825		assert_synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, action,
826		Input, Output, _),
827		assert_synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, guard,
828		PrePositive, PreNegative, _)
829		; NewInput = Input,
830		NewOutput = Output,
831		NewLibrary = Library,
832		NewLibExpansion = LibExpansion,
833		get_behavioral_constraint(NewLibrary, (Guards,Operation), NewInput, NewOutput, DistBehavioralConstraint, DistLocationVars),
834		solve_using_selected_solver(DistBehavioralConstraint, DistSolution),
835		synthesis_from_examples(Operation, DistTransitionCache, PreDistStateCache, Library, NewLibExpansion, CurrentVars, PreCondVars,
836		Guards, action, NewInput, NewOutput, DistBehavioralConstraint, DistLocationVars, M1, ParameterAmount,
837		DistSolution, Synthesized, NewDistStateCache)
838		)
839		; % the distinguishing transition's input state is not part of the examples, and thus, we ask the user to validate the transition
840		Synthesized = transition(DistIn,DistOut),
841		NewDistStateCache = DistStateCache,
842		% we assert both temporary solutions, in case of synthesizing a guard afterwards we may need to compute operation parameters
843		location_vars_to_program(Library, action, CurrentVars, LocationVars, M1, ParameterAmount, Solution, _, ProgramAST),
844		location_vars_to_program(Library, action, CurrentVars, LocationVars, M1, ParameterAmount, FurtherSolution, _, ProgramAST2),
845		assert_synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, action,
846		Input, Output, temp([ProgramAST,ProgramAST2]))
847		).
848		% distinguishing state (guards, invariants)
849		synthesis_from_examples_aux3(_, DistTransitionCache, DistStateCache, _, _, CurrentVars, PreCondVars, ValidInvariantsOrGuards, Type,
850		Input, Output, _, _, _, _, _, _, _, Distinguishing, _, _, state(DistIn), DistStateCache) :-
851		Type \= action,
852		% adjust_distinguishing_state_binding(CurrentVars,Distinguishing,CompleteDist) ,
853		get_input_nodes_from_bindings(Distinguishing, TempDistIn),
854		b_get_machinevars_with_operation_params(MachineVars),
855		maplist(get_varname_from_id_node, MachineVars, MachineVarNames),
856		% filter machine vars from a distinguishing state which may refers to machine constants that we are not interested in
857		findall(MachineVarValue, ( member(MachineVarValue, TempDistIn),
858		get_varname_from_node_info(MachineVarValue, MachineVarName),
859		member(MachineVarName, MachineVarNames)
860		), DistIn),
861		assert_synthesis_context(DistTransitionCache, DistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, Type,
862		Input, Output, _).
863		%%
864		use_operation_parameters_for_current_synthesis_type(_, action, yes) :-
865		b_get_machine_set(_),
866		!. % at least one machine set is given
867		use_operation_parameters_for_current_synthesis_type(_, action, no).
868		use_operation_parameters_for_current_synthesis_type(_, invariant, no) :-
869		!.
870		use_operation_parameters_for_current_synthesis_type(OperationName, guard, OperationUsesParameters) :-
871		machine_operation_uses_parameters(OperationName, OperationUsesParameters).
872		use_operation_parameters_for_current_synthesis_type(_, guard, OperationUsesParameters) :-
873		on_exception(error(existence_error(_,_),_), synthesis_context(_, _, _, _, _, guard, _, _, temp(Actions)), fail),
874		synthesized_operation_uses_parameters(Actions, OperationUsesParameters).
875		use_operation_parameters_for_current_synthesis_type(_, guard, OperationUsesParameters) :-
876		on_exception(error(existence_error(_,_),_), synthesis_context(_, _, _, _, _, guard, _, _, Action), fail),
877		synthesized_operation_uses_parameters([Action], OperationUsesParameters).
878		use_operation_parameters_for_current_synthesis_type(_, guard, no).
879
880		% fail if the machine operation does not exist
881		machine_operation_uses_parameters(OperationName, yes) :-
882		b_get_machine_operation(OperationName, _, Params, _),
883		Params \= [],
884		!.
885		machine_operation_uses_parameters(_, no).
886
887		synthesized_operation_uses_parameters([], no).
888		synthesized_operation_uses_parameters([ProgramAST|_], yes) :-
889		find_typed_identifier_uses_with_info(ProgramAST, TypedIdentifiers),
890		member(TypedIdentifier, TypedIdentifiers),
891		get_texpr_info(TypedIdentifier, Info),
892		( member(synthesis(param_single,_), Info)
893		; member(synthesis(param_set,_), Info)
894		),
895		!.
896		synthesized_operation_uses_parameters([_|T], OperationUsesParameters) :-
897		synthesized_operation_uses_parameters(T, OperationUsesParameters).
898
899		assert_synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, Type,
900		Input, Output, Action) :-
901		retractall(synthesis_context(_, _, _, _, _, Type, _, _, _)),
902		asserta(synthesis_context(DistTransitionCache, NewDistStateCache, CurrentVars, PreCondVars, ValidInvariantsOrGuards, Type,
903		Input, Output, Action)).
904
905		is_distinguishing(transition(_,_)).
906		is_distinguishing(state(_)).
907
908		find_further_solution(_, _, _, _, BehavioralConstraint, FurtherSolution, NewBehavioralConstraint) :-
909		synthesis_mode(SynthesisMode),
910		SynthesisMode == first_solution,
911		!,
912		FurtherSolution = none,
913		NewBehavioralConstraint = BehavioralConstraint.
914		find_further_solution(ProgramAST, LocationVars, _, solution(SolutionBindings), BehavioralConstraint, FurtherSolution, NewBehavioralConstraint) :-
915		get_new_behavioral_constraint(ProgramAST, LocationVars, solution(SolutionBindings), BehavioralConstraint, NewBehavioralConstraint),
916		solve_using_selected_solver(NewBehavioralConstraint, TempSolution),
917		find_further_solution_aux(TempSolution, FurtherSolution).
918		find_further_solution_aux(solution(S), Solution) :-
919		!,
920		Solution = solution(S).
921		find_further_solution_aux(_, none).
922
923		% Solve a constraint using the selected solver provided by solver/1.
924		solve_using_selected_solver(Constraint, Solution) :-
925		solver(z3),
926		smt_solve_predicate(z3, Constraint, _, Solution).
927		solve_using_selected_solver(Constraint, Solution) :-
928		\+ solver(z3),
929		solver_interface:solve_predicate(Constraint, _, Solution).
930
931		% no distinguishing example
932		retract_context_if_solution(Distinguishing) :-
933		( Distinguishing = distinguishing(none)
934		; Distinguishing = none
935		),
936		!,
937		retractall(synthesis_context(_, _, _, _, _, _, _, _, _)),
938		retractall(additional_machinevars(_)),
939		asserta(additional_machinevars([])).
940		retract_context_if_solution(_).
941
942		assert_library_configuration_from_ui(Library) :-
943		% either a list of manually selected components from the user or a term default:LibExpansion
944		( is_list(Library)
945		; Library = default:_LibExpansion
946		),
947		retractall(library_from_ui(_)),
948		asserta(library_from_ui(Library)).
949		% default with library expansion in prolog
950		assert_library_configuration_from_ui(_).
951
952		% Empty list of var names means we do not consider if-statements at all.
953		assert_if_statement_var_names([]).
954		assert_if_statement_var_names(ConsiderIfVarNames) :-
955		asserta(consider_if_var_names(ConsiderIfVarNames)).
956
957		pre_library_setup(UseOperationParameters, Type, _, Example, Library) :-
958		% either a specific default library is asserted (like default:1) or an explicit set of library
959		% components selected by the user
960		library_from_ui(LibraryFromUi),
961		!,
962		get_asserted_if_statement_vars(ConsiderIfVarNames),
963		get_asserted_constant_configuration(NotConsiderConstants),
964		get_all_machine_sets(MachineSets),
965		library_setup(UseOperationParameters, MachineSets, ConsiderIfVarNames, NotConsiderConstants, LibraryFromUi, Type, Example, Library).
966		pre_library_setup(UseOperationParameters, Type, LibExpansion, Example, Library) :-
967		get_asserted_if_statement_vars(ConsiderIfVarNames),
968		get_asserted_constant_configuration(NotConsiderConstants),
969		get_all_machine_sets(MachineSets),
970		% default if no library is asserted, gets expanded in prolog using synthesis_callback/16
971		library_setup(UseOperationParameters, MachineSets, ConsiderIfVarNames, NotConsiderConstants, default:LibExpansion, Type, Example, Library).
972
973		get_all_machine_sets(MachineSets) :-
974		findall(MachineSet, b_get_machine_set(_, MachineSet), MachineSets).
975
976		get_asserted_constant_configuration(NotConsiderConstants) :-
977		not_consider_constants(NotConsiderConstants),
978		!.
979		get_asserted_constant_configuration(no).
980
981		get_asserted_if_statement_vars(ConsiderIfVarNames) :-
982		consider_if_var_names(ConsiderIfVarNames),
983		!.
984		get_asserted_if_statement_vars([]).
985
986		reset_synthesis_context :-
987		retractall(synthesis_context(_, _, _, _, _, _, _, _, _)),
988		retractall(additional_machinevars(_)),
989		asserta(additional_machinevars([])).
990
991		cache_operation_tuple_to_quadruple((_,b(operation(b(identifier(op(OperationName)),_,_),Res,Par,Body),_,_)), (OperationName,Res,Par,Body)).
992
993		get_distinguishing_state_cache_from_operation_tuples(Operations, OperationName, (CachePos,CacheNeg), Operation) :-
994		member(((CachePos,CacheNeg),Operation), Operations),
995		Operation = b(operation(b(identifier(op(OperationName)),_,_),_,_,_),_,_).