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