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)).