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