1		% (c) 2018-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(synthesis_util, [get_distinguishing_state_or_trans/8,
6		get_valid_transitions_for_operation/5,
7		get_invariant_violating_transition/6,
8		get_valid_and_invalid_equality_predicates_for_operation/6,
9		get_distinct_states/5,
10		get_valid_and_invalid_equality_predicates_for_invariants/4,
11		get_violated_and_valid_machine_invariants/4,
12		get_invariant_violating_example/4,
13		get_involved_variables/4,
14		get_invariant_violating_vars_from_examples/3,
15		get_single_constant_or_set_operator_id/3,
16		get_input_output_nodes_from_bindings/3,
17		get_output_nodes_from_bindings/2,
18		get_location_var_node_by_info_term/3,
19		get_location_var_node_by_name/3,
20		get_var_node_by_info_term/3,
21		get_operation_params_from_ids/2,
22		set_operation_params_domain/2,
23		get_guard_list_from_operation/2,
24		get_current_vars_from_example/2,
25		get_input_nodes_from_bindings/2,
26		get_varname_from_node_info/2,
27		get_varname_from_id_node/2,
28		get_valid_states/3,
29		get_machinevars_by_name/2,
30		get_precondition_from_operation_body/2,
31		get_binding_for_name_or_value/3,
32		get_valid_inputs_for_operation/3,
33		b_get_typing_predicate_for_vars/2,
34		b_get_typed_invariant_from_machine/1,
35		b_compute_expression_nowf_no_bindings/2,
36		expand_state_cache_if_guard_and_solution/6,
37		add_distinguishing_states_from_cache/6,
38		conjunct_previous_invariant_or_guard_if_necessary/4,
39		check_transitions_against_machine_operations/4,
40		check_transition_against_machine_operations/5,
41		check_negative_inputs_against_operation_precondition/2,
42		replace_preds_by_subst_if_neccessary/3,
43		replace_precondition_of_operation/3,
44		contains_equivalent_state/3,
45		find_typed_identifier_uses_with_info/2,
46		delete_numbers_from_atom/2,
47		create_equality_nodes_from_example/2,
48		adapt_machine_code_for_operations/2,
49		% b_synthesis
50		b_get_machinevars_with_operation_params/1,
51		remove_prime/2,
52		parallel_to_conjunction/2,
53		prime_or_unprime_variables_in_ast/4,
54		parse_and_typecheck_value/2,
55		keep_asserted_initial_examples/6,
56		prepare_solution/6,
57		finalize_synthesized_action/3,
58		split_input_output_tuples/3,
59		prepare_synthesized_guards_for_action/2,
60		%
61		mark_examples_as_initial/4,
62		reduce_input_to_violating_vars/3,
63		is_ast/1,
64		zip/3,
65		set_type_if_necessary/2]).
66
67		:- use_module(synthesis(logging)).
68
69		:- use_module(probsrc(bsyntaxtree)).
70		:- use_module(probsrc(error_manager), [add_error/3]).
71		:- use_module(probsrc(b_interpreter), [b_test_boolean_expression_cs/5,b_compute_expression_nowf/6]).
72		:- use_module(probsrc(solver_interface), [solve_predicate/3, solve_predicate/5]).
73		:- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate/4]).
74		:- use_module(probsrc(btypechecker), [prime_identifier/2,is_primed_id/1,btype/7]).
75		:- use_module(probsrc(bmachine)).
76		:- use_module(extrasrc(before_after_predicates),
77		[before_after_predicate_with_equalities/3,before_after_predicate_for_operation/2]).
78		:- use_module(probsrc(parsercall), [parse/3]).
79		:- use_module(probsrc(translate), [translate_bexpression/2,
80		translate_bexpression_to_codes/2,
81		translate_subst_or_bexpr/2,
82		translate_machine/3,
83		generate_typing_predicates/2]).
84
85		:- use_module(library(lists)).
86		:- use_module(library(sets), [subtract/3,intersection/3]).
87
88		:- use_module(extension('plspec/plspec/plspec_core')).
89
90		:- set_prolog_flag(double_quotes, codes).
91
92		b_get_machinevars_with_operation_params(MachineVarsWithParams) :-
93		b_get_machine_variables(MachineVars),
94		b_get_machinevars_with_operation_params_aux(MachineVars, MachineVarsWithParams).
95		b_get_machinevars_with_operation_params_aux(MachineVars, MachineVarsWithParams) :-
96		% TODO: fix this spider warning, do not access dynamic additional_machinevars/1 in this module
97		catch(b_synthesis:additional_machinevars(AdditionalMachineVars), error(existence_error(_,_),_), fail),
98		!,
99		append(MachineVars, AdditionalMachineVars, MachineVarsWithParams).
100		b_get_machinevars_with_operation_params_aux(MachineVars, MachineVars).
101
102		parse_and_typecheck_value(Value, ValueAst) :-
103		atom_codes(Value, L),
104		parse(expression, L, Parsed),
105		btype(bsynthesis, Parsed, openenv(_,env_empty), _, TempAst, tr(_,_,_,_), tr(_,_,_,_)),
106		set_type_if_necessary(TempAst, ValueAst).
107
108		get_machinevars_by_name(VarNames, CurrentVars) :-
109		b_get_machinevars_with_operation_params(MachineVarsWithParams),
110		get_machinevars_by_name_aux(VarNames, MachineVarsWithParams, [], CurrentVars).
111		get_machinevars_by_name_aux([], _, Acc, Acc).
112		get_machinevars_by_name_aux([VarName|T], MachineVars, Acc, CurrentVars) :-
113		member(b(identifier(VarName),Type,Info), MachineVars),
114		!,
115		get_machinevars_by_name_aux(T, MachineVars, [b(identifier(VarName),Type,Info)|Acc], CurrentVars).
116		get_machinevars_by_name_aux([VarName|_], _, _, _) :-
117		add_error(get_machinevars_by_name, 'This is not a machine variable: ',[VarName]),
118		!,
119		fail.
120
121		% True if the given set of states contains an equivalent state.
122		contains_equivalent_state(State, States, EquivalentState) :-
123		length(State, VarAmount),
124		contains_equivalent_state(VarAmount, State, States, EquivalentState).
125		contains_equivalent_state(_, _, [], _) :-
126		!,
127		fail.
128		contains_equivalent_state(VarAmount, State, [ExampleState|_], EquivalentState) :-
129		length(ExampleState, ExampleVarAmount),
130		VarAmount = ExampleVarAmount,
131		create_equality_nodes_from_example(State, StateEqualityNodes),
132		create_equality_nodes_from_example(ExampleState, ExampleStateEqualityNodes),
133		get_distinct_independent_types_constraint_for_enums(DistinctEnumSetsConstraint),
134		( DistinctEnumSetsConstraint == b(truth,pred,[])
135		->
136		append([StateEqualityNodes,ExampleStateEqualityNodes], EqualityNodes)
137		; append([DistinctEnumSetsConstraint,StateEqualityNodes,ExampleStateEqualityNodes], EqualityNodes)
138		),
139		conjunct_predicates(EqualityNodes, Equality),
140		solve_predicate(Equality, _, Solution),
141		Solution = solution(_),
142		!,
143		EquivalentState = ExampleState.
144		contains_equivalent_state(VarAmount, State, [_|T], EquivalentState) :-
145		contains_equivalent_state(VarAmount, State, T, EquivalentState).
146
147		get_distinct_independent_types_constraint_for_enums(Constraint) :-
148		findall(MachineSetName, b_get_machine_set(MachineSetName), MachineSetNames),
149		get_distinct_independent_types_constraint_for_enums(MachineSetNames, [], ConstraintList),
150		conjunct_predicates(ConstraintList, Constraint).
151
152		get_distinct_independent_types_constraint_for_enums([], Acc, Acc).
153		get_distinct_independent_types_constraint_for_enums([MachineSetName|T], Acc, ConstraintList) :-
154		b_get_named_machine_set(MachineSetName, SetValues),
155		findall(SetValueNode, ( member(SetValue, SetValues),
156		SetValueNode = b(identifier(SetValue),global(MachineSetName),[])
157		), SetValueNodes),
158		findall(Inequality, ( member(Node1, SetValueNodes),
159		member(Node2, SetValueNodes),
160		Node1 \= Node2,
161		Inequality = b(not_equal(Node1,Node2),pred,[])
162		), Inequalities),
163		get_distinct_independent_types_constraint_for_enums(T, [Inequalities|Acc], ConstraintList).
164
165		% seq(_), string_set, integer_set, bool_set,..
166		% Also needed in location_vars_to_program.
167		get_single_constant_or_set_operator_id(seq-Type, Out, b(seq(Set),set(seq(NodeType)),[])) :-
168		get_single_constant_or_set_operator_id(Type, _, Set),
169		Set = b(_,TInnerType,_),
170		TInnerType =.. [_|InnerType],
171		NodeType =.. InnerType,
172		unique_typed_id("o", set(seq(NodeType)), TempOut),
173		% we add the internal type of infinite set constants here
174		% so we are able to call this predicate when converting location variables to ASTs later on
175		add_texpr_infos(TempOut, [synthesis(type,seq-Type)], Out).
176		get_single_constant_or_set_operator_id(constant-Type, Out, ConstantNode) :-
177		get_constant_node_or_id(constant-Type, ConstantNode),
178		unique_typed_id("o", Type, TempOut),
179		add_texpr_infos(TempOut, [synthesis(type,Type)], Out).
180
181		get_constant_node_or_id(string_set, b(string_set,set(string),[])).
182		get_constant_node_or_id(bool_set, b(bool_set,set(boolean),[])).
183		get_constant_node_or_id(integer_set, b(integer_set('INTEGER'),set(integer),[])).
184		get_constant_node_or_id(integer_set_min_max, b(integer_set('INT'),set(integer),[])).
185		get_constant_node_or_id(natural1, b(integer_set('NATURAL1'),set(integer),[])).
186		get_constant_node_or_id(natural, b(integer_set('NATURAL'),set(integer),[])).
187		get_constant_node_or_id(implementable_natural1, b(integer_set('NAT1'),set(integer),[])).
188		get_constant_node_or_id(implementable_natural, b(integer_set('NAT'),set(integer),[])).
189		get_constant_node_or_id(constant-Type, Constant) :-
190		unique_typed_id("constant", Type, TempConstant),
191		add_texpr_infos(TempConstant, [synthesis(enumerated_constant),synthesis(type,Type)], Constant).
192
193		add_distinguishing_states_from_cache(action, _, PosInput, NegInput, PosInput, NegInput) :-
194		!.
195		add_distinguishing_states_from_cache(_, (DistIn,DistOut), PosInput, NegInput, NewPosInput, NewNegInput) :-
196		append(DistIn, PosInput, TempPosInput),
197		append(DistOut, NegInput, TempNegInput),
198		remove_dups(TempPosInput, NewPosInput),
199		remove_dups(TempNegInput, NewNegInput).
200
201		b_test_boolean_expression_wf_no_bindings(BooleanExpr, Result) :-
202		find_identifier_uses(BooleanExpr, [], UsedIdNames),
203		findall(bind(UsedIdName,_), member(UsedIdName, UsedIdNames), Bindings),
204		b_test_boolean_expression_cs(BooleanExpr, Bindings, Result,'synthesis',0).
205
206		b_compute_expression_nowf_no_bindings(Expression, Result) :-
207		find_identifier_uses(Expression, [], UsedIdNames),
208		findall(bind(UsedIdName,_), member(UsedIdName, UsedIdNames), Bindings),
209		b_compute_expression_nowf(Expression, [], Bindings, Result,'synthesis',0).
210
211		% If the domain is enumerated from 1 to n we suppose set(couple(integer,_)) is a sequence.
212		is_seq(b(Node,Type,Info)) :-
213		( Type = set(couple(integer,_))
214		; Type = seq(_)
215		),
216		b_test_boolean_expression_wf_no_bindings(b(equal(b(domain(b(Node,Type,Info)),set(integer),[]),
217		b(interval(b(integer(1),integer,[]),
218		b(size(b(Node,Type,Info)),integer,[])),set(integer),[])),pred,[]), []).
219
220		get_distinguishing_state_or_trans(DistTransitionCache, CurrentVars, Type, ValidInvariantsOrGuards, AST1,
221		AST2, NewDistTransitionCache, Distinguishing) :-
222		% add typing of machine variables to the invariant for consistency with AtelierB and to find a solution referring to
223		% all machine variables
224		b_get_typed_invariant_from_machine(TypedInvariant),
225		% add WD-constraints for sequences
226		find_typed_identifier_uses(AST1, AST1Nodes),
227		find_typed_identifier_uses(AST2, AST2Nodes),
228		findall(Seq, ( member(Seq, AST1Nodes),
229		is_seq(Seq)
230		), Seq1),
231		findall(Seq, ( member(Seq, AST2Nodes),
232		is_seq(Seq)
233		), Seq2),
234		append(Seq1, Seq2, TSequences),
235		remove_dups(TSequences, Sequences),
236		maplist(sequence_well_definedness_constraint, Sequences, SeqConstraintList),
237		conjunct_predicates(SeqConstraintList, SeqConstraints),
238		get_distinct_independent_types_constraint_for_enums(DistinctEnumSetsConstraint),
239		preferences:set_preference(randomise_enumeration_order, true),
240		get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, DistTransitionCache, Type, ValidInvariantsOrGuards,
241		b(conjunct(SeqConstraints,b(conjunct(b(negation(
242		b(equivalence(AST1,AST2),pred,[])),pred,[]),TypedInvariant),pred,[])),pred,[]), Distinguishing),
243		expand_transition_cache_if_solution(Type, DistTransitionCache, CurrentVars, Distinguishing, NewDistTransitionCache),
244		synthesis_log(distinguishing_transition_cache_changed(DistTransitionCache,NewDistTransitionCache)).
245		% When synthesizing an action only search for a distinguishing transition that doesn't violate the
246		% so far synthesized guard (in case there is one).
247		% Furthermore, we exclude already visited distinguishing transitions using the cache in order to
248		% prevent cycles when a distinguishing transition's output is changed by the user
249		% (otherwise we would find the same transition over and over again because the one with an adapted
250		% output is added to the examples).
251		get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, DistTransitionCache, action, ValidInvariantsOrGuards, Constraint, Distinguishing) :-
252		ValidInvariantsOrGuards \= any,
253		ValidInvariantsOrGuards \= none,
254		!,
255		DistConstraint = b(conjunct(DistinctEnumSetsConstraint,b(conjunct(b(conjunct(Constraint,ValidInvariantsOrGuards),pred,[]),DistTransitionCache),pred,[])),pred,[]),
256		synthesis_log(distinguishing_constraint(action,DistConstraint)),
257		solve_distinguishing_constraint_with_fallback(DistConstraint, TDistinguishing),
258		get_solution_or_none(TDistinguishing, Distinguishing).
259		get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, DistTransitionCache, action, _, Constraint, Distinguishing) :-
260		!,
261		DistConstraint = b(conjunct(DistinctEnumSetsConstraint,b(conjunct(Constraint,DistTransitionCache),pred,[])),pred,[]),
262		synthesis_log(distinguishing_constraint(action,Constraint)),
263		solve_distinguishing_constraint_with_fallback(DistConstraint, TDistinguishing),
264		get_solution_or_none(TDistinguishing, Distinguishing).
265		% DistTransitionCache is empty when synthesizing guard/invariant
266		get_distinguishing_state_or_trans_aux(DistinctEnumSetsConstraint, _, Type, _, Constraint, Distinguishing) :-
267		synthesis_log(distinguishing_constraint(Type,Constraint)),
268		solve_distinguishing_constraint_with_fallback(b(conjunct(DistinctEnumSetsConstraint,Constraint),pred,[]), TDistinguishing),
269		get_solution_or_none(TDistinguishing, Distinguishing).
270
271		% Solving the distinguishing constraint maybe causes an integer overflow due to infinite domains which
272		% possibly ends in not finding any solution, i.e., neither true nor false.
273		% Therefore, we try different solvers if no solution can be found.
274		% Of course, we do not want to enumerate infinite domains, but there is no reasonable domain restriction
275		% if for instance the invariant defines a variable to be an element of INTEGER without an upper bound.
276		% The distinguishing constraint is of the form "not(P1 <=> P2) & I", whereat P1,P2 are two synthesized
277		% programs and I is the current machine invariant. When synthesizing a substitution with already known
278		% guards G the constraint results to "not(P1 <=> P2) & I & G".
279		solve_distinguishing_constraint_with_fallback(DistConstraint, Solution) :-
280		solve_predicate(DistConstraint, _, ProBSolution),
281		% ProB either found a solution or a contradiction
282		synthesis_log(solve_distinguishing_constraint(DistConstraint,'ProB')),
283		ProBSolution \= no_solution_found(_),
284		!,
285		Solution = ProBSolution.
286		solve_distinguishing_constraint_with_fallback(DistConstraint, Z3Solution) :-
287		% ProB could not make a decision and answered no_solution_found/1, then we ask z3
288		synthesis_log(solve_distinguishing_constraint(DistConstraint,'Z3')),
289		smt_solve_predicate(z3, DistConstraint, _, Z3Solution).
290		% Solution \= no_solution_found(_) , ! , Solution = Z3Solution.
291		%%%%% Maybe too much overhead to ask a third solver for the distinguishing constraint since two solvers were already not able to find a solution.
292		% solve_distinguishing_constraint_with_fallback(DistConstraint,ProBZ3Solution) :-
293		% synthesis_log(solve_distinguishing_constraint(DistConstraint,'Combined ProB and Z3')) ,
294		% preferences:set_preference(smt_supported_interpreter,true) ,
295		% Z3 also did not find a solution, then we ask ProB/Z3 combined as a last try
296		% solve_predicate(DistConstraint,_,ProBZ3Solution) ,
297		% preferences:set_preference(smt_supported_interpreter,false).
298		get_solution_or_none(solution(Solution), solution(Solution)).
299		get_solution_or_none(Solution, none) :-
300		Solution \= solution(_).
301
302		b_get_typed_invariant_from_machine(TypedInvariant) :-
303		b_get_typing_predicate(TypingPredicate),
304		b_get_invariant_from_machine(Invariant),
305		conjunct_predicates([TypingPredicate,Invariant], TypedInvariant).
306
307		% Return typing predicate for the machine variables.
308		b_get_typing_predicate(TypingPredicate) :-
309		b_get_machinevars_with_operation_params(MachineVars),
310		findall(NonSeq, ( member(NonSeq, MachineVars),
311		NonSeq \= b(_,seq(_),_)
312		), NonSeqMachineVars),
313		b_get_typing_predicate_for_vars(NonSeqMachineVars, TypingPredicate).
314
315		% Return typing predicate for specific machine variables.
316		b_get_typing_predicate_for_vars(CurrentVars, TypingPredicate) :-
317		generate_typing_predicates(CurrentVars, TypingPredicatesList),
318		conjunct_predicates(TypingPredicatesList, TypingPredicate).
319
320		:- spec_pre(expand_transition_cache_if_solution/5, [atom,ast,list(ast),one_of([atom,solution_compound]),var]).
321		:- spec_invariant(expand_transition_cache_if_solution/5, [atom,ast,list(ast),one_of([atom,solution_compound]),ast]).
322		:- spec_post(expand_transition_cache_if_solution/5, [atom,ast,list(ast),one_of([atom,solution_compound]),var],
323		[atom,ast,list(ast),one_of([atom,solution_compound]),ast]).
324		expand_transition_cache_if_solution(action, DistTransitionCache, CurrentVars, solution(Solution), NewDistTransitionCache) :-
325		!,
326		get_input_output_nodes_from_bindings(Solution, Input, Output),
327		exclude_transition_constraint(Input, Output, CurrentVars, Exclusion),
328		NewDistTransitionCache = b(conjunct(DistTransitionCache,Exclusion),pred,[]).
329		expand_transition_cache_if_solution(action, DistTransitionCache, _, _, DistTransitionCache).
330		expand_transition_cache_if_solution(Type, DistTransitionCache, _, _, DistTransitionCache) :-
331		Type \= action.
332
333		:- spec_pre(expand_state_cache_if_guard_and_solution/6, [atom,solution_compound,pair(ast_examples,ast_examples),
334		ast_examples,ast_examples,var]).
335		:- spec_invariant(expand_state_cache_if_guard_and_solution/6, [atom,solution_compound,pair(ast_examples,ast_examples),
336		ast_examples,ast_examples,pair(ast_examples,ast_examples)]).
337		:- spec_post(expand_state_cache_if_guard_and_solution/6, [atom,solution_compound,pair(ast_examples,ast_examples),
338		ast_examples,ast_examples,var],
339		[atom,solution_compound,pair(ast_examples,ast_examples),
340		ast_examples,ast_examples,pair(ast_examples,ast_examples)]).
341		expand_state_cache_if_guard_and_solution(guard, solution(_), (UsedPositives,UsedNegatives), PosInput,
342		NegInput, (PositiveStates,NegativeStates)) :-
343		append(UsedPositives, PosInput, TPositiveStates),
344		append(UsedNegatives, NegInput, TNegativeStates),
345		remove_dups(TPositiveStates, PositiveStates),
346		remove_dups(TNegativeStates, NegativeStates).
347		expand_state_cache_if_guard_and_solution(_, _, DistStateCache, _, _, DistStateCache).
348
349		:- spec_pre(exclude_transition_constraint/4, [list(ast),list(ast),list(ast),var]).
350		:- spec_invariant(exclude_transition_constraint/4, [list(ast),list(ast),list(ast),ast]).
351		:- spec_post(exclude_transition_constraint/4, [list(ast),list(ast),list(ast),var],
352		[list(ast),list(ast),list(ast),ast]).
353		exclude_transition_constraint(Input, Output, CurrentVars, b(negation(EqualityConjunction),pred,[])) :-
354		b_get_machinevars_with_operation_params(MachineVars),
355		maplist(get_varname_from_id_node, CurrentVars, CurrentIDs),
356		create_equality_nodes_from_examples(CurrentIDs, Input, Output, MachineVars, EqualityNodes),
357		conjunct_predicates(EqualityNodes, EqualityConjunction).
358
359		sequence_well_definedness_constraint(SeqIDNode, WDConstraint) :-
360		% well-defined sequence: domain enumerated from 1..n
361		WDConstraint = b(equal(b(domain(SeqIDNode),set(integer),[]),
362		b(interval(b(integer(1),integer,[]),b(size(SeqIDNode),integer,[])),set(integer),[])),pred,[]).
363
364		is_ast(b(_,_,_)).
365
366		delete_numbers_from_atom(NumberAtom, Atom) :-
367		atom_codes(NumberAtom, Codes),
368		delete_numbers_from_codelist(Codes, NewCodes),
369		atom_codes(Atom, NewCodes).
370		delete_numbers_from_codelist([], []).
371		delete_numbers_from_codelist([Code|R], [Code|NR]) :-
372		( Code > 57
373		; Code < 48
374		),
375		!,
376		delete_numbers_from_codelist(R, NR).
377		delete_numbers_from_codelist([_|R], NR) :-
378		delete_numbers_from_codelist(R, NR).
379
380		% Returns a list of all guards or 'any' if none is given.
381		:- spec_pre(get_guard_list_from_operation/2, [atom,var]).
382		:- spec_invariant(get_guard_list_from_operation/2, [atom,one_of([ast,atom])]).
383		:- spec_post(get_guard_list_from_operation/2, [atom,var], [atom,one_of([ast,atom])]).
384		get_guard_list_from_operation(Operation, ListOfGuards) :-
385		b_get_machine_operation(Operation, _, OperationParameters, OpBody),
386		get_guard_list_from_operation_aux(Operation, OpBody, GuardList),
387		recreate_guards_for_operation_parameters(OperationParameters, OperationParameterGuards),
388		append(GuardList, OperationParameterGuards, ListOfGuards).
389		% No given guards.
390		get_guard_list_from_operation(_, any).
391
392		get_guard_list_from_operation_aux(Operation, OpBody, GuardList) :-
393		get_guard_list_from_operation_aux2(Operation, OpBody, Guard),
394		conjunction_to_list(Guard, GuardList).
395		get_guard_list_from_operation_aux(_, _, []).
396
397		get_guard_list_from_operation_aux2(_, b(precondition(Guard,_),_,_), Guard).
398		get_guard_list_from_operation_aux2(Operation, b(rlevent(Operation,_,_,_,Guard,_,_,_,_,_,_),_,_), Guard).
399		get_guard_list_from_operation_aux2(_, b(any(_,Guard,_),subst,_), Guard).
400
401		% ProB removes typing guards for operations parameters which we need for synthesis to create constants for operation parameters
402		recreate_guards_for_operation_parameters(OperationParameters, OperationParameterGuards) :-
403		findall(SetAst, b_get_machine_set(_, SetAst), IndependentTypes),
404		recreate_guards_for_operation_parameters(OperationParameters, IndependentTypes, [], OperationParameterGuards).
405		recreate_guards_for_operation_parameters([], _, Acc, Acc).
406		recreate_guards_for_operation_parameters([OperationParameter|T], IndependentTypes, Acc, OperationParameterGuards) :-
407		get_texpr_type(OperationParameter, Type),
408		member(b(SetName,set(Type),Info), IndependentTypes),
409		Membership = b(member(OperationParameter,b(SetName,set(Type),Info)),pred,[]),
410		recreate_guards_for_operation_parameters(T, IndependentTypes, [Membership|Acc], OperationParameterGuards).
411
412		:- spec_pre(conjunct_previous_invariant_or_guard_if_necessary/4, [atom,one_of([atom,ast,list(ast)]),ast,var]).
413		:- spec_invariant(conjunct_previous_invariant_or_guard_if_necessary/4, [atom,one_of([atom,ast,list(ast)]),ast,ast]).
414		:- spec_post(conjunct_previous_invariant_or_guard_if_necessary/4, [atom,one_of([atom,ast,list(ast)]),ast,var],
415		[atom,one_of([atom,ast,list(ast)]),ast,ast]).
416		conjunct_previous_invariant_or_guard_if_necessary(invariant, ValidInvariants, ProgramAST, SolutionAST) :-
417		!,
418		% mark synthesized invariants in the info to be able to split synthesized invariants from those that have already been valid beforehand
419		% we want to avoid redundancy when generating typing invariants later on
420		conjunction_to_list(ProgramAST, ProgramASTList),
421		findall(MarkedConjunct, ( member(Conjunct, ProgramASTList),
422		add_texpr_infos(Conjunct, [synthesized_code], MarkedConjunct)
423		), MarkedConjunctList),
424		conjunct_predicates(MarkedConjunctList, MarkedProgramAst),
425		append(ValidInvariants, [MarkedProgramAst], InvariantsList), % ValidInvariants prior to synthesized ones since they may contain typing invariants
426		conjunct_predicates(InvariantsList, SolutionAST).
427		conjunct_previous_invariant_or_guard_if_necessary(guard, Guards, ProgramAST, SolutionAST) :-
428		Guards \= any,
429		!,
430		% search for valid guards that are already given by the machine ( NewPreCond => OldPreCond )
431		find_typed_identifier_uses(ProgramAST, [], ProgIDs),
432		findall(Pre, ( member(Pre, Guards),
433		find_typed_identifier_uses(Pre, PreIDs),
434		append(ProgIDs, PreIDs, TIDs),
435		remove_dups(TIDs, IDs),
436		b_test_boolean_expression_wf_no_bindings(b(forall(IDs,ProgramAST,Pre),pred,[used_ids([])]), [])
437		), InvalidPreConds),
438		sets:subtract(Guards, InvalidPreConds, ValidPreConds),
439		append(ValidPreConds, [ProgramAST], PreCondsList), % ValidPreConds prior to synthesized ones since they may contain predicates setting the type of operation parameters
440		conjunct_predicates(PreCondsList, SolutionAST).
441		conjunct_previous_invariant_or_guard_if_necessary(action, Guard, ProgramAST, SolutionAST) :-
442		\+ member(Guard, [any,none]),
443		!,
444		SolutionAST = b(precondition(Guard,ProgramAST),subst,[]).
445		conjunct_previous_invariant_or_guard_if_necessary(_, _, ProgramAST, ProgramAST).
446
447		% Replace equal by assign_single_id and conjunctions by parallel substitution.
448		:- spec_pre(replace_preds_by_subst_if_neccessary/3, [atom,ast,var]).
449		:- spec_invariant(replace_preds_by_subst_if_neccessary/3, [atom,ast,ast]).
450		:- spec_post(replace_preds_by_subst_if_neccessary/3, [atom,ast,var], [atom,ast,ast]).
451		replace_preds_by_subst_if_neccessary(action, TSolutionAST, SolutionAST) :-
452		conjunction_to_list(TSolutionAST, EqualityList),
453		maplist(equality_to_assignment, EqualityList, AssignmentList),
454		SolutionAST = b(parallel(AssignmentList),subst,[]).
455		replace_preds_by_subst_if_neccessary(_, SolutionAST, SolutionAST).
456
457		equality_to_assignment(b(equal(Primed,Assignment),pred,Info), b(assign_single_id(Primed,Assignment),subst,Info)).
458
459		% Replace parallel substitution by conjunction predicates and assignments by equalities.
460		:- spec_pre(parallel_to_conjunction/2, [ast,var]).
461		:- spec_invariant(parallel_to_conjunction/2, [ast,ast]).
462		:- spec_post(parallel_to_conjunction/2, [ast,var], [ast,ast]).
463		parallel_to_conjunction(b(Node,Type,Info), b(Node,Type,Info)) :-
464		ground(Node),
465		Type \= subst.
466		parallel_to_conjunction(b(Node,subst,_), Conjunction) :-
467		ground(Node),
468		Node = parallel(Assignments),
469		findall(Equality, ( member(Assignment, Assignments),
470		equality_to_assignment(Equality, Assignment)
471		), EqualityNodes),
472		conjunct_predicates(EqualityNodes, Conjunction).
473		%%
474		% Get the variables involved in an invariant violation if currently all machine variables are considered,
475		% i.e., they have not been reduced by now.
476		get_involved_variables(_, PosInput, _, VarNames) :-
477		examples_already_reduced(PosInput),
478		!,
479		PosInput = [Example|_],
480		% the examples already have been reduced by the user
481		maplist(get_varname_from_node_info, Example, VarNames).
482		get_involved_variables(Guards, PosInput, NegInput, VarNames) :-
483		get_involved_variables_aux(Guards, PosInput, NegInput, TempVarNames),
484		remove_dups(TempVarNames, VarNames),
485		% only consider machine variables
486		% b_get_machinevars_with_operation_params(MachineVars) ,
487		% maplist(get_varname_from_id_node,MachineVars,MachineVarNames) ,
488		% sets:intersection(VarNamesNoDups,MachineVarNames,VarNames) ,
489		synthesis_log(involved_variables(VarNames)).
490		% check the invariants first
491		get_involved_variables_aux(_, _, NegInput, VarNames) :-
492		get_violated_and_valid_machine_invariants(NegInput, _, ViolatingVars, _),
493		ViolatingVars \= [],
494		!,
495		findall(Name, member(b(identifier(Name),_,_), ViolatingVars), VarNames).
496		% if no invariant violating vars, check the guards
497		get_involved_variables_aux(Guards, PosInput, NegInput, VarNames) :-
498		Guards \= [],
499		append(PosInput, NegInput, Input),
500		check_states_on_guards(Input, Guards, ViolatedGuards),
501		findall(UsedIDs, ( member(Guard, ViolatedGuards),
502		find_identifier_uses(Guard, [], UsedIDs)
503		), NestedList),
504		append(NestedList, UsedIDs),
505		UsedIDs \= [],
506		remove_dups(UsedIDs, VarNames).
507		% otherwise, consider all variables used in the examples
508		get_involved_variables_aux(_, PosInput, _, VarNames) :-
509		PosInput = [Example|_],
510		maplist(get_varname_from_node_info, Example, VarNames).
511
512		check_states_on_guards(State, Guards, ViolatedGuards) :-
513		maplist(create_equality_nodes_from_example, State, StateEqualities),
514		findall(Guard, ( member(Guard, Guards),
515		check_states_on_guard(StateEqualities, Guard)
516		), ValidGuards),
517		subtract(Guards, ValidGuards, ViolatedGuards).
518		check_states_on_guard([], _).
519		check_states_on_guard([StateEquality|T], Guard) :-
520		conjunct_predicates([Guard|StateEquality], CheckGuard),
521		b_test_boolean_expression_wf_no_bindings(CheckGuard, []),
522		!,
523		check_states_on_guard(T, Guard).
524
525		:- spec_pre(get_violated_and_valid_machine_invariants/4, [list(ast),var,var,var]).
526		:- spec_invariant(get_violated_and_valid_machine_invariants/4, [list(ast),list(ast),list(ast),list(ast)]).
527		:- spec_post(get_violated_and_valid_machine_invariants/4, [list(ast),var,var,var],
528		[list(ast),list(ast),list(ast),list(ast)]).
529		get_violated_and_valid_machine_invariants(Input, ViolatedInvariants, ViolatingVars, ValidInvariants) :-
530		% according to specific operation
531		get_invariants_for_current_vars(Input, _, InvariantList),
532		% consider the machine properties in case an invariant refers to machine constants
533		b_get_properties_from_machine(MachineProperties),
534		maplist(get_violated_and_valid_machine_invariants_aux(MachineProperties, InvariantList), Input, TempViolatedInvariants),
535		tools:flatten(TempViolatedInvariants, TempViolatedInvariants2),
536		remove_dups(TempViolatedInvariants2, ViolatedInvariants),
537		conjunct_predicates(ViolatedInvariants, TempPred),
538		find_typed_identifier_uses_with_info(TempPred, TempViolatingVars),
539		b_get_machinevars_with_operation_params(MachineVars),
540		% filter only machine variables from TempViolatingVars and do not consider machine constants that may occur within an invariant
541		% but do not define the machine state which only refers to machine variables
542		findall(MachineVar, ( member(MachineVar, TempViolatingVars),
543		get_varname_from_id_node(MachineVar, MachineVarName),
544		member(b(identifier(MachineVarName),_,_), MachineVars)
545		), ViolatingVars),
546		% all other machine variables are valid considering the current machine variables
547		b_get_invariant_from_machine(MachineInvariant),
548		conjunction_to_list(MachineInvariant, MachineInvariantList),
549		subtract(MachineInvariantList, ViolatedInvariants, ValidInvariants).
550
551		get_violated_and_valid_machine_invariants_aux(MachineProperties, InvariantList, Input, ViolatedInvariants) :-
552		create_equality_nodes_from_example(Input, EqualityNodes),
553		conjunct_predicates([MachineProperties|EqualityNodes], EqualityPredWithMachineProperties),
554		get_violated_and_valid_machine_invariants_aux2(EqualityPredWithMachineProperties, InvariantList, ViolatedInvariants).
555
556		get_violated_and_valid_machine_invariants_aux2(_, [], []).
557		get_violated_and_valid_machine_invariants_aux2(EqualityNodes, [SingleInv|T], [SingleInv|NT]) :-
558		conjunct_predicates([EqualityNodes,SingleInv], InvPred),
559		\+ b_test_boolean_expression_wf_no_bindings(InvPred, []),
560		!,
561		get_violated_and_valid_machine_invariants_aux2(EqualityNodes, T, NT).
562		get_violated_and_valid_machine_invariants_aux2(EqualityNodes, [_|T], NT) :-
563		get_violated_and_valid_machine_invariants_aux2(EqualityNodes, T, NT).
564
565		% Get the machine invariants considering at least one of the current variables derived from the examples.
566		get_invariants_for_current_vars(Examples, TypedIDs, InvariantList) :-
567		Examples = [Example|_],
568		maplist(get_varname_from_node_info, Example, VarNames),
569		get_machinevars_by_name(VarNames, TypedIDs),
570		b_get_invariant_from_machine(MachineInvariant),
571		conjunction_to_list(MachineInvariant, CompleteInvariantList),
572		findall(Invariant, ( member(Invariant, CompleteInvariantList),
573		find_identifier_uses(Invariant, [], UsedIDs),
574		intersection(UsedIDs, VarNames, Intersection),
575		Intersection \= []
576		), InvariantList).
577
578		% Check if the given examples are already reduced by the user, i.e., they refer to less variables than
579		% there are machine variables.
580		examples_already_reduced(Examples) :-
581		Examples = [Example|_],
582		length(Example, VarAmount),
583		b_get_machinevars_with_operation_params(MachineVars),
584		length(MachineVars, MachineVarAmount),
585		VarAmount < MachineVarAmount.
586
587		% The examples are tuples of variable name and pretty value from the java ui.
588		get_invariant_violating_vars_from_examples([], [], []) :-
589		!.
590		get_invariant_violating_vars_from_examples(Positive, Negative, ViolatingVarNames) :-
591		% split examples that are tuples of input and output state
592		split_input_output_tuples(Positive, PosInput, PosOutput),
593		split_input_output_tuples(Negative, NegInput, NegOutput),
594		append([PosInput,PosOutput,NegInput,NegOutput], Input),
595		get_violated_and_valid_machine_invariants(Input, _, ViolatingVars, _),
596		!,
597		maplist(get_varname_from_id_node, ViolatingVars, ViolatingVarNames).
598
599		% Get another transition that violates the invariant, exclude given input/output example.
600		:- spec_pre(get_invariant_violating_transition/6, [atom,list(ast),list(ast),list(ast),list(ast),var]).
601		:- spec_invariant(get_invariant_violating_transition/6, [atom,list(ast),list(ast),list(ast),list(ast),pair(ast,ast)]).
602		:- spec_post(get_invariant_violating_transition/6, [atom,list(ast),list(ast),list(ast),list(ast),var],
603		[atom,list(ast),list(ast),list(ast),list(ast),pair(ast,ast)]).
604		get_invariant_violating_transition(Operation, UsedVars, ViolatedInvariants, Input, Output, Counter) :-
605		b_get_machine_operation(Operation, _, _, TOpBody),
606		% don't create contradiction in case the guard is equivalent
607		% to an invariant which we will negate in the following
608		remove_pre_condition_from_body(TOpBody, OpBody),
609		before_after_predicate_with_equalities(OpBody, UsedVars, BABody),
610		% find_identifier_uses(OpBody,[],BodyIDs) ,
611		findall(V, ( member(b(identifier(V),_,_), UsedVars)
612		), BodyIDs),
613		b_get_machinevars_with_operation_params(MachineVars),
614		create_equality_nodes_from_examples(BodyIDs, Input, Output, MachineVars, TNodeList),
615		% negate equalities to exclude this transition
616		findall(Inequality, ( create_texpr(negation(Equality), pred, [], Inequality),
617		member(Equality, TNodeList)
618		), NodeList),
619		conjunct_predicates(ViolatedInvariants, Invariant),
620		maplist(get_varname_from_id_node, MachineVars, MachineVarNames),
621		prime_or_unprime_variables_in_ast(prime, MachineVarNames, Invariant, PrimedInvariant),
622		create_texpr(negation(Invariant), pred, [], NInvariant),
623		create_texpr(negation(PrimedInvariant), pred, [], NPrimedInvariant),
624		conjunct_predicates([BABody,NInvariant,NPrimedInvariant|NodeList], BAExclusion),
625		solve_predicate(BAExclusion, _, Solution),
626		get_invariant_violating_transition_aux(Solution, Counter).
627
628		get_invariant_violating_transition_aux(Solution, none) :-
629		Solution \= solution(_).
630		get_invariant_violating_transition_aux(solution(Solution), (CounterInput,CounterOutput)) :-
631		% split by input and output state
632		get_input_output_nodes_from_bindings(Solution, CounterInput, CounterOutput).
633
634		get_invariant_violating_example(_, [], [], _) :-
635		fail.
636		get_invariant_violating_example(ViolatedInvariants, [PosInput|TIn], [PosOutput|TOut], Example) :-
637		maplist(check_invariant_on_state(PosInput, PosOutput), ViolatedInvariants),
638		!,
639		% transition doesn't violate an invariant
640		get_invariant_violating_example(ViolatedInvariants, TIn, TOut, Example).
641		% invariant violating transition found
642		get_invariant_violating_example(_, [PosInput|_], [PosOutput|_], (PosInput,PosOutput)).
643
644		% Is true if the given invariant is true for the pair of input/output states.
645		check_invariant_on_state(Input, Output, InvariantAst) :-
646		create_equality_nodes_from_examples(Input, Output, EqualityNodes),
647		conjunct_predicates([InvariantAst|EqualityNodes], InvariantTransitionPred),
648		b_test_boolean_expression_wf_no_bindings(InvariantTransitionPred, _).
649
650		%% Get the input and/or output nodes from a solution of the distinguishing constraint.
651		:- spec_pre(get_input_output_nodes_from_bindings/3, [solution_bindings,var,var]).
652		:- spec_invariant(get_input_output_nodes_from_bindings/3, [solution_bindings,list(ast),list(ast)]).
653		:- spec_post(get_input_output_nodes_from_bindings/3, [solution_bindings,var,var], [solution_bindings,list(ast),list(ast)]).
654		get_input_output_nodes_from_bindings(Solution, Input, Output) :-
655		get_input_nodes_from_bindings(Solution, Input),
656		get_output_nodes_from_bindings(Solution, Output).
657
658		:- spec_pre(get_input_nodes_from_bindings/2, [solution_bindings,var]).
659		:- spec_invariant(get_input_nodes_from_bindings/2, [solution_bindings,list(ast)]).
660		:- spec_post(get_input_nodes_from_bindings/2, [solution_bindings,var], [solution_bindings,list(ast)]).
661		get_input_nodes_from_bindings(Solution, Input) :-
662		findall(Binding, ( member(Binding, Solution),
663		get_varname_from_binding(Binding, VarName),
664		\+ is_primed_id(VarName)
665		), Bindings),
666		example_bindings_to_ast_nodes(Bindings, Input).
667
668		:- spec_pre(get_output_nodes_from_bindings/2, [solution_bindings,var]).
669		:- spec_invariant(get_output_nodes_from_bindings/2, [solution_bindings,list(ast)]).
670		:- spec_post(get_output_nodes_from_bindings/2, [solution_bindings,var], [solution_bindings,list(ast)]).
671		get_output_nodes_from_bindings(Solution, Output) :-
672		get_output_nodes_from_bindings_aux(Solution, NewSolution),
673		example_bindings_to_ast_nodes(NewSolution, Output).
674		get_output_nodes_from_bindings_aux([], []).
675		get_output_nodes_from_bindings_aux([Binding|T], [Binding|NT]) :-
676		get_varname_from_binding(Binding, VarName),
677		is_primed_id(VarName),
678		!,
679		get_output_nodes_from_bindings_aux(T, NT).
680		get_output_nodes_from_bindings_aux([_|T], NT) :-
681		get_output_nodes_from_bindings_aux(T, NT).
682
683		get_varname_from_binding(binding(VarName,_,_), VarName).
684		get_varname_from_binding(bind(VarName,_), VarName).
685
686		remove_pre_condition_from_body(b(Node,_,_), Body) :-
687		functor(Node, Functor, Arity),
688		Functor == rlevent,
689		Arity == 11,
690		arg(7, Node, Actions),
691		!,
692		create_texpr(parallel(Actions), subst, [], OpBody),
693		remove_pre_condition_from_body(OpBody, Body).
694		remove_pre_condition_from_body(b(any(_,_,TActions),subst,_), Body) :-
695		( is_list(TActions) ->
696		Actions = TActions
697		; Actions = [TActions]
698		),
699		!,
700		create_texpr(parallel(Actions), subst, [], OpBody),
701		remove_pre_condition_from_body(OpBody, Body).
702		remove_pre_condition_from_body(PreBody, Body) :-
703		PreBody = b(precondition(_,Body),_,_),
704		!.
705		remove_pre_condition_from_body(Body, Body).
706
707		% prime/unprime all identifiers in VarsToConsider within an ast, if VarsToConsider is an empty list prime/unprime all variables
708		:- spec_pre(prime_or_unprime_variables_in_ast/4, [atom,list(ast),ast,var]).
709		:- spec_invariant(prime_or_unprime_variables_in_ast/4, [atom,list(ast),ast,ast]).
710		:- spec_post(prime_or_unprime_variables_in_ast/4, [atom,list(ast),ast,var], [atom,list(ast),ast,ast]).
711		prime_or_unprime_variables_in_ast(prime, VarsToConsider, b(identifier(ID),Type,Info), PrimedID) :-
712		( member(ID, VarsToConsider)
713		; VarsToConsider = []
714		),
715		!,
716		prime_identifier(b(identifier(ID),Type,Info), PrimedID).
717		prime_or_unprime_variables_in_ast(prime, VarsToConsider, b(identifier(ID),Type,Info), Ast) :-
718		!,
719		\+ member(ID, VarsToConsider),
720		Ast = b(identifier(ID),Type,Info).
721		prime_or_unprime_variables_in_ast(unprime, VarsToConsider, b(identifier(ID),Type,Info), UnprimedID) :-
722		( member(ID, VarsToConsider)
723		; VarsToConsider = []
724		),
725		!,
726		( is_primed_id(ID)
727		->
728		remove_prime(b(identifier(ID),Type,Info), UnprimedID)
729		; UnprimedID = b(identifier(ID),Type,Info)
730		).
731		prime_or_unprime_variables_in_ast(unprime, VarsToConsider, b(identifier(ID),Type,Info), Ast) :-
732		!,
733		\+ member(ID, VarsToConsider),
734		Ast = b(identifier(ID),Type,Info).
735		prime_or_unprime_variables_in_ast(_, _, b(Node,Type,Info), Ast) :-
736		( Node = integer(_)
737		; Node = value(_)
738		; Node = integer_set(_)
739		; Node = string(_)
740		; Node =.. [_]
741		),
742		!,
743		Ast = b(Node,Type,Info).
744		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, b(Node,Type,Info), b(NewNode,Type,Info)) :-
745		Node = parallel(Assignments),
746		maplist(prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider), Assignments, NewAssignments),
747		NewNode = parallel(NewAssignments).
748		% skip nodes like comprehension_set, set_extension or sequence_extension
749		prime_or_unprime_variables_in_ast(_, _, b(Node,Type,Info), b(Node,Type,Info)) :-
750		functor(Node, OpType, _),
751		( OpType = comprehension_set
752		; OpType = set_extension
753		; OpType = sequence_extension
754		),
755		!.
756		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, b(Node,Type,Info), b(NewNode,Type,Info)) :-
757		Node =.. [Op,In],
758		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, In, NewIn),
759		NewNode =.. [Op,NewIn].
760		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, b(exists(Ids,Pred),Type,Info), b(exists(NewIds,NewPred),Type,Info)) :-
761		maplist(prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider), Ids, NewIds),
762		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, Pred, NewPred).
763		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, b(Node,Type,Info), b(NewNode,Type,Info)) :-
764		Node =.. [Op,In1,In2],
765		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, In1, NewIn1),
766		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, In2, NewIn2),
767		NewNode =.. [Op,NewIn1,NewIn2].
768		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, b(forall(Ids,Left,Right),Type,Info), b(forall(NewIds,NewLeft,NewRight),Type,Info)) :-
769		maplist(prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider), Ids, NewIds),
770		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, Left, NewLeft),
771		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, Right, NewRight).
772		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, b(Node,Type,Info), b(NewNode,Type,Info)) :-
773		% e.g. if_then_else
774		Node =.. [Op,In1,In2,In3],
775		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, In1, NewIn1),
776		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, In2, NewIn2),
777		prime_or_unprime_variables_in_ast(PrimeType, VarsToConsider, In3, NewIn3),
778		NewNode =.. [Op,NewIn1,NewIn2,NewIn3].
779
780		% Check that all negative inputs are invalid for the operation's precondition.
781		check_negative_inputs_against_operation_precondition(_, []). % no negative input states are present
782		check_negative_inputs_against_operation_precondition(Operation, NegInput) :-
783		NegInput \= [],
784		b_get_machine_operation(Operation, _, _, OpBody),
785		OpBody = b(precondition(PreCondition,_),_,_),
786		check_negative_inputs_against_operation_precondition_aux(PreCondition, NegInput).
787
788		% fails if any negative input state is valid on the current precondition, that means, the precondition needs to be strengthened
789		check_negative_inputs_against_operation_precondition_aux(_, []).
790		check_negative_inputs_against_operation_precondition_aux(PreCondition, [NegState|T]) :-
791		create_equality_nodes_from_example(NegState, EqualityNodes),
792		conjunct_predicates([PreCondition|EqualityNodes], EqualityPred),
793		\+ b_test_boolean_expression_wf_no_bindings(EqualityPred, _),
794		check_negative_inputs_against_operation_precondition_aux(PreCondition, T).
795
796		%% User adds a missing state transition.
797		% Search for a machine operation that completely supports the missing state
798		% or one where we just have to synthesize a relaxed guard.
799		% VarNames refers to the variables used in the added states.
800		check_transitions_against_machine_operations(VarNodes, InputExamples, OutputExamples, Result) :-
801		% check each example againt the existing machine operations
802		maplist(check_transition_against_machine_operations(VarNodes), InputExamples, OutputExamples, SingleResults),
803		check_transitions_against_machine_operations_aux(SingleResults, Result),
804		!.
805		check_transitions_against_machine_operations_aux(SingleResults, Result) :-
806		% an operation satisifies the transition but its guard needs to be relaxed
807		member((OpName,guard), SingleResults),
808		% and all other example transitions are also satisfied by this operation,
809		maplist(operation_match(OpName), SingleResults),
810		% therefore we synthesize a relaxed guard
811		Result = (OpName,guard).
812		check_transitions_against_machine_operations_aux(SingleResults, Result) :-
813		% an operation satisifies all transitions, and thus, we don't have to synthesize anything
814		member((OpName,done), SingleResults),
815		maplist('='((OpName,done)), SingleResults),
816		Result = (OpName,done).
817		check_transitions_against_machine_operations_aux(_, no_match).
818
819		operation_match(OpName, (OpName,_)).
820
821		:- spec_pre(check_transition_against_machine_operations/4, [list(ast),list(ast),list(ast),var]).
822		:- spec_invariant(check_transition_against_machine_operations/4, [list(ast),list(ast),list(ast),
823		one_of([atom,pair(atom,atom)])]).
824		:- spec_post(check_transition_against_machine_operations/4, [list(ast),list(ast),list(ast),var],
825		[list(ast),list(ast),list(ast),
826		one_of([atom,pair(atom,atom)])]).
827		% Check a single transition against the existing machine operations.
828		check_transition_against_machine_operations(VarNodes, Input, Output, Result) :-
829		findall((Op,Res,Par,Body), b_get_machine_operation(Op, Res, Par, Body), Operations),
830		check_transition_against_machine_operations(Operations, Input, Output, VarNodes, Result).
831		check_transition_against_machine_operations([], _, _, _, no_match).
832		check_transition_against_machine_operations([(_,_,_,b(skip,subst,_))|T], Input, Output, VarNodes, Result) :-
833		check_transition_against_machine_operations(T, Input, Output, VarNodes, Result).
834		% Skip if the desired action's and the given ones' variables doesn't match.
835		check_transition_against_machine_operations([(_,_,_,OpBody)|T], Input, Output, VarNodes, Result) :-
836		find_identifier_uses(OpBody, [], BodyIDs),
837		findall(Name, member(b(identifier(Name),_,_), VarNodes), VarNames),
838		% find distinguishing variables
839		findall(DistName, ( member(DistName, BodyIDs),
840		\+ member(DistName, VarNames)
841		), DistNames),
842		DistNames \= [],
843		!,
844		check_transition_against_machine_operations(T, Input, Output, VarNodes, Result).
845		check_transition_against_machine_operations([(OpName,_,_,OpBody)|T], Input, Output, VarNodes, Result) :-
846		b_get_machinevars_with_operation_params(MachineVars),
847		before_after_predicate_with_equalities(OpBody, MachineVars, BABody),
848		find_identifier_uses(OpBody, [], BodyIDs),
849		create_equality_nodes_from_examples(BodyIDs, Input, Output, VarNodes, NodeList),
850		b_get_typed_invariant_from_machine(Invariant),
851		conjunct_predicates([BABody,Invariant|NodeList], BABodyPred),
852		check_transition_against_machine_operations_aux(BABodyPred, NodeList, [(OpName,_,_,OpBody)|T], Input, Output, VarNodes, Result).
853
854		% Found operation that already executes the transition.
855		check_transition_against_machine_operations_aux(BABodyPred, _, [(OpName,_,_,_)|_], _, _, _, (OpName,done)) :-
856		solve_predicate(BABodyPred, _, solution(_)),
857		!.
858		% Only the guard of an operation does not fit.
859		check_transition_against_machine_operations_aux(_, NodeList, [(OpName,_,_,OpBody)|_], _, _, _, (OpName,guard)) :-
860		b_get_machinevars_with_operation_params(MachineVars),
861		% remove guard and try if action itself supports the missing state
862		OpBody = b(precondition(_PreCondition,Action),_,_),
863		before_after_predicate_with_equalities(Action, MachineVars, BAAction),
864		conjunct_predicates([BAAction|NodeList], BAActionPred),
865		solve_predicate(BAActionPred, _, solution(_)),
866		!.
867		% The action also does not match so that we search for another operation.
868		check_transition_against_machine_operations_aux(_, _, [_|T], Input, Output, VarNodes, Result) :-
869		check_transition_against_machine_operations(T, Input, Output, VarNodes, Result).
870		%%
871		% Get valid transitions for an operation and return tuples holding pretty printed equality predicates of before/after states.
872		% Furthermore, get invalid states if a precondition is given and return pretty printed equality predicates for this states.
873		% We can directly use these pretty printed predicates to compute the states in ProB2 using FindStateCommand.
874		get_valid_and_invalid_equality_predicates_for_operation(OperationName, ValidAmount, InvalidAmount, ValidPrettyEqualityTuples, InvalidPrettyEqualities, IgnoredIDs) :-
875		preferences:set_preference(randomise_enumeration_order, true),
876		b_get_machine_operation(OperationName, _, _, Substitution),
877		find_identifier_uses(Substitution, [], TempUsedIDs),
878		% filter only machine variables, an operation may access machine constants that we need to discard here
879		b_get_machinevars_with_operation_params(MachineVars),
880		findall(UsedID, ( member(UsedID, TempUsedIDs),
881		member(b(identifier(UsedID),_,_), MachineVars)
882		), UsedIDs),
883		findall(IgnoredID, ( member(b(identifier(IgnoredID),_,_), MachineVars),
884		\+ member(IgnoredID, UsedIDs)
885		), IgnoredIDs),
886		get_machinevars_by_name(UsedIDs, UsedMachineVars),
887		get_valid_transitions_for_operation(UsedMachineVars, ValidAmount, OperationName, BeforeStates, AfterStates),
888		maplist(create_equality_predicate_from_example, BeforeStates, BeforeEqualities),
889		maplist(create_equality_predicate_from_example, AfterStates, AfterEqualities),
890		maplist(translate_bexpression, BeforeEqualities, PrettyBeforeEqualities),
891		maplist(translate_bexpression, AfterEqualities, PrettyAfterEqualities),
892		zip(PrettyBeforeEqualities, PrettyAfterEqualities, ValidPrettyEqualityTuples),
893		get_invalid_state_equalities_for_operation(OperationName, UsedMachineVars, InvalidAmount, Substitution, InvalidEqualities),
894		maplist(translate_bexpression, InvalidEqualities, InvalidPrettyEqualities),
895		!.
896
897		get_invalid_state_equalities_for_operation(OperationName, MachineVars, Amount, b(precondition(Precondition,_),subst,_), InvalidEqualities) :-
898		!,
899		% additionally consider the machine properties since a precondition may access machine constants
900		b_get_properties_from_machine(MachineProperties),
901		% filter predicates that set the types of operation parameters from the actual preconditions, since we do not want to negate the typing of operation parameters in the following
902		b_get_machine_operation(OperationName, _, OperationParams, _),
903		split_typing_predicates_from_precondition(OperationParams, Precondition, TypingPredicates, PreconditionPredicate),
904		conjunct_predicates([MachineProperties,TypingPredicates,b(negation(PreconditionPredicate),pred,[])], NegatedPrecondition),
905		get_invalid_state_equalities_for_operation_aux(MachineVars, Amount, NegatedPrecondition, [], InvalidStates),
906		maplist(create_equality_predicate_from_example, InvalidStates, InvalidEqualities).
907		% no precondition is given
908		get_invalid_state_equalities_for_operation(_, _, _, _, []).
909
910		get_invalid_state_equalities_for_operation_aux(_, 0, _, Acc, Acc).
911		get_invalid_state_equalities_for_operation_aux(MachineVars, Amount, PreconditionWithProperties, Acc, InvalidStates) :-
912		exclude_accumulated_states(MachineVars, Acc, [], TExclusion),
913		( TExclusion = [] ->
914		Exclusion = b(truth,pred,[])
915		; Exclusion = TExclusion
916		),
917		create_texpr(conjunct(Exclusion,PreconditionWithProperties), pred, [], Predicate),
918		solve_predicate(Predicate, _, Solution),
919		Solution = solution(SolutionBindings),
920		!,
921		% solutions may also refer to machine constants that we do not want to consider here since we search for machine states
922		findall(Binding, ( member(Binding, SolutionBindings),
923		Binding = binding(Name,_,_),
924		member(b(identifier(Name),_,_), MachineVars)
925		), MachineVarBindings),
926		example_bindings_to_ast_nodes(MachineVarBindings, InvalidState),
927		NAmount is Amount-1,
928		get_invalid_state_equalities_for_operation_aux(MachineVars, NAmount, PreconditionWithProperties, [InvalidState|Acc], InvalidStates).
929		get_invalid_state_equalities_for_operation_aux(_, _, _, Acc, Acc).
930
931		get_valid_transitions_for_operation(CurrentVars, Amount, OperationName, BeforeStates, AfterStates) :-
932		Amount \= 0,
933		get_valid_inputs_for_operation(OperationName, Amount, ValidInputStates),
934		maplist(create_equality_nodes_from_example, ValidInputStates, ValidInputStateEqualities),
935		before_after_predicate_for_operation(OperationName, BeforeAfterPredicate),
936		get_valid_transitions_for_operation_aux(CurrentVars, ValidInputStateEqualities, BeforeAfterPredicate, [], [], BeforeStates, AfterStates).
937		get_valid_transitions_for_operation(_, _, _, [], []).
938
939		get_valid_transitions_for_operation_aux(_, [], _, BeforeAcc, AfterAcc, BeforeAcc, AfterAcc).
940		get_valid_transitions_for_operation_aux(CurrentVars, [ValidInputStateEquality|T], BeforeAfterPredicate, BeforeAcc, AfterAcc, BeforeStates, AfterStates) :-
941		conjunct_predicates(ValidInputStateEquality, InputEquality),
942		solve_predicate(b(conjunct(InputEquality,BeforeAfterPredicate),pred,[]), _, Solution),
943		Solution = solution(SolutionBindings),
944		!,
945		% solutions may also refer to machine constants that we do not want to consider here since we search for machine states
946		findall(Primed, ( member(Primed, SolutionBindings),
947		Primed = binding(Name,_,_),
948		is_primed_id(Name),
949		remove_prime(b(identifier(Name),_,_), UnprimedAst),
950		member(UnprimedAst, CurrentVars)
951		), AfterBindings),
952		sets:subtract(SolutionBindings, AfterBindings, TempBeforeBindings),
953		findall(Unprimed, ( member(Unprimed, TempBeforeBindings),
954		Unprimed = binding(Name,_,_),
955		\+ is_primed_id(Name),
956		member(b(identifier(Name),_,_), CurrentVars)
957		), BeforeBindings),
958		example_bindings_to_ast_nodes(BeforeBindings, Before),
959		example_bindings_to_ast_nodes(AfterBindings, After),
960		get_valid_transitions_for_operation_aux(CurrentVars, T, BeforeAfterPredicate, [Before|BeforeAcc], [After|AfterAcc], BeforeStates, AfterStates).
961		get_valid_transitions_for_operation_aux(CurrentVars, [_|T], BeforeAfterPredicate, BeforeAcc, AfterAcc, BeforeStates, AfterStates) :-
962		get_valid_transitions_for_operation_aux(CurrentVars, T, BeforeAfterPredicate, BeforeAcc, AfterAcc, BeforeStates, AfterStates).
963
964		exclude_accumulated_states(_, [], Acc, Exclusion) :-
965		conjunct_predicates(Acc, Exclusion).
966		exclude_accumulated_states(CurrentVars, [BeforeState|T], Acc, Exclusion) :-
967		maplist(exclude_variable_state(CurrentVars), BeforeState, ExclusionList),
968		conjunct_predicates(ExclusionList, Inequalities),
969		exclude_accumulated_states(CurrentVars, T, [Inequalities|Acc], Exclusion).
970
971		exclude_variable_state(MachineVars, b(Node,Type,Info), Inequality) :-
972		member(synthesis(machinevar,VarName), Info),
973		member(b(identifier(VarName),MachineVarType,MachineVarInfo), MachineVars),
974		create_texpr(not_equal(b(Node,Type,Info),b(identifier(VarName),MachineVarType,MachineVarInfo)), pred, [], Inequality).
975
976		% Filter predicates that set the types of operation parameters from the actual preconditions.
977		split_typing_predicates_from_precondition(OperationParams, Precondition, TypingPredicate, PreconditionPredicate) :-
978		maplist(get_texpr_id, OperationParams, OperationParamNames),
979		conjunction_to_list(Precondition, PreconditionList),
980		findall(TypingPred, ( member(TypingPred, PreconditionList),
981		find_identifier_uses(TypingPred, [], UsedIDs),
982		sets:intersection(UsedIDs, OperationParamNames, Intersection),
983		Intersection \= []
984		), TypingPredicatesList),
985		sets:subtract(PreconditionList, TypingPredicatesList, ActualPreconditionList),
986		conjunct_predicates(TypingPredicatesList, TypingPredicate),
987		conjunct_predicates(ActualPreconditionList, PreconditionPredicate).
988
989		% Can be used in both directions: Either VarName or Value has to be ground.
990		:- spec_pre(get_binding_for_name_or_value/3, [solution_bindings,one_of([var,atom]),one_of([var,atom,compound])]).
991		:- spec_invariant(get_binding_for_name_or_value/3, [solution_bindings,one_of([var,atom]),one_of([var,atom,compound])]).
992		:- spec_post(get_binding_for_name_or_value/3, [solution_bindings,one_of([var,atom]),one_of([var,atom,compound])],
993		[solution_bindings,one_of([var,atom]),one_of([var,atom,compound])]).
994		get_binding_for_name_or_value(SolutionBindings, VarName, Value) :-
995		( member(binding(VarName,Value,_), SolutionBindings)
996		;
997		member(bind(VarName,Value), SolutionBindings)
998		).
999
1000		% search identifier nodes within an ast and keep each nodes information
1001		find_typed_identifier_uses_with_info(AST, UsedIDs) :-
1002		find_typed_identifier_uses_with_info_aux(AST, TempUsedIDs),
1003		remove_dups(TempUsedIDs, UsedIDs),
1004		!.
1005
1006		find_typed_identifier_uses_with_info_aux(List, IDs) :-
1007		is_list(List),
1008		findall(ID, ( member(ID, List),
1009		ID = b(identifier(_),_,_)
1010		), IDs).
1011		find_typed_identifier_uses_with_info_aux(b(identifier(IDName),Type,Info), [b(identifier(IDName),Type,Info)]).
1012		find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
1013		Node =.. [Name,List],
1014		( Name = set_extension
1015		; Name = parallel
1016		),
1017		maplist(find_typed_identifier_uses_with_info_aux, List, UsedIDsNested),
1018		tools:flatten(UsedIDsNested, UsedIDs).
1019		find_typed_identifier_uses_with_info_aux(b(assign_single_id(_ID,Ast),_,_), UsedIDs) :-
1020		find_typed_identifier_uses_with_info_aux(Ast, UsedIDs).
1021		find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
1022		Node = if_then_else(Condition,TrueOut,FalseOut),
1023		find_typed_identifier_uses_with_info_aux(Condition, ConditionIDs),
1024		find_typed_identifier_uses_with_info_aux(TrueOut, TrueOutIDs),
1025		find_typed_identifier_uses_with_info_aux(FalseOut, FalseOutIDs),
1026		append([ConditionIDs,TrueOutIDs,FalseOutIDs], UsedIDs).
1027		find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
1028		Node = forall(_Ids,Left,Right),
1029		find_typed_identifier_uses_with_info_aux(Left, LeftIDs),
1030		find_typed_identifier_uses_with_info_aux(Right, RightIDs),
1031		append([LeftIDs,RightIDs], UsedIDs).
1032		find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
1033		Node =.. [_,Arg],
1034		find_typed_identifier_uses_with_info_aux(Arg, UsedIDs).
1035		find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
1036		Node =.. [_,Arg1,Arg2],
1037		find_typed_identifier_uses_with_info_aux(Arg1, UsedIDs1),
1038		find_typed_identifier_uses_with_info_aux(Arg2, UsedIDs2),
1039		append(UsedIDs1, UsedIDs2, UsedIDs).
1040		find_typed_identifier_uses_with_info_aux(b(Node,_,_), UsedIDs) :-
1041		functor(Node, Functor, Arity),
1042		Functor = rlevent,
1043		Arity = 5,
1044		arg(5, Node, Body),
1045		find_typed_identifier_uses_with_info_aux(Body, UsedIDs).
1046		find_typed_identifier_uses_with_info_aux(_, []).
1047
1048		% Get current identifier names from an example before creating equality nodes to the example.
1049		:- spec_pre(create_equality_nodes_from_examples/3, [ast_example,ast_example,var]).
1050		:- spec_invariant(create_equality_nodes_from_examples/3, [ast_example,ast_example,ast_example]).
1051		:- spec_post(create_equality_nodes_from_examples/3, [ast_example,ast_example,var],
1052		[ast_example,ast_example,ast_example]).
1053		create_equality_nodes_from_examples(Input, Output, EqualityNodes) :-
1054		b_get_machinevars_with_operation_params(MachineVars),
1055		maplist(get_varname_from_node_info, Input, CurrentIDs),
1056		create_equality_nodes_from_examples(CurrentIDs, Input, Output, MachineVars, EqualityNodes).
1057		% We need to set variables to values from example by creating equality nodes
1058		% that we can add to the before after predicate.
1059		create_equality_nodes_from_examples([], _, _, _, []).
1060		create_equality_nodes_from_examples([VarName|T], Input, Output, VarNodes, [Node1,Node2|NodeList]) :-
1061		member(VarNode, VarNodes),
1062		VarNode = b(identifier(VarName),_,_),
1063		member(InputNode, Input),
1064		get_varname_from_node_info(InputNode, VarName),
1065		member(OutputNode, Output),
1066		get_varname_from_node_info(OutputNode, VarName),
1067		Node1 = b(equal(VarNode,InputNode),pred,[]),
1068		prime_identifier(VarNode, PrimedVarNode),
1069		Node2 = b(equal(PrimedVarNode,OutputNode),pred,[]),
1070		create_equality_nodes_from_examples(T, Input, Output, VarNodes, NodeList).
1071
1072		create_equality_nodes_from_example(ExampleState, EqualityNodes) :-
1073		create_equality_nodes_from_example(ExampleState, [], EqualityNodes).
1074		create_equality_nodes_from_example([], Acc, Acc).
1075		create_equality_nodes_from_example([ValueAst|T], Acc, EqualityNodes) :-
1076		get_varname_from_node_info(ValueAst, VarName),
1077		ValueAst = b(_,VarType,_),
1078		% note: following enforces variables to be real machine variables
1079		% (we consider operation parameters to be part of our I/O "state" in synthesis by marking them with machinevar/1 in AST info)
1080		%get_machinevars_by_name([VarName], [MachineVar]),
1081		Var = b(identifier(VarName),VarType,[]),
1082		Equality = b(equal(Var,ValueAst),pred,[]),
1083		create_equality_nodes_from_example(T, [Equality|Acc], EqualityNodes).
1084
1085		create_equality_predicate_from_example(ExampleState, EqualityPredicate) :-
1086		create_equality_nodes_from_example(ExampleState, EqualityNodes),
1087		conjunct_predicates(EqualityNodes, EqualityPredicate).
1088
1089		get_location_var_node_by_info_term(LocationVars, SynthesisTerm, LocationVar) :-
1090		member(LocationVar, LocationVars),
1091		LocationVar = b(identifier(_),integer,Info),
1092		member(SynthesisTerm, Info).
1093
1094		get_var_node_by_info_term(LocationVars, SynthesisTerm, LocationVar) :-
1095		member(LocationVar, LocationVars),
1096		get_texpr_info(LocationVar, Info),
1097		member(SynthesisTerm, Info).
1098
1099		get_location_var_node_by_name(LocationVarName, LocationVars, LocationVarNode) :-
1100		member(LocationVarNode, LocationVars),
1101		LocationVarNode = b(identifier(LocationVarName),integer,_).
1102
1103		% Compute some valid input states for a given operation by considering the invariant as well as the operation's precondition.
1104		get_valid_inputs_for_operation(OperationName, C, ValidStates) :-
1105		preferences:get_preference(randomise_enumeration_order, RandEnumOrder),
1106		preferences:set_preference(randomise_enumeration_order, true),
1107		b_get_machine_operation(OperationName, _, _, Substitution),
1108		get_precondition_from_operation_body(Substitution, Precondition),
1109		% TODO: use complete invariant for UI
1110		b_get_typed_invariant_from_machine(Invariant),
1111		% consider the machine properties since the guard may access machine constants
1112		b_get_properties_from_machine(MachineProperties),
1113		conjunct_predicates([Invariant,Precondition,MachineProperties], PreconditionInvariant),
1114		solve_predicate(PreconditionInvariant, _, 1, [force_evaluation], SolutionTerm),
1115		SolutionTerm = solution(Solution),
1116		!,
1117		find_identifier_uses(Substitution, [], TempUsedIDs),
1118		% filter only machine variables, an operation may access machine constants that we need to discard here
1119		b_get_machinevars_with_operation_params(MachineVars),
1120		findall(UsedID, ( member(UsedID, TempUsedIDs),
1121		member(b(identifier(UsedID),_,_), MachineVars)
1122		), UsedIDs),
1123		get_machinevars_by_name(UsedIDs, UsedMachineVars),
1124		get_states_aux(UsedMachineVars, C, Solution, PreconditionInvariant, b(truth,pred,[]), ValidStates),
1125		!,
1126		% restore previous enumeration order
1127		( RandEnumOrder == false ->
1128		preferences:set_preference(randomise_enumeration_order, false)
1129		; true
1130		).
1131
1132		get_precondition_from_operation_body(b(select([b(select_when(Condition,_),_,_)]),_,_), Condition).
1133		get_precondition_from_operation_body(b(precondition(Precondition,_),_,_), Precondition).
1134		get_precondition_from_operation_body(_, b(truth,pred,[])).
1135
1136		get_valid_and_invalid_equality_predicates_for_invariants(ValidAmount, InvalidAmount, ValidPrettyEqualities, InvalidPrettyEqualities) :-
1137		b_get_machinevars_with_operation_params(MachineVars),
1138		maplist(get_texpr_id, MachineVars, MachineVarNames),
1139		get_valid_states(MachineVarNames, ValidAmount, ValidStates),
1140		maplist(create_equality_predicate_from_example, ValidStates, ValidEqualities),
1141		maplist(translate_bexpression, ValidEqualities, ValidPrettyEqualities),
1142		get_invalid_states(MachineVarNames, InvalidAmount, InvalidStates),
1143		maplist(create_equality_predicate_from_example, InvalidStates, InvalidEqualities),
1144		maplist(translate_bexpression, InvalidEqualities, InvalidPrettyEqualities).
1145
1146		% Get invalid states for visualizing the invariants.
1147		:- spec_pre(get_invalid_states/3, [list(atom),int,var]).
1148		:- spec_invariant(get_invalid_states/3, [list(atom),int,list(ast)]).
1149		:- spec_post(get_invalid_states/3, [list(atom),int,var], [list(atom),int,list(ast)]).
1150		get_invalid_states(CurrentVarNames, C, ValidStates) :-
1151		preferences:set_preference(randomise_enumeration_order, true),
1152		b_get_invariant_from_machine(Invariant),
1153		Invariant \= b(truth,pred,_), % only typing invariants are given, we then do not provide any invalid states
1154		NegInvariant = b(negation(Invariant),pred,[]),
1155		solve_predicate(NegInvariant, _, 1, [force_evaluation], SolutionTerm),
1156		SolutionTerm = solution(Solution),
1157		!,
1158		get_machinevars_by_name(CurrentVarNames, CurrentVarNodes),
1159		get_states_aux(CurrentVarNodes, C, Solution, NegInvariant, b(truth,pred,[]), ValidStates).
1160		get_invalid_states(_, _, []).
1161
1162		% Get valid states for synthesis of invariants.
1163		:- spec_pre(get_valid_states/3, [list(atom),int,var]).
1164		:- spec_invariant(get_valid_states/3, [list(atom),int,list(ast)]).
1165		:- spec_post(get_valid_states/3, [list(atom),int,var], [list(atom),int,list(ast)]).
1166		get_valid_states(CurrentVarNames, C, ValidStates) :-
1167		preferences:set_preference(randomise_enumeration_order, true),
1168		b_get_typed_invariant_from_machine(Invariant),
1169		solve_predicate(Invariant, _, 1, [force_evaluation], SolutionTerm),
1170		SolutionTerm = solution(Solution),
1171		!,
1172		get_machinevars_by_name(CurrentVarNames, CurrentVarNodes),
1173		get_states_aux(CurrentVarNodes, C, Solution, Invariant, b(truth,pred,[]), ValidStates).
1174
1175		:- spec_pre(get_states_aux/6, [list(atom),int,solution_bindings,ast,ast,var]).
1176		:- spec_invariant(get_states_aux/6, [list(atom),int,solution_bindings,ast,ast,list(ast)]).
1177		:- spec_post(get_states_aux/6, [list(atom),int,solution_bindings,ast,ast,var], [list(atom),int,solution_bindings,ast,ast,list(ast)]).
1178		get_states_aux(CurrentVarNodes, C, Solution, Invariant, PriorExclusion, [ValidState|NT]) :-
1179		C \= 1,
1180		C1 is C-1,
1181		findall(Exclusion, ( member(Var, CurrentVarNodes),
1182		Var = b(identifier(VarName),Type,_),
1183		member(binding(VarName,Value,_), Solution),
1184		create_texpr(not_equal(Var,b(value(Value),Type,[])), pred, [], Exclusion)
1185		), ExclusionList),
1186		disjunct_predicates(ExclusionList, Exclusion),
1187		create_texpr(conjunct(PriorExclusion,Exclusion), pred, [], TExclusion),
1188		create_texpr(conjunct(Invariant,TExclusion), pred, [], NewPred),
1189		solve_predicate(NewPred, _, 1, [force_evaluation], SolutionTerm),
1190		SolutionTerm = solution(NewSolution),
1191		!,
1192		example_bindings_to_ast_nodes(Solution, TempValidState),
1193		reduce_state_to_current_vars(CurrentVarNodes, TempValidState, ValidState),
1194		get_states_aux(CurrentVarNodes, C1, NewSolution, NewPred, TExclusion, NT).
1195		get_states_aux(CurrentVarNodes, _, Solution, _, _, [ValidState]) :-
1196		is_list(Solution),
1197		example_bindings_to_ast_nodes(Solution, TempValidState),
1198		reduce_state_to_current_vars(CurrentVarNodes, TempValidState, ValidState).
1199		get_states_aux(_, _, _, _, _, []).
1200
1201		% A state is a list of ast value nodes each having the term synthesis/2 with the corresponding machine var name in its info.
1202		reduce_state_to_current_vars(CurrentVarNodes, State, ReducedState) :-
1203		findall(ValueNode, ( member(ValueNode, State),
1204		get_texpr_info(ValueNode, ValueNodeInfo),
1205		member(synthesis(machinevar,MachineVar), ValueNodeInfo),
1206		member(b(identifier(MachineVar),_,_), CurrentVarNodes)
1207		), ReducedState).
1208
1209		%% Only for synthesis of guards or invariants:
1210		% In case we synthesize guard/invariant it is possible that a state is graduated as positive and negative
1211		% because we replace output states with TRUE/FALSE. Thus, the constraint would have a contradiction.
1212		% E.g. synthesizing an invariant: If we graduate [0]-->[-1] as valid and [-1]-->[-2] as invalid,
1213		% we don't want to assume [-1] to be a negative state from the second example.
1214		% Synthesizing a guard it is the opposite, i.e., we don't want to assume [-1] to be a positive state.
1215		get_distinct_states(invariant, Positive, TempNegative, Positive, Negative) :-
1216		get_distinct_states(Positive, TempNegative, Negative).
1217		get_distinct_states(guard, TempPositive, Negative, Positive, Negative) :-
1218		get_distinct_states(Negative, TempPositive, Positive).
1219
1220		% Duplicates are subtracted from the examples given in the second argument.
1221		:- spec_pre(get_distinct_states/3, [ast_examples,ast_examples,var]).
1222		:- spec_invariant(get_distinct_states/3, [ast_examples,ast_examples,ast_examples]).
1223		:- spec_post(get_distinct_states/3, [ast_examples,ast_examples,var], [ast_examples,ast_examples,ast_examples]).
1224		get_distinct_states(Examples1, TempExamples2, Examples2) :-
1225		findall(E, ( member(E, TempExamples2),
1226		\+ contains_equivalent_state(E, Examples1, _)
1227		), Examples2).
1228
1229		% Mark initial examples to be able to restrict constant domains when defining the synthesis
1230		% constraint. Otherwise we would expand the constant domains for each new example derived from
1231		% distinguishing interactions.
1232		mark_examples_as_initial(TempPositive, TempNegative, Positive, Negative) :-
1233		maplist(mark_examples_as_initial_aux, TempPositive, Positive),
1234		maplist(mark_examples_as_initial_aux, TempNegative, Negative).
1235		mark_examples_as_initial_aux([], []).
1236		mark_examples_as_initial_aux([ValueNode|T], [b(Node,Type,NewInfo)|NT]) :-
1237		ValueNode = b(Node,Type,Info),
1238		mark_examples_as_initial_aux2(Info, NewInfo),
1239		mark_examples_as_initial_aux(T, NT).
1240		mark_examples_as_initial_aux2(Info, Info) :-
1241		member(synthesis(initial_example), Info).
1242		mark_examples_as_initial_aux2(Info, [synthesis(initial_example)|Info]) :-
1243		\+ member(synthesis(initial_example), Info).
1244
1245		% InputList contains all machine variables, but for synthesizing an invariant we only need to
1246		% observe variables from violated invariants.
1247		% Furthermore we accept hints from the user on variables that are probably involved in an action's
1248		% guard so we also need to reduce examples there.
1249		reduce_input_to_violating_vars(ViolatingVars, InputExample, ReducedExample) :-
1250		% find values of matching variable names located in ast nodes info term synthesis/2
1251		findall(Value, ( member(Value, InputExample),
1252		get_varname_from_node_info(Value, VarName),
1253		member(VarName, ViolatingVars)
1254		), ReducedExample).
1255
1256		% Get the current variables from an example (info contains synthesis/2 with var name).
1257		get_current_vars_from_example(Example, CurrentVars) :-
1258		b_get_machinevars_with_operation_params(MachineVars),
1259		findall(VarName, ( member(Node, Example),
1260		get_varname_from_node_info(Node, VarName)
1261		), CurrentVarNames),
1262		findall(VarNode, ( member(VarNode, MachineVars),
1263		VarNode = b(identifier(VarName),_,_),
1264		member(VarName, CurrentVarNames)
1265		), CurrentVars).
1266
1267		value_to_ast(Value, b(value(Value),Type,[])) :-
1268		kernel_objects:infer_value_type(Value, Type).
1269
1270		get_varname_from_node_info(b(_,_,Info), VarName) :-
1271		member(synthesis(machinevar,VarName), Info).
1272
1273		get_varname_from_id_node(b(identifier(VarName),_,_), VarName).
1274
1275		% translate prob values to asts node and add the machine variable name to each node's info
1276		example_bindings_to_ast_nodes([], []).
1277		example_bindings_to_ast_nodes([Binding|T], [Ast|NT]) :-
1278		( Binding = binding(TVarName,In,_)
1279		; Binding = bind(TVarName,In)
1280		),
1281		value_to_ast(In, TAst),
1282		remove_prime(TVarName, VarName),
1283		add_texpr_infos(TAst, [synthesis(machinevar,VarName)], TTAst),
1284		set_type_if_necessary(TTAst, Ast),
1285		!,
1286		example_bindings_to_ast_nodes(T, NT).
1287
1288		remove_prime(b(identifier(VarName),Type,Info), b(identifier(UnPrimed),Type,Info)) :-
1289		!,
1290		remove_prime(VarName, UnPrimed).
1291		remove_prime(VarName, UnPrimed) :-
1292		atom_concat(UnPrimed, '\'', VarName),
1293		!.
1294		remove_prime(VarName, VarName).
1295
1296		% we have to set the types of untyped ast nodes like empty sets
1297		% TO DO: correctly set the type environment for the type checker in btype/7 and get rid of set_type_if_necessary/2
1298		set_type_if_necessary(b(Node,Type,Info), b(TypedNode,GroundType,Info)) :-
1299		Node \= identifier(_),
1300		Node \= couple(_,_),
1301		untyped(Type),
1302		b_get_machinevars_with_operation_params(MachineVars),
1303		member(synthesis(machinevar,VarName), Info),
1304		member(b(identifier(VarName),GroundType,_), MachineVars),
1305		set_nested_types_if_necessary(Node, GroundType, TypedNode).
1306		% or couples refering to enumerated machine sets
1307		set_type_if_necessary(b(couple(Key,Value),Type,Info), b(couple(TypedKey,TypedValue),couple(KeyType,ValueType),Info)) :-
1308		untyped(Type),
1309		!,
1310		set_type_if_necessary(Key, TypedKey),
1311		set_type_if_necessary(Value, TypedValue),
1312		get_texpr_type(TypedKey, KeyType),
1313		get_texpr_type(TypedValue, ValueType).
1314		% or elements of enumerated machine sets
1315		set_type_if_necessary(b(identifier(IdName),Type,Info), b(identifier(IdName),GroundType,Info)) :-
1316		untyped(Type),
1317		!,
1318		b_get_machine_enumerated_sets_with_names(SetNamesTuples),
1319		% get the ast node of the enumerated set the identifier belongs to
1320		findall(SetNode, ( member((SetNode,ElmNames), SetNamesTuples),
1321		member(IdName, ElmNames)
1322		), [SetNode]),
1323		SetNode = b(_,set(GroundType),_).
1324		set_type_if_necessary(b(Node,Type,Info), b(Node,Type,Info)).
1325
1326		% set the type of the elements of sets or sequences
1327		set_nested_types_if_necessary(Node, set(InnerType), TypedNode) :-
1328		Node =.. [SetOrSeq,Elements],
1329		( SetOrSeq = set_extension
1330		; SetOrSeq = sequence_extension
1331		),
1332		maplist(set_explicit_type_if_necessary(InnerType), Elements, TypedElements),
1333		TypedNode =.. [SetOrSeq,TypedElements].
1334		set_nested_types_if_necessary(Node, _, Node).
1335
1336		set_explicit_type_if_necessary(InnerType, b(Node,Type,Info), TypedNode) :-
1337		untyped(Type),
1338		!,
1339		TypedNode = b(Node,InnerType,Info).
1340		set_explicit_type_if_necessary(_, Ast, Ast).
1341
1342		b_get_machine_enumerated_sets_with_names(SetNamesTuples) :-
1343		findall((SetName,SetNode), b_get_machine_set(SetName, SetNode), NameNodeTuples),
1344		findall((SetName,ElmNames), b_get_named_machine_set(SetName, ElmNames), NameElmsTuples),
1345		findall((SetNode,ElmNames), ( member((SetName,SetNode), NameNodeTuples),
1346		member((SetName,ElmNames), NameElmsTuples)
1347		), SetNamesTuples).
1348
1349		untyped(Type) :-
1350		var(Type).
1351		untyped(set(Type)) :-
1352		untyped(Type).
1353		untyped(set(couple(Key,Value))) :-
1354		( untyped(Key)
1355		; untyped(Value)
1356		).
1357		untyped(seq(Type)) :-
1358		untyped(Type).
1359		untyped(seq(couple(Key,Value))) :-
1360		( untyped(Key)
1361		; untyped(Value)
1362		).
1363		% ProB sometimes sets the type of empty sets to set(any)
1364		% TO DO: check this
1365		untyped(any).
1366
1367		% Zip two lists of the same size, i.e., create tuples of elements having the same index respectively.
1368		zip(L1, L2, Zipped) :-
1369		zip_aux(L1, L2, [], Zipped).
1370		zip_aux([], [], Acc, Acc).
1371		zip_aux([Elm1|T1], [Elm2|T2], Acc, Zipped) :-
1372		zip_aux(T1, T2, [(Elm1,Elm2)|Acc], Zipped).
1373
1374		% Used in b_synthesis
1375		% An operation satisfies the provided behavior, and thus, we do not have to synthesize anything.
1376		prepare_solution(_AdaptMachineCode, _, _, operation_satisfied(OperationName), operation_satisfied(OperationName), none).
1377		% Synthesis returned a distinguishing state or transition. The machine code is not changed.
1378		prepare_solution(_AdaptMachineCode, _, _, state(State), none, state(TranslatedState)) :-
1379		!,
1380		maplist(translate_example_ast, State, TranslatedState).
1381		prepare_solution(_AdaptMachineCode, _, _, transition(Input,Output), none, transition(TranslatedInput,TranslatedOutput)) :-
1382		!,
1383		maplist(translate_example_ast, Input, TranslatedInput),
1384		maplist(translate_example_ast, Output, TranslatedOutput).
1385		% Succeeded synthesizing a program fitting the desired behavior. Apply the solution to the machine code.
1386		prepare_solution(yes, Operation, SynthesisType, Synthesized, NewMachineAtom, distinguishing(none)) :-
1387		full_b_machine(Machine),
1388		apply_solution_to_machine_and_type_invariant(Machine, Operation, SynthesisType, Synthesized, NewMachineAst),
1389		translate_machine(NewMachineAst, Codes, _),
1390		atom_codes(NewMachineAtom, Codes).
1391		prepare_solution(no, _, _, Synthesized, Solution, Distinguishing) :-
1392		!,
1393		translate_subst_or_bexpr(Synthesized, PrettyPrint),
1394		Solution = (Synthesized, PrettyPrint),
1395		Distinguishing = distinguishing(none).
1396
1397		% Return a tuple of machine variable name and value for a given state's value ast.
1398		translate_example_ast(ExampleAst, (MachineVarName,TranslatedValue)) :-
1399		translate_bexpression(ExampleAst, TranslatedValue),
1400		get_varname_from_node_info(ExampleAst, MachineVarName).
1401
1402		% We derive several operations when implicitly synthesizing if-statements which we here apply to the machine code.
1403		adapt_machine_code_for_operations(Operations, NewMachineAtom) :-
1404		full_b_machine(Machine),
1405		adapt_machine_code_for_operations_aux(Operations, Machine, TempNewMachine),
1406		% type invariants which may have been optimized by ProB
1407		b_get_invariant_from_machine(Invariant),
1408		apply_solution_to_machine_and_type_invariant(TempNewMachine, _, invariant, Invariant, NewMachineAst),
1409		translate_machine(NewMachineAst, Codes, _),
1410		atom_codes(NewMachineAtom, Codes).
1411
1412		adapt_machine_code_for_operations_aux([], MachineCode, MachineCode).
1413		adapt_machine_code_for_operations_aux([Operation|T], MachineCode, NewMachineCode) :-
1414		apply_solution_to_machine(MachineCode, _, action, Operation, TempNewMachine),
1415		adapt_machine_code_for_operations_aux(T, TempNewMachine, NewMachineCode).
1416
1417		apply_solution_to_machine_and_type_invariant(Machine, Operation, Type, Synthesized, NewMachine) :-
1418		Type \= invariant,
1419		apply_solution_to_machine(Machine, Operation, Type, Synthesized, TempNewMachine),
1420		% the invariant has not been changed but typing predicates may be removed by the solver optimization,
1421		% therefore, we add typing predicates for each machine variable at the beginning of the invariant
1422		b_get_invariant_from_machine(Invariant),
1423		apply_solution_to_machine(TempNewMachine, _, invariant, Invariant, NewMachine).
1424		apply_solution_to_machine_and_type_invariant(Machine, Operation, invariant, SynthesizedInvariant, NewMachine) :-
1425		apply_solution_to_machine(Machine, Operation, invariant, SynthesizedInvariant, NewMachine).
1426
1427		apply_solution_to_machine(Machine, _, _, none, Machine).
1428		apply_solution_to_machine(machine(MachineName,Content), _, action, Synthesized, NewMachine) :-
1429		member(operation_bodies/OperationBodies, Content),
1430		subtract(Content, [operation_bodies/_], TempContent),
1431		apply_solution_to_machine_aux(action, OperationBodies, Synthesized, NewOperationBodies),
1432		append(TempContent, [operation_bodies/NewOperationBodies], NewContent),
1433		NewMachine = machine(MachineName,NewContent).
1434		apply_solution_to_machine(machine(MachineName,Content), Operation, guard, Synthesized, NewMachine) :-
1435		member(operation_bodies/OperationBodies, Content),
1436		subtract(Content, [operation_bodies/_], TempContent),
1437		apply_solution_to_machine_aux(guard, Operation, Synthesized, OperationBodies, NewOperationBodies),
1438		append(TempContent, [operation_bodies/NewOperationBodies], NewContent),
1439		NewMachine = machine(MachineName,NewContent).
1440		apply_solution_to_machine(machine(MachineName,Content), _, invariant, Synthesized, NewMachine) :-
1441		subtract(Content, [invariant/_], TempContent),
1442		conjunction_to_list(Synthesized, SynthesizedList),
1443		% split synthesized code from previous invariants that have been valid beforehand
1444		findall(SynthesizedCode, ( member(SynthesizedCode, SynthesizedList),
1445		get_texpr_info(SynthesizedCode, Info),
1446		member(synthesized_code, Info)
1447		), SynthesizedCodeList),
1448		conjunct_predicates(SynthesizedCodeList, TempSynthesizedCode),
1449		find_typed_identifier_uses(TempSynthesizedCode, UsedVars),
1450		% create typing invariants only for variables that are involved in the synthesized code, the other typing invariants have already been conjuncted in ValidInvariants
1451		% we hereby want to avoid redundancy and conflicts in typing invariants, like the valid invariant has been i : NATURAL but generate_typing_predicates creates i : INTEGER afterwards
1452		% whilst i has not even been affected by the invariant violation
1453		b_get_typing_predicate_for_vars(UsedVars, TypingPredicate),
1454		conjunct_predicates([TypingPredicate,Synthesized], TypedSynthesizedInvariant),
1455		add_invariant_to_machine_content(TempContent, TypedSynthesizedInvariant, NewContent),
1456		NewMachine = machine(MachineName,NewContent).
1457
1458		% Existing operations are replaced by the synthesized ones.
1459		apply_solution_to_machine_aux(action, OperationBodies, Synthesized, NewOperationBodies) :-
1460		is_list(Synthesized),
1461		maplist(get_name_from_operation_ast, Synthesized, OperationNames),
1462		remove_operations_from_list(OperationBodies, OperationNames, [], UninvoledOperations),
1463		append(Synthesized, UninvoledOperations, NewOperationBodies).
1464		apply_solution_to_machine_aux(action, OperationBodies, Synthesized, [Synthesized|UninvoledOperations]) :-
1465		\+ is_list(Synthesized),
1466		get_name_from_operation_ast(Synthesized, OperationName),
1467		remove_operations_from_list(OperationBodies, [OperationName], [], UninvoledOperations).
1468
1469		% Given a list of operation bodies, i.e. operation/4 ASTs, remove those whose name is in OperationNames.
1470		remove_operations_from_list([], _, Acc, Acc).
1471		remove_operations_from_list([OperationBody|T], OperationNames, Acc, NewOperationBodies) :-
1472		get_name_from_operation_ast(OperationBody, OperationName),
1473		\+ member(OperationName, OperationNames),
1474		remove_operations_from_list(T, OperationNames, [OperationBody|Acc], NewOperationBodies).
1475		remove_operations_from_list([_|T], OperationNames, Acc, NewOperationBodies) :-
1476		remove_operations_from_list(T, OperationNames, Acc, NewOperationBodies).
1477
1478		apply_solution_to_machine_aux(guard, OperationName, Synthesized, [Operation|T], [NewOperation|T]) :-
1479		replace_precondition_if_operation_fits(OperationName, Operation, Synthesized, NewOperation),
1480		!.
1481		apply_solution_to_machine_aux(guard, OperationName, Synthesized, [Operation|T], [Operation|NT]) :-
1482		apply_solution_to_machine_aux(guard, OperationName, Synthesized, T, NT).
1483
1484		get_name_from_operation_ast(b(operation(ID,_,_,_),_,_), OperationName) :-
1485		ID = b(identifier(op(OperationName)),_,_).
1486
1487		% insert the synthesized invariant prior to the linking_invariant
1488		add_invariant_to_machine_content([linking_invariant/OperationBodies|T], Invariant, [invariant/Invariant,linking_invariant/OperationBodies|T]).
1489		add_invariant_to_machine_content([ContentType/Content|T], Invariant, [ContentType/Content|NewContent]) :-
1490		ContentType \= operation_bodies,
1491		add_invariant_to_machine_content(T, Invariant, NewContent).
1492
1493		replace_precondition_if_operation_fits(OperationName, Operation, Synthesized, NewOperation) :-
1494		Operation = b(Node,Type,Info),
1495		Node = operation(OperationNameId,X,Y,Body),
1496		get_varname_from_id_node(OperationNameId, IdName),
1497		IdName = op(OperationName), % operation fits
1498		replace_precondition_if_operation_fits_aux(Body, Synthesized, NewBody),
1499		NewOperation = b(operation(OperationNameId,X,Y,NewBody),Type,Info).
1500		% Replace or create a new precondition if the given operation name is equal to the one of the operation.
1501		replace_precondition_if_operation_fits_aux(Body, Synthesized, NewBody) :-
1502		Body = b(precondition(_,Substitutions),subst,Info),
1503		!,
1504		NewBody = b(precondition(Synthesized,Substitutions),subst,Info).
1505		replace_precondition_if_operation_fits_aux(Body, Synthesized, NewBody) :-
1506		Body = b(Substitutions,subst,Info),
1507		NewBody = b(precondition(Synthesized,Substitutions),subst,Info).
1508
1509		replace_precondition_of_operation(Operation, none, FinalOperation) :-
1510		!,
1511		FinalOperation = Operation.
1512		replace_precondition_of_operation(Operation, Precondition, FinalOperation) :-
1513		Operation = b(operation(OperationName,Res,Par,Body),subst,_),
1514		Body = b(precondition(_,Subst),_,_),
1515		!,
1516		FinalOperation = b(operation(OperationName,Res,Par,b(precondition(Precondition,Subst),subst,[])),subst,[]).
1517		replace_precondition_of_operation(Operation, Precondition, FinalOperation) :-
1518		Operation = b(operation(OperationName,Res,Par,Subst),subst,_),
1519		FinalOperation = b(operation(OperationName,Res,Par,b(precondition(Precondition,Subst),subst,[])),subst,[]).
1520
1521		% The Java UI provides tuples of input and output examples.
1522		split_input_output_tuples(InputOutputTupleList, InputList, OutputList) :-
1523		split_input_output_tuples(InputOutputTupleList, [], [], InputList, OutputList).
1524		split_input_output_tuples([], InputListAcc, OutputListAcc, InputListAcc, OutputListAcc).
1525		split_input_output_tuples([(Input,Output)|T], InputListAcc, OutputListAcc, InputList, OutputList) :-
1526		maplist(variable_parsedvalue_tuple_to_ast, Input, InputAsts),
1527		maplist(variable_parsedvalue_tuple_to_ast, Output, OutputAsts),
1528		accumulate_input_output_if_non_empty(InputAsts, InputListAcc, NewInputListAcc),
1529		accumulate_input_output_if_non_empty(OutputAsts, OutputListAcc, NewOutputListAcc),
1530		split_input_output_tuples(T, NewInputListAcc, NewOutputListAcc, InputList, OutputList).
1531
1532		accumulate_input_output_if_non_empty([], Acc, Acc).
1533		accumulate_input_output_if_non_empty(Asts, Acc, [Asts|Acc]) :-
1534		Asts \= [].
1535
1536		% Given a tuple of variable name and parsed term. Create the ast using the typechecker and
1537		% add synthesis/2 term to the node's info describing the corresponding machine variable.
1538		variable_parsedvalue_tuple_to_ast((VarName,ParsedValue), TypedAst) :-
1539		%% TO DO: use type_check_in_machine_context/2
1540		btype(bsynthesis, ParsedValue, openenv(_,env_empty), _, TempAst, tr(_,_,_,_), tr(_,_,_,_)),
1541		add_texpr_infos(TempAst, [synthesis(machinevar,VarName)], TempAst2),
1542		remove_set_of_couple_type(TempAst2, TempAst3),
1543		set_type_if_necessary(TempAst3, TempAst4),
1544		!,
1545		get_texpr_type(TempAst4, Type),
1546		add_texpr_infos(TempAst4, [synthesis(type,Type)], TypedAst).
1547
1548		% Remove set(couple(_,_)) type since a sequence with size < 3 may be interpreted as a set of couples although it should be a seq(_).
1549		% The type is added afterwards according to the corresponding machine variable.
1550		remove_set_of_couple_type(b(Node,Type,Info), b(Node,_,Info)) :-
1551		Type == set(couple(_,_)),
1552		!.
1553		remove_set_of_couple_type(AST, AST).
1554
1555
1556		keep_asserted_initial_examples(Input, Output, OldInput, OldOutput, NewInput, NewOutput) :-
1557		keep_asserted_initial_states(Input, OldInput, NewInput),
1558		keep_asserted_initial_states(Output, OldOutput, NewOutput).
1559		keep_asserted_initial_states([], _, []).
1560		keep_asserted_initial_states([State|T], OldStates, [NewState|NT]) :-
1561		contains_equivalent_state(State, OldStates, EquivalentState),
1562		!,
1563		NewState = EquivalentState,
1564		keep_asserted_initial_states(T, OldStates, NT).
1565		keep_asserted_initial_states([State|T], OldStates, [State|NT]) :-
1566		keep_asserted_initial_states(T, OldStates, NT).
1567
1568		get_operation_params_from_ids(TypedIdentifiers, Params) :-
1569		get_operation_params_from_ids(TypedIdentifiers, [], Params).
1570		get_operation_params_from_ids([], Acc, Acc).
1571		get_operation_params_from_ids([TypedIdentifier|T], Acc, Params) :-
1572		get_texpr_info(TypedIdentifier, Info),
1573		( ( member(synthesis(ParamType,_), Info),
1574		( ParamType = param_single
1575		; ParamType = param_set
1576		)
1577		)
1578		; member(introduced_by(operation), Info)
1579		),
1580		TypedIdentifier = b(Node,Type,_),
1581		\+ member(b(Node,Type,_), Acc),
1582		!,
1583		get_operation_params_from_ids(T, [TypedIdentifier|Acc], Params).
1584		get_operation_params_from_ids([_|T], Acc, Params) :-
1585		get_operation_params_from_ids(T, Acc, Params).
1586
1587		set_operation_params_domain(Params, Membership) :-
1588		set_operation_params_domain(Params, [], MembershipList),
1589		conjunct_predicates(MembershipList, Membership).
1590
1591		set_operation_params_domain([], Acc, Acc).
1592		set_operation_params_domain([Param|T], Acc, MembershipList) :-
1593		get_texpr_info(Param, ParamInfo),
1594		( member(synthesis(type,set(global(IndependentType))), ParamInfo)
1595		; Param = b(_,global(IndependentType),_)
1596		),
1597		b_get_named_machine_set(IndependentType, SetAst, _),
1598		set_operation_params_domain(T, [b(member(Param,SetAst),pred,[])|Acc], MembershipList).
1599
1600		finalize_synthesized_action(_, none, none).
1601		finalize_synthesized_action(OperationName, b(precondition(PreCondition,Substitutions),subst,[]),
1602		b(operation(OpNameId,_,Params,b(precondition(NewPreCondition,UnprimedSubstitutions),subst,[])),subst,[])) :-
1603		OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
1604		find_typed_identifier_uses_with_info(Substitutions, TypedIdentifiers),
1605		get_operation_params_from_ids(TypedIdentifiers, Params),
1606		Params \= [],
1607		!,
1608		set_operation_params_domain(Params, ParamTypeDefsPred),
1609		conjunct_predicates([ParamTypeDefsPred,PreCondition], NewPreCondition),
1610		prime_or_unprime_variables_in_ast(unprime, [], Substitutions, UnprimedSubstitutions).
1611		finalize_synthesized_action(OperationName, b(precondition(PreCondition,Substitutions),subst,[]),
1612		b(operation(OpNameId,_,_,b(precondition(PreCondition,UnprimedSubstitutions),subst,[])),subst,[])) :-
1613		OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
1614		prime_or_unprime_variables_in_ast(unprime, [], Substitutions, UnprimedSubstitutions).
1615		finalize_synthesized_action(OperationName, Action, b(operation(OpNameId,_,Params,b(precondition(ParamTypeDefsPred,UnprimedAction),subst,[])),subst,[])) :-
1616		OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
1617		find_typed_identifier_uses_with_info(Action, TypedIdentifiers),
1618		get_operation_params_from_ids(TypedIdentifiers, Params),
1619		Params \= [],
1620		!,
1621		set_operation_params_domain(Params, ParamTypeDefsPred),
1622		prime_or_unprime_variables_in_ast(unprime, [], Action, UnprimedAction).
1623		finalize_synthesized_action(OperationName, Action, b(operation(OpNameId,_,_,UnprimedAction),subst,[])) :-
1624		OpNameId = b(identifier(op(OperationName)),op([],[]),[]),
1625		prime_or_unprime_variables_in_ast(unprime, [], Action, UnprimedAction).
1626
1627		% Synthesizing a guard for an action simultaneously can fail. We memorize distinguishing transitions
1628		% so even without a guard we won't find a distinguishing transitions twice. However,
1629		% finding a new distingushing transition that leads to synthesizing a guard simultaneously may
1630		% succeed with the new example later on (previous distinguishing states are also memorized and will be reused).
1631		prepare_synthesized_guards_for_action(Guards, Guards) :-
1632		is_ast(Guards).
1633		prepare_synthesized_guards_for_action(_, any).
1634
1635
1636		% Get all the location vars from a list of operators. The result is a map with entries like
1637		% Operator:ListOfLocationVars. Just one iteration of the list of location variables for all operators.
1638		% get_all_location_vars_for_operators(Operators,LocationVars,OperatorLVarsMap) :-
1639		% findall(Op:[],member(Op,Operators),EmptyAcc) ,
1640		% get_all_location_vars_for_operators_aux(LocationVars,EmptyAcc,OperatorLVarsMap).
1641		% get_all_location_vars_for_operators_aux([],Acc,Acc).
1642		% get_all_location_vars_for_operators_aux([LocationVar|T],Acc,OperatorLVarsMap) :-
1643		% LocationVar = b(_,_,Info) ,
1644		% member(synthesis(ComponentName,LocationType),Info) ,
1645		% member(LocationType,[left_input,right_input,output]) ,
1646		% delete_numbers_from_atom(ComponentName,Operator) ,
1647		% accumulate_locationvar_for_operator(LocationVar,Operator,Acc,NewAcc) ,
1648		% get_all_location_vars_for_operators_aux(T,NewAcc,OperatorLVarsMap).
1649		% get_all_location_vars_for_operators_aux([_|T],Acc,OperatorLVarsMap) :-
1650		% get_all_location_vars_for_operators_aux(T,Acc,OperatorLVarsMap).
1651
1652		% If the operator the location variable refers to is one that we search for, we accumulate the variable respectively.
1653		% accumulate_locationvar_for_operator(LocationVar,Operator,Acc,NewAcc) :-
1654		% member(Operator:OperatorLocationVars,Acc) ,
1655		% delete(Acc,Operator:_,TempAcc) ,
1656		% NewAcc = [Operator:[LocationVar|OperatorLocationVars]|TempAcc].
1657		% Otherwise skip the location variable.
1658		% accumulate_locationvar_for_operator(_,Operator,Acc,Acc) :-
1659		% \+member(Operator:_,Acc).
1660
1661		% Adjust the distinguishing state to the current variables (synthesis type is guard or invariant).
1662		% :- spec_pre(adjust_distinguishing_state_binding/3,[list(ast),solution_bindings,var]).
1663		% :- spec_invariant(adjust_distinguishing_state_binding/3,[list(ast),solution_bindings,solution_bindings]).
1664		% :- spec_post(adjust_distinguishing_state_binding/3,[list(ast),solution_bindings,var],
1665		% [list(ast),solution_bindings,solution_bindings]).
1666		% adjust_distinguishing_state_binding(CurrentVars,Distinguishing,Distinguishing) :-
1667		% length(CurrentVars,VarAmount) ,
1668		% length(Distinguishing,VarAmount).
1669		% Shrink distinguishing state.
1670		% adjust_distinguishing_state_binding(CurrentVars,Distinguishing,ShrunkenInput) :-
1671		% length(CurrentVars,VarAmount) ,
1672		% length(Distinguishing,DistAmount) ,
1673		% VarAmount < DistAmount ,
1674		% findall(Binding,(member(Binding,Distinguishing) , Binding = binding(VarName,_,_) ,
1675		% member(b(identifier(VarName),_,_),CurrentVars)),ShrunkenInput).
1676		% Expand distinguishing state.
1677		% adjust_distinguishing_state_binding(CurrentVars,Distinguishing,ShrunkenInput) :-
1678		% length(CurrentVars,VarAmount) ,
1679		% length(Distinguishing,DistAmount) ,
1680		% VarAmount > DistAmount ,
1681		% findall(Binding,(member(b(identifier(VarName),_,_),CurrentVars) ,
1682		% \+member(Binding,Distinguishing) , Binding = binding(VarName,_,_)),ShrunkenInput).