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