1 | | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | |
6 | | :- module(b_trace_checking, [tcltk_check_state_sequence_from_file/1, |
7 | | tcltk_check_sequence_from_file/3, |
8 | | check_default_trace_for_specfile/1, get_default_trace_file/2, |
9 | | print_trace_as_fdr_check/0, |
10 | | tcltk_save_history_as_trace_file/2, %print_trace_for_replay/1, |
11 | | perform_initialisation/0, |
12 | | find_successor_state/4 |
13 | | ]). |
14 | | |
15 | | :- use_module(library(lists)). |
16 | | |
17 | | :- use_module(tools). |
18 | | :- use_module(module_information,[module_info/2]). |
19 | | :- module_info(group,testing). |
20 | | :- module_info(description,'Replay saved traces; raise error if not possible. Used in regression testing.'). |
21 | | |
22 | | :- use_module(bsyntaxtree, [get_texpr_type/2, conjunct_predicates/2]). |
23 | | :- use_module(bmachine,[b_machine_name/1, b_is_operation_name/1, b_get_machine_operation_typed_parameters/2]). |
24 | | :- use_module(b_global_sets,[lookup_global_constant/2]). |
25 | | :- use_module(error_manager). |
26 | | :- use_module(debug). |
27 | | :- use_module(preferences,[get_preference/2,preference/2,temporary_set_preference/3,reset_temporary_preference/2]). |
28 | | :- use_module(specfile,[b_mode/0, csp_mode/0, get_operation_name/2, get_operation_return_values_and_arguments/3]). |
29 | | :- use_module(translate,[translate_event/2]). |
30 | | :- use_module(state_space,[current_options/1, current_state_id/1, current_expression/2, |
31 | | max_reached_for_node/1, not_all_transitions_added/1]). |
32 | | :- use_module(junit_tests). |
33 | | :- use_module(tools_printing,[print_red/1, print_green/1]). |
34 | | % -------------------------------- |
35 | | |
36 | | % replay trace with state predicates; one predicate per line |
37 | | |
38 | | % b_trace_checking:tcltk_check_state_sequence_from_file('~/Desktop/scheduler6.ptrace'). |
39 | | |
40 | | tcltk_check_state_sequence_from_file(File) :- |
41 | | open(File,read,Stream,[encoding('UTF-8')]), |
42 | | state_space:current_state_id(ID), |
43 | | format(user_output,'Opened predicate list file: ~w~n Starting from state ~w.~n',[File,ID]), |
44 | | call_cleanup(tcltk_check_state_sequence_from_file_aux(File,0,Stream,ID), |
45 | | (format(user_output,'Finished processing list file: ~w~n',[File]), |
46 | | close(Stream))). |
47 | | |
48 | | tcltk_check_state_sequence_from_file_aux(File,LineNr,Stream,ID) :- read_line(Stream,Codes), |
49 | | Codes \= end_of_file, |
50 | | L1 is LineNr+1, |
51 | | !, %print(codes(Codes)),nl, |
52 | | process_line(File,L1,Stream,Codes,ID). |
53 | | tcltk_check_state_sequence_from_file_aux(_,LineNr,_,_) :- printsilent('reached EOF at line: '), printsilent(LineNr),nls. |
54 | | |
55 | | :- use_module(bmachine,[b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2, |
56 | | b_type_check_raw_expr/4]). |
57 | | :- use_module(translate_keywords). |
58 | | |
59 | | % TO DO: also allow operation names, parameters to be specified? |
60 | | process_line(File,LineNr,Stream,Codes,ID) :- |
61 | | % insert newlines to ensure error message correct: |
62 | | insert_nl_prefix(LineNr,Codes,CodesNL), |
63 | | b_parse_wo_type_machine_predicate_from_codes_to_raw_expr(CodesNL,Parsed), |
64 | | % in case we did translate keywords (e.g., in Event-B mode); translate them back: |
65 | | translate_keywords:raw_backtranslate_keyword_ids(Parsed,Parsed2), |
66 | | % now type check the raw expression: |
67 | | b_type_check_raw_expr(Parsed2,[prob_ids(all),variables],Pred,closed), |
68 | | % bmachine:b_parse_machine_predicate_from_codes(CodesNL,[prob_ids(all),variables],Pred), |
69 | | !, |
70 | | format('Line ~w : ~w --?--> ',[LineNr,ID]),translate:print_bexpr(Pred),nl, |
71 | | find_successor_state(ID,Pred,SuccID,LineNr), |
72 | | tcltk_check_state_sequence_from_file_aux(File,LineNr,Stream,SuccID). |
73 | | process_line(_File,LineNr,_Stream,Codes,_ID) :- |
74 | | atom_codes(Atom,Codes), |
75 | | add_error(tcltk_check_state_sequence_from_file,'Could not parse state predicate: ',Atom), |
76 | | add_error(tcltk_check_state_sequence_from_file,'Line: ',LineNr), |
77 | | %add_error(tcltk_check_state_sequence_from_file,'File: ',File), |
78 | | fail. |
79 | | |
80 | | insert_nl_prefix(N,Acc,Acc) :- N =< 1,!. |
81 | | insert_nl_prefix(N,Acc,[10,13|Res]) :- N1 is N-1, insert_nl_prefix(N1,Acc,Res). |
82 | | |
83 | | :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]). |
84 | | :- use_module(specfile,[expand_const_and_vars_to_full_store/2]). |
85 | | :- use_module(state_space,[visited_expression/2, |
86 | | max_reached_for_node/1, max_reached_or_timeout_for_node/1, time_out_for_node/1]). |
87 | | :- use_module(library(codesio),[format_to_codes/3]). |
88 | | :- use_module(eventhandling, [announce_event/1]). |
89 | | |
90 | | find_successor_state(_ID,Pred,NewID,_) :- |
91 | | % transition(ID,ActionOpAsTerm,OpID,SuccID), |
92 | | user:tcltk_get_options(_), |
93 | | current_options(Options), % print(Options),nl, |
94 | | member( (_,Action,ActionOpAsTerm,NewID), Options), |
95 | | state_space:visited_expression(NewID,State), |
96 | | expand_const_and_vars_to_full_store(State,EState), |
97 | | % print(try(NewID,State)),nl, |
98 | | add_prob_deferred_set_elements_to_store(EState,DEState,all), |
99 | | announce_event(start_solving), |
100 | | b_interpreter:b_test_boolean_expression_wf(Pred,[],DEState), % deferred |
101 | | announce_event(end_solving), |
102 | | debug_println(19,successor_found(NewID)), |
103 | | print(' --> '),my_print_event(ActionOpAsTerm,_),nl,nl, |
104 | | my_perform_action_as_string(Action,ActionOpAsTerm,NewID), |
105 | | !. |
106 | | find_successor_state(ID,Pred,NewID,_LineNr) :- |
107 | | max_reached_or_timeout_for_node(ID), % we have not computed all options |
108 | | get_op_name_for_state(ID,OpName), print(try_providing_custom_predicate(OpName)),nl, |
109 | | user:tcltk_add_user_executed_operation_typed(OpName,Pred,NewID), % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine |
110 | | (silent_mode(on) -> true |
111 | | ; print_green(successor_found(NewID)),nl, |
112 | | print(' --> '),print(OpName),nl), |
113 | | !. |
114 | | find_successor_state(ID,Pred,_,LineNr) :- |
115 | | % we could try and execute operation by predicate here; in case max_reached_for_node(ID) or time_out_for_node(ID) |
116 | | format('State ID = ~w; line number = ~w~n',[ID,LineNr]), |
117 | | (max_reached_for_node(ID) |
118 | | -> format_to_codes('Try increasing the MAX_OPERATIONS preference. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes) |
119 | | ; time_out_for_node(ID) -> format_to_codes('TIME-OUT occurred. No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes) |
120 | | ; format_to_codes('No successor found satisfying predicate at step ~w of replay: ',[LineNr],Codes) |
121 | | ), |
122 | | atom_codes(Msg,Codes), |
123 | | translate:translate_bexpression(Pred,TP), |
124 | | add_error(tcltk_check_state_sequence_from_file,Msg,TP), |
125 | | fail. |
126 | | |
127 | | :- use_module(bmachine,[b_machine_has_constants_or_properties/0]). |
128 | | get_op_name_for_state(root,OP) :- !, |
129 | | (b_machine_has_constants_or_properties -> OP='$setup_constants' ; OP='$initialise_machine'). |
130 | | get_op_name_for_state(ID,'$initialise_machine') :- |
131 | | visited_expression(ID,concrete_constants(_)),!. |
132 | | %get_op_name_for_state(ID,OpName) :- bmachine:b_top_level_operation(OpName). % not supported yet |
133 | | |
134 | | % -------------------------------- |
135 | | |
136 | | check_default_trace_for_specfile(File) :- get_default_trace_file(File,TFile), |
137 | | tcltk_check_sequence_from_file(prolog,TFile,backtrack). |
138 | | |
139 | | get_default_trace_file(File,TraceFile) :- |
140 | | split_filename(File,FN,_Ext), |
141 | | string_concatenate(FN,'.trace',TraceFile). |
142 | | |
143 | | :- use_module(tools_printing,[print_error/1]). |
144 | | tcltk_check_sequence_from_file(Style,File,deterministic_trace_replay) :- !, |
145 | | temporary_set_preference(deterministic_trace_replay,true,CHNG), |
146 | | format('Performing deterministic replay (lower memory usage, but no backtracking in case replay fails) for file: ~w~n',[File]), |
147 | | (tcltk_check_sequence_from_file2(Style,File) |
148 | | -> reset_temporary_preference(deterministic_trace_replay,CHNG) |
149 | | ; reset_temporary_preference(deterministic_trace_replay,CHNG)). |
150 | | tcltk_check_sequence_from_file(Style,File,_DetOrBacktrack) :- |
151 | | tcltk_check_sequence_from_file2(Style,File). |
152 | | |
153 | | tcltk_check_sequence_from_file2(Style,File) :- |
154 | | read_trace_file(Style,File,MachineName,Trace), |
155 | | length(Trace,Len), |
156 | ? | (b_mode -> b_machine_name(OurName) ; true), |
157 | ? | ((OurName=MachineName |
158 | | ; MachineName = 'dummy(uses)') % old trace files have these |
159 | | -> printsilent_message('Checking file for machine: '), printsilent_message(OurName) |
160 | | ; print_error('### Trace File has been generated for different machine: '), |
161 | | print_error(MachineName), |
162 | | print_error('### Our machine: '), print_error(OurName) |
163 | | ), |
164 | | formatsilent('Starting trace check of length ~w~n',[Len]), |
165 | | statistics(walltime,[Time1,_]), |
166 | ? | (perform_sequence_of_operations(Trace,0) |
167 | | -> nls,print_green('Trace checking successful !'),nl |
168 | | ; nls, |
169 | | add_error(trace_checking_fails,'Trace Checking was not successful: ',(File,MachineName)) |
170 | | %% ,throw(trace_checking_failed(MachineName)) % comment in if you want to stop immediately upon such an error |
171 | | ), |
172 | | statistics(walltime,[Time2,_]), Time is Time2-Time1, |
173 | | formatsilent('Walltime: ~w ms~n',[Time]), |
174 | | (csp_mode -> print_trace_as_fdr_check ; true), |
175 | | |
176 | ? | (junit_mode(_) -> (get_error(trace_checking,Errors) -> V=error([Errors]) |
177 | | ; otherwise -> V=pass), |
178 | | create_and_print_junit_result(File,'Trace_checking', MachineName, Time, V) |
179 | | ; otherwise -> true). |
180 | | |
181 | | :- use_module(json,[json_parse_file/2]). |
182 | | read_trace_file(prolog,File,MachineName,Trace) :- |
183 | | formatsilent('% Opening trace file: ~w~n',[File]), |
184 | | my_see(File), |
185 | | parse_trace_file(MachineName,Trace),!, |
186 | | seen. |
187 | | read_trace_file(json,File,MachineName,Trace) :- |
188 | | MachineName = 'dummy(uses)', % name not stored in JSON files |
189 | | json_parse_file(File,Term), |
190 | | !, |
191 | | (translate_json_term(Term,Trace) -> true |
192 | | ; add_error(trace_checking_fails,'Could not translate JSON transitionList: ',Term), |
193 | | %trace, translate_json_term(Term,Trace), |
194 | | Trace = []). |
195 | | read_trace_file(_,File,_,_) :- |
196 | | add_error(trace_checking_fails,'Could not read trace file: ',File),fail. |
197 | | |
198 | | my_see(File) :- on_exception(error(existence_error(_,_),_), |
199 | | see(File), add_error_fail(my_see,'File does not exist: ',File)). |
200 | | |
201 | | parse_trace_file(MName,Trace) :- |
202 | | safe_read(Term),!, |
203 | | (Term = end_of_file -> (Trace = []) |
204 | | ; (Term = machine(MName) |
205 | | -> Trace = T |
206 | | ; Trace = [Term|T] |
207 | | ), |
208 | | parse_trace_file(MName,T) |
209 | | ). |
210 | | |
211 | | safe_read(T) :- on_exception(E,read(T), |
212 | | ( add_error(safe_read,'Exception while reading input: ~w ~n',[E]), T=end_of_file)). |
213 | | |
214 | | |
215 | | translate_json_term(obj(ObjList),Trace) :- |
216 | | member(pair(transitionList,List),ObjList), |
217 | | !, |
218 | | temporary_set_preference(repl_cache_parsing,true,CHNG), |
219 | | maplist(translate_json_operation,List,Trace), |
220 | | reset_temporary_preference(repl_cache_parsing,CHNG). |
221 | | |
222 | | :- use_module(bsyntaxtree, [def_get_texpr_ids/2]). |
223 | | translate_json_operation(obj([pair(name,string(OpNameC))|RestPair]), Operation ) :- % new style |
224 | | %print(rest(RestPair)),nl, |
225 | | get_parameters(RestPair,Paras), |
226 | | !, |
227 | | atom_codes(OpName,OpNameC), print(json_translate_operation(OpName)),nl, |
228 | | (bmachine:b_get_machine_operation_parameter_names(OpName,OpParameterNames) -> true |
229 | | ; add_error(translate_json_operation,'Unknown operation: ',OpName),fail), |
230 | | maplist(translate_json_para,Paras,Bindings), |
231 | | order_paras(OpParameterNames,OpName,Bindings,BValues), % put the parameters into the order expected |
232 | | Op =.. [OpName|BValues], |
233 | | (bmachine:b_get_machine_operation(OpName,OpResults,_P,_Body,_OType,_OpPos), |
234 | | OpResults \= [] % we have return values |
235 | | -> Operation = '-->'(Op,BResValues), |
236 | | (member(pair(results,obj(ResParas)),RestPair) % we could provide this as an option: check results or not |
237 | | -> maplist(translate_json_para,ResParas,Bindings2), |
238 | | def_get_texpr_ids(OpResults,OpResultNames), |
239 | | order_paras(OpResultNames,OpName,Bindings2,BResValues) |
240 | | ; true) |
241 | | ; Operation = Op). %, print(translated(Op)),nl. |
242 | | |
243 | | get_parameters(RestPair,Paras) :- member(pair(params,obj(Paras)),RestPair),!. |
244 | | %get_parameters(RestPair,Paras) :- member(pair(parameters,Paras),RestPair), !. % old style |
245 | | get_parameters(_,[]). % e.g., for initialise machine |
246 | | |
247 | | order_paras([],OpName,Rest,[]) :- (Rest=[] -> true ; format('*** Unknown parameters for ~w: ~w~n',[OpName,Rest])). |
248 | | order_paras([ID|T],OpName,Env,[Val|TVal]) :- |
249 | | (select(bind(ID,Val),Env,Env2) -> order_paras(T,OpName,Env2,TVal) |
250 | | ; %add_error(translate_json_operation,'Parameter not specified: ',ID:Env), % keep Val a variable |
251 | | format('*** Parameter not specified for ~w: ~w~n',[OpName,ID]), |
252 | | order_paras(T,OpName,Env,TVal) |
253 | | ). |
254 | | |
255 | | % TO DO: using eval_strings is very ugly, use a better API predicate |
256 | | translate_json_para(pair(Name,string(C)),bind(Name,Value)) :- !, |
257 | | eval_strings:eval_expression_codes(C,_Res,_EnumWarning,_LocalState,_Typed,_TypeInfo), |
258 | | eval_strings:last_expression(_Type,_Expr,Value). |
259 | | %translate_json_para(string(C),Value) :- !, % old style |
260 | | % eval_strings:eval_expression_codes(C,_Res,_EnumWarning,_LocalState,_Typed,_TypeInfo), |
261 | | % eval_strings:last_expression(_Type,_Expr,Value). |
262 | | % %print(eval(S,Value)),nl. |
263 | | translate_json_para(Para,_) :- add_error(translate_json_para,'Unknown JSON para:',Para),fail. |
264 | | |
265 | | is_a_reset_operation(start_cspm_MAIN). |
266 | | is_a_reset_operation(start_csp_MAIN). |
267 | | is_a_reset_operation(Op) :- functor(Op,'$setup_constants',_). |
268 | | is_a_reset_operation(Op) :- functor(Op,'$initialise_machine',_), |
269 | ? | b_mode, \+ b_machine_has_constants_or_properties. |
270 | | |
271 | | :- use_module(bmachine, [b_machine_has_constants_or_properties/0]). |
272 | | perform_initialisation :- b_mode, b_machine_has_constants_or_properties,!, |
273 | | perform_sequence_of_operations(['$setup_constants','$initialise_machine'],0). |
274 | | perform_initialisation :- perform_sequence_of_operations(['$initialise_machine'],0). |
275 | | |
276 | | |
277 | | perform_sequence_of_operations([],Ident) :- |
278 | ? | (silent_mode(on) -> true ; ident(Ident),print('SUCCESS'),nl). |
279 | | perform_sequence_of_operations([Op|T],Ident) :- |
280 | ? | get_error_context(Context), |
281 | ? | state_space:current_state_id(ID),get_operation_name(Op,FOP), |
282 | ? | set_error_context(operation(FOP,ID)), |
283 | ? | perform_one_operation_in_sequence(Op,Ident), |
284 | ? | restore_error_context(Context), |
285 | ? | Ident1 is Ident+1, |
286 | ? | (get_preference(deterministic_trace_replay,true) -> ! ; true), |
287 | ? | perform_sequence_of_operations(T,Ident1). |
288 | | |
289 | | :- use_module(store,[lookup_value_for_existing_id/3]). |
290 | | |
291 | | perform_one_operation_in_sequence('$non_det_modified_vars'(ActionAsTerm,NonDetVars),Ident) :- !, |
292 | | current_expression(_CurID,State), |
293 | | current_options(Options), |
294 | | member( (_Id,Action,ActionOpAsTerm,NewID), Options), |
295 | | unify_action_as_term(ActionAsTerm,ActionOpAsTerm,State), |
296 | | %ident(Ident), format('checking non_det_modified_vars for ~w in ~w~n',[ActionAsTerm,NewID]),nl, |
297 | | check_non_det_vars(NewID,NonDetVars), |
298 | | !, |
299 | | perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident). |
300 | | perform_one_operation_in_sequence('$non_det_modified_vars'(Op,_),Ident) :- !, |
301 | | ident(Ident), format('ignoring non_det_modified_vars for ~w~n',[Op]), % TO DO: use constraint-based finding of successor |
302 | | perform_one_operation_in_sequence(Op,Ident). |
303 | | perform_one_operation_in_sequence('$check_value'(ID,VAL),Ident) :- !, |
304 | | ident(Ident), format('checking value of ~w ',[ID]), |
305 | | state_space:current_expression(_,State), |
306 | | expand_const_and_vars_to_full_store(State,EState), |
307 | | lookup_value_for_existing_id(ID,EState,StoredVal), |
308 | | translate:print_bvalue(StoredVal), |
309 | | (unify(StoredVal,VAL) -> print_green(' ok'),nl |
310 | | ; print_red(' failed'),nl, %print(StoredVal),nl, print(VAL),nl, |
311 | | fail). |
312 | | perform_one_operation_in_sequence(Op,Ident) :- |
313 | ? | (silent_mode(on) -> true |
314 | ? | ; ident(Ident),print('<- '),print(Ident), print(': '), my_print_event(Op,OpStr), |
315 | | print(' :: '), |
316 | | state_space:current_state_id(CurID), print(CurID),nl |
317 | | ), |
318 | ? | ((functor(Op,'$initialise_machine',_),\+(state_space:current_expression(_,concrete_constants(_))) |
319 | ? | ; is_a_reset_operation(Op)) |
320 | | -> user:tcltk_goto_state(reset,root), |
321 | | user:tcltk_get_options(_) |
322 | | ; true), |
323 | ? | convert_action(Op,COp), |
324 | ? | if(perform_single_operation(COp,Ident),true, |
325 | | (silent_mode(off), |
326 | | ident(Ident), print_red(' **** FAIL ****'),nl, |
327 | | %% trace, perform_single_operation(COp,Ident), |
328 | | fail)), |
329 | ? | (get_preference(deterministic_trace_replay,true) -> ! ; true), |
330 | ? | (silent_mode(on) -> true |
331 | ? | ; ident(Ident), print(' | '), print(Ident), print(': '), print(OpStr), |
332 | | %functor(Op,OpName,_), print(OpName), |
333 | | %((OpName = '-->', arg(1,Op,A1), functor(A1,RealOpName,_)) -> print(RealOpName) ; true), |
334 | | print_green(' success -->'), |
335 | | state_space:current_state_id(NewCurID), |
336 | | statistics(walltime,[Tot,Delta]), |
337 | | format('~w [~w (Delta ~w) ms]~n',[NewCurID,Tot,Delta]) |
338 | | ). |
339 | | |
340 | | my_print_event(Op,OpStrTA) :- |
341 | | temporary_set_preference(expand_avl_upto,4,CHNG), |
342 | | translate_event(Op,OpStr), |
343 | | truncate_atom(OpStr,100,OpStrTA), |
344 | | reset_temporary_preference(expand_avl_upto,CHNG), |
345 | | write(OpStrTA). |
346 | | |
347 | | /* convert global constants such as b with S={a,b,c} into fd(2,'S') */ |
348 | | convert_action(V,R) :- var(V),!,R=V. |
349 | | convert_action(io(V,Ch),R) :- !, strip_dots(V,SV),R=io(SV,Ch,_SRCSPAN). |
350 | | convert_action(io(V,Ch,_),R) :- !, strip_dots(V,SV),R=io(SV,Ch,_SRCSPAN). |
351 | | convert_action(tick(_SRCSPAN),R) :- !, R = tick(_). |
352 | | convert_action(X,Res) :- nonvar(X),X=..[F|Args],!, |
353 | | l_convert_term(Args,CArgs),Res=..[F|CArgs]. |
354 | | convert_action(X,X). |
355 | | |
356 | | convert_term(V,R) :- var(V),!,R=V. |
357 | | convert_term(closure(A,B,C),R) :- !, R=closure(A,B,C). % we may mess with identifiers; see test 1575 |
358 | | convert_term(term(bool(0)),R) :- !, R=pred_false /* bool_false */. |
359 | | convert_term(term(bool(1)),R) :- !, R=pred_true /* bool_true */. |
360 | | convert_term(bool_true,pred_true /* bool_true */) :- !. |
361 | | convert_term(bool_false,pred_false /* bool_false */) :- !. |
362 | | convert_term(string(S),R) :- !, R=string(S). |
363 | | convert_term(X,Representation) :- atomic(X), lookup_global_constant(X,Representation),!. |
364 | | convert_term(X,Res) :- nonvar(X),X=..[F|Args],!, |
365 | | l_convert_term(Args,CArgs),Res=..[F|CArgs]. |
366 | | convert_term(X,X). |
367 | | |
368 | | l_convert_term([],[]). |
369 | | l_convert_term([H|T],[CH|CT]) :- convert_term(H,CH), l_convert_term(T,CT). |
370 | | |
371 | | /* newer version of ProB no longer has dot() constructor */ |
372 | | strip_dots([],[]). |
373 | | strip_dots([H|T],[X|ST]) :- (H=dot(X) -> true ; X=H), strip_dots(T,ST). |
374 | | strip_dots(tail_in(X),[in(XR)]) :- |
375 | | (X=dotTuple(R) -> XR=tuple(R) ; XR = X). /* we also no longer use tail_in */ |
376 | | |
377 | | get_state(concrete_constants(X),R) :- !, R=X. |
378 | | get_state(const_and_vars(_,X),R) :- !, R=X. |
379 | | get_state(X,X). |
380 | | |
381 | | % check whether state NewID contains all the bindings in NonDetVars |
382 | | check_non_det_vars(NewID,NonDetVars) :- |
383 | | visited_expression(NewID,State), |
384 | | get_state(State,VarState), |
385 | | maplist(check_non_det_bind(VarState),NonDetVars). |
386 | | |
387 | | check_non_det_bind(State,bind(Var,Val)) :- member(bind(Var,StoredVal),State), unify(StoredVal,Val). |
388 | | |
389 | | :- use_module(state_space,[current_state_id/1, current_expression/2, visited_expression_id/1]). |
390 | | perform_single_operation('$jump'(TO,FROM),Ident) :- !, |
391 | | current_state_id(ID), |
392 | | print_red('Warning: trace file contains JUMP!'),nl, |
393 | | (ID=FROM -> true ; ident(Ident),format('Cannot perform jump from ~w (to ~w)~n',[FROM,TO])), |
394 | | (visited_expression_id(TO) -> user:tcltk_goto_state(jump,TO) |
395 | | ; add_error(trace_checking_fails,'State ID does not exist for jump:',TO),fail |
396 | | ). |
397 | | perform_single_operation(ActionAsTerm,Ident) :- |
398 | | % tools_printing:print_term_summary(perform_single_op(ActionAsTerm)), |
399 | ? | current_expression(_CurID,State), |
400 | ? | current_options(Options), |
401 | ? | ( if( ( member( (_Id,Action,ActionOpAsTerm,NewID), Options), |
402 | | unify_action_as_term(ActionAsTerm,ActionOpAsTerm,State)), |
403 | ? | perform_action_tclk(Action,ActionOpAsTerm,NewID,Ident), |
404 | ? | if(perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State), |
405 | ? | perform_action_tclk(Action,_AlternateActionOpAsTerm,NewID,Ident), |
406 | | perform_custom_operation_retry(ActionAsTerm,_NewID) |
407 | | ) |
408 | | |
409 | | ) |
410 | | ; |
411 | | single_operation_skip(ActionAsTerm,Ident) |
412 | | ), |
413 | | (get_preference(deterministic_trace_replay,true) -> ! ; true). |
414 | | perform_single_operation(ActionAsTerm,Ident) :- |
415 | | current_options(Options), |
416 | | member( (_Id,PActionS,'*permute*',NewID), Options), /* permute action from symmetry reduction */ |
417 | | perform_action_tclk(PActionS,'*permute*',NewID,Ident), !, |
418 | | (silent_mode(on) -> true |
419 | | ; ident(Ident), print(' | ** PERMUTING **'),nl), |
420 | | perform_single_operation(ActionAsTerm,Ident). |
421 | | perform_single_operation(ActionAsTerm,Ident) :- |
422 | | %%user:current_expression(CurID,State), |
423 | | \+ functor(ActionAsTerm,tau,1), |
424 | | current_options(Options), %print(options(Options)),nl, |
425 | | member( (_Id,AX,tau(X),NewID), Options), |
426 | | (silent_mode(on) -> true |
427 | | ; ident(Ident), print(' | ** SKIPPING ADDITIONAL TAU in SPEC. **'),nl), |
428 | | perform_action_tclk(AX,tau(X),NewID,Ident), |
429 | | perform_single_operation(ActionAsTerm,Ident). |
430 | | %perform_single_operation(ActionAsTerm,Ident) :- |
431 | | % ident(Ident),print(unsuccessful(ActionAsTerm)),nl,fail. |
432 | | |
433 | | |
434 | | perform_action_tclk(Action,ActionOpAsTerm,NewID,_Ident) :- |
435 | | my_perform_action_as_string(Action,ActionOpAsTerm,NewID), |
436 | | user:tcltk_get_options(_). |
437 | | perform_action_tclk(_Action,_ActionOpAsTerm,_NewID,Ident) :- % undo action |
438 | | state_space:current_state_id(FromID), |
439 | | user:tcltk_backtrack, user:tcltk_get_options(_), |
440 | | state_space:current_state_id(ToID), |
441 | | silent_mode(off), |
442 | | ident(Ident), |
443 | | print(backtrack_from_to(FromID,ToID)),nl, |
444 | | fail. |
445 | | |
446 | | % a more flexible version: allow string representations of ProB to evolve compared to when test suites where stored |
447 | | my_perform_action_as_string(ActionStr,ActionOpAsTerm,NewID) :- |
448 | | user:tcltk_perform_action_string(ActionStr,ActionOpAsTerm,NewID). |
449 | | |
450 | | :- use_module(library(avl)). |
451 | | unify_action_as_term(A,A,_) :- !. |
452 | | unify_action_as_term('-->'(Op,Results),'-->'(Op2,Results2),State) :- !, |
453 | | unify_action_as_term(Op,Op2,State), |
454 | | l_unify(Results,Results2). |
455 | | unify_action_as_term(A,B,State) :- functor(A,F,N), functor(B,F2,N2), |
456 | | unify_functor(F,F2,State), |
457 | | (N=N2 -> true |
458 | | ; format('*** SAME EVENT WITH VARYING ARITY: ~w : ~w vs ~w arguments ***~n',[F,N,N2]), |
459 | | % Probably due to show_eventb_any_arguments differently set ? |
460 | | fail), |
461 | | A=..[F|AA], B=..[F2|BB], |
462 | | l_unify(AA,BB). |
463 | | l_unify([],[]). |
464 | | l_unify([H|T],[I|S]) :- unify(H,I), l_unify(T,S). |
465 | | |
466 | | |
467 | | unify_functor('initialise_machine','$initialise_machine',_) :- !. % old-style format |
468 | | unify_functor('setup_constants','$setup_constants',root) :- !. % old-style format |
469 | | unify_functor(X,X,_). |
470 | | |
471 | | %:- use_module(custom_explicit_sets,[equal_explicit_sets/4]). |
472 | | :- use_module(debug). |
473 | | unify(A,A) :- !. |
474 | | unify(A,avl_set(B)) :- %print(exp(A,B)),nl, |
475 | | expand_explicit_set(A,AA), |
476 | | %nl,translate:print_bvalue(AA),nl, translate:print_bvalue(avl_set(B)),nl, % print(chck(A,AA,B)),nl, |
477 | | AA = avl_set(B),!. |
478 | | %unify(A,B) :- print(unify(A,B)),nl,fail. |
479 | | unify(C1,C2) :- is_a_set(C1),(C2=closure(_P,_T,_B) ; C2=global_set(_)), |
480 | | %print(unify_closure(C1,C2)),nl, |
481 | | (C1=[_|_] -> custom_explicit_sets:convert_to_avl(C1,C11) ; C11=C1), % TO DO: replace by proper expansion predicate |
482 | | (unify_explicit_sets(C11,C2) |
483 | | -> true |
484 | | ; print(ko_unify_closure),nl, translate:print_bvalue(C11),nl, translate:print_bvalue(C2),nl, |
485 | | %terms:term_hash((C1,C2),H), print(hash(H)),nl, (H=140674321 -> trace, unify_explicit_sets(C11,C2)), |
486 | | fail),!. |
487 | | %avl_domain(B,R), print(chck(A,B,R)),nl,l_unify(A,R). |
488 | | unify(C1,C2) :- %tools_printing:print_term_summary(fail(C1,C2)),nl, |
489 | | debug_println(9,unify_failed(C1,C2)),fail. |
490 | | |
491 | | is_a_set(closure(_,_,_)). |
492 | | is_a_set([]). |
493 | | is_a_set([_|_]). |
494 | | is_a_set(global_set(_)). |
495 | | is_a_set(avl_set(_)). |
496 | | |
497 | | expand_explicit_set([H|T],AA) :- !, custom_explicit_sets:convert_to_avl([H|T],AA). |
498 | | expand_explicit_set(A,AA) :- |
499 | | on_enumeration_warning(custom_explicit_sets:try_expand_and_convert_to_avl_if_smaller_than(A,AA,200), fail). |
500 | | unify_explicit_sets(C1,C2) :- |
501 | | ALLOW=no_expansion, %(C1 = avl_set(_) -> ALLOW=allow_expansion ; ALLOW=no_expansion), |
502 | | on_enumeration_warning(custom_explicit_sets:equal_explicit_sets4(C1,C2,ALLOW,no_wf_available), fail). |
503 | | |
504 | | |
505 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,root) :- |
506 | | functor(ActionAsTerm,'setup_constants',_), !, % rename to new format |
507 | | nl,print('DEPRECATED TRACE FILE'),nl,nl,nl, |
508 | | ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$setup_constants'|Args], |
509 | | perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID). |
510 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,State) :- |
511 | ? | (State=root ; State=concrete_constants(_)), |
512 | | functor(ActionAsTerm,'initialise_machine',_), !, % rename to new format |
513 | | nl,print('DEPRECATED TRACE FILE'),nl,nl,nl, |
514 | | ActionAsTerm =.. [_|Args], ActionAsTerm2 =..['$initialise_machine'|Args], |
515 | | perform_single_operation_retry(Options,ActionAsTerm2,Action,NewID). |
516 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID,_State) :- |
517 | ? | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID). |
518 | | |
519 | | |
520 | | % check that parameters provided for setup_constants in trace file can be found in State |
521 | | %check_initialised_args([],_). |
522 | | %check_initialised_args([V|T],State) :- |
523 | | % select(bind(_,V2),State,Rest), |
524 | | % unify(V,V2), |
525 | | % %print('SELECTED: '),translate:print_bvalue(V2),nl, |
526 | | % !, |
527 | | % check_initialised_args(T,Rest). |
528 | | %check_initialised_args([V|T],State) :- |
529 | | % print('MISMATCH'),nl, %print(mismatch(V,C)),nl, |
530 | | % print('COULD NOT FIND: '), translate:print_bvalue(V),nl, |
531 | | % tools_printing:print_term_summary(V),nl, |
532 | | % %print(V),nl, print(State),nl, |
533 | | % V=closure(_,_,_), memberchk(bind(_,closure(_,_,_)),State), |
534 | | % check_initialised_args(T,State). |
535 | | |
536 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
537 | | functor(ActionAsTerm,'$setup_constants',_), !, |
538 | | perform_alternative_op_with_same_functor(Options, ['$setup_constants' /* ,'$partial_setup_constants' */], |
539 | | 'set up constants', 'initialisation of constants', |
540 | | ActionAsTerm, Action, NewID), |
541 | | %visited_expression(NewID,concrete_constants(C)), ActionAsTerm =.. [_|Args], |
542 | | % check that state NewID corresponds to parameters provided for setup_constants in trace file |
543 | | %print(check_args),nl, check_initialised_args(Args,C), print('argsok'),nl. % TO DO: try and enable this for all tests |
544 | | true. |
545 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
546 | ? | functor(ActionAsTerm,'$initialise_machine',_),!, |
547 | ? | perform_alternative_op_with_same_functor(Options, ['$initialise_machine'], |
548 | | 'initialise', 'initialisation', |
549 | | ActionAsTerm, Action, NewID), |
550 | | true. %visited_expression(NewID,S), (S=const_and_vars(_,VS) -> true ; VS=S), ActionAsTerm =.. [_|Args], |
551 | | %check_initialised_args(Args,VS), print('initargsok'),nl. |
552 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
553 | | functor(ActionAsTerm,tau,_), arg(1,ActionAsTerm,Arg), nonvar(Arg),!, |
554 | | perform_alternative_op_with_same_functor(Options, [tau], |
555 | | tau, tau, |
556 | | ActionAsTerm, Action, NewID). |
557 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
558 | | functor(ActionAsTerm,F,0), preference(show_eventb_any_arguments,true), |
559 | | /* then allow also the same operation name but with more arguments */ |
560 | | member( (_Id,Action,ActionAsTerm2,NewID), Options), |
561 | | functor(ActionAsTerm2,F,FArity), FArity>0, |
562 | | print_message('Allowing extra Event-B style ANY arguments.'). |
563 | | perform_single_operation_retry(Options,ActionAsTerm,Action,NewID) :- |
564 | ? | functor(ActionAsTerm,F,N),N>0, preference(show_eventb_any_arguments,false), |
565 | | /* then allow also the same operation name but with more arguments */ |
566 | ? | member( (_Id,Action,F,NewID), Options), |
567 | | print_message('Allowing operation without Event-B style ANY arguments.'). |
568 | | %perform_single_operation_retry(Options,_ActionsAsTerm,_Action,_NewID) :- |
569 | | % print_message('No more options: '), print(Options),nl,fail. |
570 | | |
571 | | :- use_module(runtime_profiler,[profile_single_call/3]). |
572 | | :- use_module(tools,[start_ms_timer/1, stop_ms_timer_with_msg/2]). |
573 | | |
574 | | perform_custom_operation_retry(OpName,NewID) :- |
575 | | (OpName = '$initialise_machine' ; OpName = '$setup_constants'), |
576 | | !, |
577 | | state_space:current_state_id(CurID), |
578 | | (max_reached_for_node(CurID) ; not_all_transitions_added(CurID)), |
579 | | preferences:get_preference(maxNrOfInitialisations,0), |
580 | | user:tcltk_add_user_executed_operation_typed(OpName,b(truth,pred,[]),NewID), |
581 | | (get_preference(deterministic_trace_replay,true) -> ! ; true), |
582 | | print_green(init_found(NewID)),nl. |
583 | | perform_custom_operation_retry(ActionAsTerm,NewID) :- |
584 | | (ActionAsTerm = '-->'(_,_) % for operations with return types we cannot provide a predicate to solve yet |
585 | | -> preferences:get_preference(maxNrOfEnablingsPerOperation,0) |
586 | | ; true), |
587 | | state_space:current_state_id(CurID), |
588 | | (max_reached_for_node(CurID) ; not_all_transitions_added(CurID)), |
589 | | debug_println(9,try_custom(CurID,ActionAsTerm)), % Execute operation by predicate |
590 | | % (state_space:transition(CurID,AA,BB,CC),format('Successor of ~w: ~w --~w--> ~w~n',[CurID,AA,BB,CC]),fail ; true), |
591 | | get_operation_name(ActionAsTerm,OpName), |
592 | | get_operation_return_values_and_arguments(ActionAsTerm,ExpectedResults,OpArgs), |
593 | | % TO DO: optionally check return values |
594 | | (OpArgs = [] -> Pred = b(truth,pred,[]) |
595 | | ; \+ b_is_operation_name(OpName) |
596 | | -> add_error(trace_checking_fails,'Operation does not exist in loaded specification:',OpName),fail |
597 | | ; b_get_machine_operation_typed_parameters(OpName,TArgParas), |
598 | | l_generate_predicate(OpArgs,TArgParas,OpName,Conjuncts), |
599 | | conjunct_predicates(Conjuncts,Pred) |
600 | | ), |
601 | | !, |
602 | | %print('PRED: '),translate:print_bexpr(Pred),nl, |
603 | | start_ms_timer(Timer), |
604 | | profile_single_call(OpName,CurID, |
605 | | user:tcltk_add_user_executed_operation_typed(OpName,OpTerm,Pred,NewID) % The Pred can only talk about parameters and the state before; thus this only works for setup_constants and initialise_machine |
606 | | ), |
607 | | (get_preference(deterministic_trace_replay,true) -> ! ; true), % by preventing backtracking we can reduce memory consumption |
608 | | print_green(successor_found(NewID, OpName)),nl, |
609 | | get_operation_return_values_and_arguments(OpTerm,ActualResults,_), |
610 | | (l_unify(ExpectedResults,ActualResults) -> true |
611 | | ; ajoin(['Result values for ',OpName,' do not match for transition from ',CurID,' to ',NewID,':'],Msg), |
612 | | translate_bvalue(ExpectedResults,ER), |
613 | | translate_bvalue(ActualResults,AR), |
614 | | add_warning(b_trace_checking,Msg,[expected(ER),actual(AR)]) |
615 | | ), |
616 | | (debug_mode(on) -> stop_ms_timer_with_msg(Timer,'Custom: ') ; true), |
617 | | garbage_collect, % important to keep memory consumption down for long traces e.g. for Innotrans VBF traces |
618 | | (debug_mode(on) -> print_memory_used_wo_gc,nl ; true), |
619 | | user:tcltk_get_options(_). |
620 | | |
621 | | l_generate_predicate([],[],_,[]) :- !. |
622 | | l_generate_predicate([],_,Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too few parameters for: ',Op). |
623 | | l_generate_predicate(_,[],Op,[]) :- !, add_warning(b_trace_checking,'Trace file contains too many parameters for: ',Op). |
624 | | l_generate_predicate([ArgVal|TArg],[TypedPara|TPar],OpName,[Pred|TPred]) :- |
625 | | generate_predicate(ArgVal,TypedPara,Pred), |
626 | | l_generate_predicate(TArg,TPar,OpName,TPred). |
627 | | generate_predicate(ArgVal,TypedPara,b(equal(TypedPara,TVal),pred,[])) :- |
628 | | get_texpr_type(TypedPara,Type), |
629 | | TVal = b(value(ArgVal),Type,[]). |
630 | | |
631 | | perform_alternative_op_with_same_functor(Options,Functors,ActionMsg,AltMsg,ActionAsTerm,Action,NewID) :- |
632 | ? | \+ member( (_,_,ActionAsTerm,_), Options), |
633 | ? | ajoin(['Could not ', ActionMsg, ' with parameters from trace file.'], Msg1), |
634 | ? | ajoin(['Will attempt any possible ', AltMsg, '.'], Msg2), |
635 | ? | print_message(Msg1), print_message(Msg2), |
636 | | %print(ActionAsTerm),nl, print(Options),nl,nl, |
637 | ? | member( (_,ActionStr,MachineActionAsTerm,NewID), Options), |
638 | | functor(MachineActionAsTerm,Functor,_), |
639 | | member(Functor,Functors), |
640 | | (Action=ActionStr -> true ; print(cannot_match(Action,ActionStr)),nl,fail). |
641 | | |
642 | | single_operation_skip(tau(_),Ident) :- |
643 | | ident(Ident), print(' | *** TRYING TO SKIP TAU IN TRACE FILE'),nl. |
644 | | |
645 | | |
646 | | |
647 | | ident(0). |
648 | ? | ident(N) :- N > 40, !, N1 is N mod 40, ident(N1). |
649 | ? | ident(N) :- N>0, print('- '), N1 is N-1, ident(N1). |
650 | | |
651 | | |
652 | | /* ------------------------------------------------------------------ */ |
653 | | |
654 | | :- use_module(state_space,[get_action_trace/1]). |
655 | | print_trace_as_fdr_check :- |
656 | | print('-- Trace Check Generated by ProB:'),nl, |
657 | | get_action_trace(T), |
658 | | reverse(T,RT), |
659 | | print('PROB_TEST_TRACE = '),print_fdr(RT), |
660 | | nl, |
661 | | print('assert MAIN [T= PROB_TEST_TRACE'),nl. |
662 | | |
663 | | print_fdr([]) :- print('STOP'),nl. |
664 | | print_fdr([jump|T]) :- print_fdr(T). |
665 | | print_fdr([action(Str,Term)|T]) :- |
666 | | (Term = i(_) |
667 | | -> (nl,print(' ( STOP /\\ ')) |
668 | | ; (Term = tick(_) |
669 | | -> print('SKIP ; ') |
670 | | ; ((Term = tau(_) ; Term = 'start_cspm_MAIN') |
671 | | -> true |
672 | | ; (print(Str), print(' -> ')) |
673 | | ) |
674 | | )), |
675 | | print_fdr(T), |
676 | | (Term = i(_) |
677 | | -> print(' )') |
678 | | ; true |
679 | | ). |
680 | | |
681 | | % ----------------------- |
682 | | |
683 | | tcltk_save_history_as_trace_file(Style,File) :- |
684 | | formatsilent('% Saving history (~w format) to: ~w~n',[Style,File]), |
685 | | tell(File), |
686 | | (specfile:b_or_z_mode |
687 | | -> b_machine_name(OurName) |
688 | | ; specfile:currently_opened_file(OurName) |
689 | | ), |
690 | | (Style=prolog -> print_quoted(machine(OurName)), print('.'),nl ; true), |
691 | | call_cleanup(print_trace_for_replay(Style), |
692 | | (told,print_message(done))). |
693 | | |
694 | | :- use_module(state_space,[transition/4, op_trace_ids/1]). % transition(CurID,Term,TransId,DestID) |
695 | | |
696 | | % print the animator's history trace for later replay |
697 | | % prolog style is currently used by ProB Tcl/Tk |
698 | | % json style is used by ProB2 UI |
699 | | print_trace_for_replay(Style) :- |
700 | | op_trace_ids(OpIds), |
701 | | reverse(OpIds,Trace), |
702 | | print_trace_for_replay(Style,Trace). |
703 | | |
704 | | print_trace_for_replay(prolog,Trace) :- !, print_transition_list_prolog(Trace). |
705 | | print_trace_for_replay(json,Trace) :- !, print_transition_list_json(Trace). |
706 | | print_trace_for_replay(Style,_) :- |
707 | | add_internal_error('Style not supported: ',print_trace_for_replay(Style,_)). |
708 | | |
709 | | print_transition_list_prolog(Trace) :- |
710 | | member(OpId,Trace), |
711 | | transition(PrevId,Op,OpId,SuccId), |
712 | | (atomic(Op), |
713 | | ( transition(PrevId,Op,_,SuccId2), SuccId2 \= SuccId -> true), % another transition with same label Op exists |
714 | | translate:get_non_det_modified_vars_in_target_id(Op,SuccId,NonDetVars) |
715 | | -> print_quoted('$non_det_modified_vars'(Op,NonDetVars)) |
716 | | ; print_quoted(Op) |
717 | | ), |
718 | | write('.'),nl, |
719 | | fail. |
720 | | print_transition_list_prolog(_). |
721 | | |
722 | | % print list in JSON format for ProB2 UI: |
723 | | print_transition_list_json(Trace) :- |
724 | | format('{~n "transitionList": [~n',[]), |
725 | | print_json_list(Trace), |
726 | | format(' ]~n }~n',[]). |
727 | | |
728 | | print_json_list([]). |
729 | | print_json_list([H|T]) :- print_json_opid(H), |
730 | | (T==[] -> nl ; write(','),nl, print_json_list(T)). |
731 | | |
732 | | :- use_module(specfile,[get_operation_internal_name/2, |
733 | | get_operation_return_values_and_arguments/3, |
734 | | get_possible_language_specific_top_level_event/3]). |
735 | | |
736 | | print_json_opid(OpId) :- %print(Op),nl, trace, |
737 | | transition(_PrevId,Op,OpId,_SuccId), |
738 | | get_operation_internal_name(Op,OpName), % TO DO: currently this is INITIALISATION instead of $initialise_machine |
739 | | (get_possible_language_specific_top_level_event(OpName,ResultNames,ParaNames) -> true |
740 | | ; ResultNames=unknown, ParaNames=unknown), |
741 | | get_operation_return_values_and_arguments(Op,ReturnValues,Paras), |
742 | | % TO DO: extract variables and constants for $initialise_machine, $setup_constants |
743 | | format(' {~n',[]), |
744 | | format(' "name": "~w",~n',[OpName]), |
745 | | format(' "params": {~n',[]), |
746 | | (get_preference(show_eventb_any_arguments,true), |
747 | | \+ same_length(Paras,ParaNames) |
748 | | -> print_json_paras(Paras,1,unknown) |
749 | | ; print_json_paras(Paras,1,ParaNames) |
750 | | ), |
751 | | (ReturnValues=[] -> true |
752 | | ; format(' },~n',[]), |
753 | | format(' "results": {~n',[]), |
754 | | print_json_paras(ReturnValues,1,ResultNames) |
755 | | ), |
756 | | format(' }~n',[]), |
757 | | format(' }',[]). |
758 | | |
759 | | :- use_module(translate, [translate_bvalue/2]). |
760 | | :- use_module(tools,[b_escape_string_atom/2]). |
761 | | mytranslate(H,ES) :- translate_bvalue(H,S), b_escape_string_atom(S,ES). |
762 | | |
763 | | % print_json_paras(ListOfValues,ParameterNr,ListOfParameterNames) |
764 | | print_json_paras([],_,_) :- !. |
765 | | print_json_paras([H|T],Nr,[HName|NT]) :- !, Nr1 is Nr+1, |
766 | | b_escape_string_atom(HName,EN), |
767 | | mytranslate(H,ES), |
768 | | format(' "~w": "~w"',[EN,ES]), |
769 | | (T==[] -> nl ; write(','),nl, print_json_paras(T,Nr1,NT)). |
770 | | print_json_paras([H|T],Nr,unknown) :- Nr1 is Nr+1, |
771 | | mytranslate(H,ES), |
772 | | !, |
773 | | format(' "para~w": "~w"',[Nr,ES]), |
774 | | (T==[] -> nl ; write(','),nl, print_json_paras(T,Nr1,unknown)). |
775 | | print_json_paras(P,Nr,PN) :- add_internal_error('Cannot print JSON parameters:',print_json_paras(P,Nr,PN)). |