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 | :- module(eclipse_interface, | |
6 | [ | |
7 | clear_loaded_machines/0, | |
8 | clear_loaded_machines_wo_errors/0, | |
9 | ||
10 | get_rand/4, % DEPRECATED, remove when switching to the new core | |
11 | set_rand/4, % DEPRECATED, remove when switching to the new core | |
12 | ||
13 | debug_console/2, | |
14 | ||
15 | typecheck_b_project/3, | |
16 | ||
17 | load_b_file/1, load_prob_file/1, | |
18 | load_eventb_file/1, | |
19 | load_tla_file/1, | |
20 | load_xtl_file/1, | |
21 | ||
22 | load_classical_b/1, % deprecated | |
23 | load_classical_b/2, % deprecated | |
24 | ||
25 | find_shortest_trace_to_current_state/1, | |
26 | find_shortest_trace_to_current_state2/2, | |
27 | ||
28 | do_ltl_modelcheck/6, | |
29 | ||
30 | get_invariants/1, | |
31 | get_name/1, | |
32 | ||
33 | evaluate/3, | |
34 | ||
35 | %es_reset/0, %evalstore: reset, remove all dynamic stores | |
36 | ||
37 | load_cspm_spec_from_pl_file/1, | |
38 | ||
39 | init_eclipse_preferences/0, | |
40 | ||
41 | set_eclipse_card/2, | |
42 | ||
43 | getAllOperations/1, % deprecated, remove in 2.0 | |
44 | getSetElements/1, | |
45 | getInternalRep/1, | |
46 | get_machine_objects/5, | |
47 | ||
48 | get_all_transitions/1, | |
49 | ||
50 | getErrorMessages/2, | |
51 | ||
52 | ops_with_timeout/1, ops_with_virtual_timeout/1, ops_with_real_timeout/1, ops_user_interrupt_occured/0, | |
53 | ||
54 | getCurrentStateID/1, | |
55 | getVarCstValue/3, applyVarCstValue/4, | |
56 | isRootState/1, isConstantsSetUpState/1, | |
57 | getOperationParameterNames/2, % deprecated, remove in 2.0 | |
58 | ||
59 | get_operation_infos/1, | |
60 | ||
61 | ||
62 | % getCurrentStateValues/2, no longer exists ??! | |
63 | getStateValues/2, | |
64 | ||
65 | test_boolean_expression_in_node/2, | |
66 | computeOperations/1, | |
67 | executeOperationNr/1, executeOperationNr_on_computed_node/1, | |
68 | ||
69 | setCurrentState/1, | |
70 | computeOperationsForState/2, % Used in ProB 1.0 | |
71 | ||
72 | evaluate_expression/2, | |
73 | ||
74 | print_states_for_dot/1, | |
75 | ||
76 | evaluate_expression_as_tree/4, | |
77 | evaluate_properties_as_tree/1, | |
78 | evaluate_invariant_as_tree/2, | |
79 | evaluate_precondition_as_tree/3, | |
80 | evaluate_raw_expression_as_tree/3, | |
81 | ||
82 | %in contrast to evaluate_expression, it supports predicates and does typing | |
83 | evaluate_raw_expression/3, | |
84 | evaluate_raw_expressions/3, | |
85 | ||
86 | sap_generate_local_testcases/5, | |
87 | sap_find_test_path/4, | |
88 | execute_custom_operations/6, | |
89 | ||
90 | evaluation_get_top_level/1, | |
91 | evaluation_expand_formula/3, | |
92 | evaluation_get_values/3, | |
93 | evaluation_insert_formula/3, | |
94 | ||
95 | deadlock_freedom_check/1, | |
96 | deadlock_freedom_check/2, | |
97 | invariant_check/2, | |
98 | ||
99 | save_as_classical_b/4, | |
100 | ||
101 | analyse_predicate/6, | |
102 | get_classicalb_machine_objects/2, | |
103 | ||
104 | dot_hierarchy/1, | |
105 | ||
106 | refinement_check/2, | |
107 | ||
108 | load_sets_for_cbc/1, | |
109 | ||
110 | cbc_static_assertion_violation_checking/1, | |
111 | get_vacuous_invariants/1, get_vacuous_guards/1, | |
112 | ||
113 | quick_describe_unsat_properties/1, | |
114 | find_state_satisfying_predicate/2, | |
115 | ||
116 | prob_construct_trace/6 | |
117 | ]). | |
118 | ||
119 | :- use_module(module_information). | |
120 | :- module_info(group,cli). | |
121 | :- module_info(description,'This module provides the Prolog interface to Java and other languages (usually called via socket server).'). | |
122 | ||
123 | :- use_module(library(system),[environ/2]). | |
124 | :- use_module(library(lists)). | |
125 | ||
126 | :- use_module(error_manager). | |
127 | :- use_module(self_check). | |
128 | :- use_module(bsyntaxtree). | |
129 | :- use_module(version). | |
130 | :- use_module(eventhandling,[announce_event/1]). | |
131 | ||
132 | :- use_module(model_checker). | |
133 | ||
134 | :- use_module(b_global_sets,[enum_global_type/2]). | |
135 | :- use_module(translate). | |
136 | :- use_module(store). | |
137 | ||
138 | :- use_module(bvisual2). | |
139 | ||
140 | :- use_module(library(codesio)). | |
141 | ||
142 | :- use_module(state_space,[visited_expression/2, visited_expression_id/1]). | |
143 | :- ensure_loaded(tcltk_interface). | |
144 | ||
145 | ||
146 | :- use_module(b_state_model_check,[cbc_deadlock_freedom_check/3]). | |
147 | ||
148 | :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]). | |
149 | ||
150 | %:- use_module(extension('counter/counter'), [get_counter/2]). | |
151 | :- use_module(prob2_interface, [get_state/2]). | |
152 | ||
153 | % analyse_predicate(+Type,-Desc,-Result,-Total,-False,-Unknown) | |
154 | ||
155 | analyse_predicate(Type,Desc,Result,Total,False,Unknown) :- | |
156 | user:tcltk_analyse_option(Type,Desc), | |
157 | user:tcltk_analyse(ascii,Type,list(Result),Total,False,Unknown). | |
158 | ||
159 | ||
160 | /* a list of the calls provided by this interface; useful for the whitelist of the socket server */ | |
161 | ||
162 | ||
163 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
164 | % WARNING: This is dangerous in a release. It allows to execute arbitrary code | |
165 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
166 | ||
167 | ||
168 | check_key(Key) :- | |
169 | environ('PROB_DEBUGGING_KEY',Key). | |
170 | ||
171 | :- dynamic current_prob_module/1. | |
172 | current_prob_module(user). | |
173 | ||
174 | debug_console(Key,Commands) :- | |
175 | check_key(Key), debug_console2(Commands). | |
176 | debug_console2([]). | |
177 | debug_console2([H|T]) :- | |
178 | nonvar(H), | |
179 | debug_command(H), debug_console2(T). | |
180 | ||
181 | debug_command(set_module(X)) :- | |
182 | !, current_module(X), retractall(current_prob_module(_)), assert(current_prob_module(X)). | |
183 | debug_command(Command) :- | |
184 | current_prob_module(M), | |
185 | write(M:Command),nl, | |
186 | call(M:Command). | |
187 | ||
188 | ||
189 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
190 | ||
191 | ||
192 | /* ------------------------- */ | |
193 | /* Machine Loading Interface */ | |
194 | /* ------------------------- */ | |
195 | ||
196 | %:- use_module(pref_definitions,[b_get_preferences_from_machine/0]). | |
197 | :- use_module(specfile,[b_or_z_mode/0,set_animation_mode/1,set_animation_minor_mode/1,animation_mode/1, | |
198 | set_currently_opened_file/1]). | |
199 | :- use_module(bmachine_construction,[check_machine/4, get_constructed_machine_name/2]). | |
200 | :- use_module(probltlsrc(ltl),[ltl_model_check_with_ce/4,ltl_formula_structure/3]). | |
201 | :- use_module(probltlsrc(ltl_tools),[typecheck_temporal_formula/3]). | |
202 | %:- use_module(tcltk_interface, [find_shortest_trace_to_node/5]). | |
203 | ||
204 | :- use_module(state_space). | |
205 | :- use_module(bmachine). | |
206 | ||
207 | ||
208 | % DEPRECATED, only here because the old Rodin plugin calls the predicates | |
209 | get_rand(0,0,0,0). | |
210 | set_rand(_,_,_,_). | |
211 | ||
212 | %:- use_module(preferences,[reset_all_temporary_preferences/0]). | |
213 | clear_loaded_machines :- | |
214 | clear_loaded_machines_wo_errors, | |
215 | reset_errors, | |
216 | % now done via event-handling: reset_all_temporary_preferences, | |
217 | garbage_collect_atoms,!. % reclaim atoms if possible | |
218 | clear_loaded_machines :- add_error(clear_loaded_machines,'clear_loaded_machines Failed'). | |
219 | ||
220 | % new profiler | |
221 | %:- use_module('../extensions/profiler/profiler.pl'). | |
222 | ||
223 | % old profiler | |
224 | %:- use_module(runtime_profiler,[reset_runtime_profiler/0]). | |
225 | ||
226 | :- use_module(eval_strings,[reset_eval_strings/0]). | |
227 | :- use_module(eventhandling, [announce_event/1]). | |
228 | clear_loaded_machines_wo_errors :- | |
229 | announce_event(reset_specification), | |
230 | announce_event(clear_specification), | |
231 | % Now done via event_handling: reduce_graph_reset reset_runtime_profiler, reset_refinement_checker state_space_initialise, b_machine_hierarchy:reset_hierarchy, b_interpreter:reset_b_interpreter, reset_model_checker haskell_csp:clear_cspm_spec, b_machine_reset, | |
232 | % reset_dynamics, % new profiler | |
233 | reset_eval_strings. | |
234 | ||
235 | % Errors is a list of error(ErrorDescription,Position) | |
236 | % Position is the number of the Syntaxtree-Node | |
237 | typecheck_b_project(Main,Machines,Errors) :- | |
238 | check_machine(Main,Machines,_,Errors). | |
239 | ||
240 | load_classical_b(Machines) :- % DEPRECATED | |
241 | set_animation_mode(b), | |
242 | load_classical_b(Machines,Errors), | |
243 | add_errors(Errors). | |
244 | load_classical_b(Machines,Errors) :- | |
245 | [First|_] = Machines, | |
246 | get_constructed_machine_name(First,Main), | |
247 | b_set_machine(Main,Machines,Errors). | |
248 | % Don't forget to call update_preferences_from_spec after this and before start_animation | |
249 | ||
250 | ||
251 | add_errors([]). | |
252 | add_errors([H|T]) :- error_manager:add_error('eclipse_interface','Error loading machine',H),add_errors(T). | |
253 | ||
254 | :- use_module(debug,[debug_println/2]). | |
255 | :- use_module(parsercall,[call_tla2b_parser/1, tla2prob_filename/2]). | |
256 | load_tla_file(Filename) :- | |
257 | call_tla2b_parser(Filename), | |
258 | tla2prob_filename(Filename,GeneratedProbFile), | |
259 | debug_println(10,loading_generated_prob_file(GeneratedProbFile)), | |
260 | load_prob_file(GeneratedProbFile), | |
261 | %load_b_file(GeneratedBFile), | |
262 | debug_println(10,set_animation_minor_mode(tla)), | |
263 | set_animation_minor_mode(tla). | |
264 | load_b_file(Filename) :- | |
265 | clear_loaded_machines_wo_errors, | |
266 | set_animation_mode(b), | |
267 | bmachine:b_load_machine_from_file(Filename), | |
268 | set_currently_opened_file(Filename). | |
269 | load_prob_file(Filename) :- | |
270 | clear_loaded_machines_wo_errors, | |
271 | set_animation_mode(b), | |
272 | bmachine:b_load_machine_probfile(Filename), | |
273 | set_currently_opened_file(Filename). | |
274 | ||
275 | :- use_module(prob2_interface, [load_event_b_project/4]). | |
276 | :- use_module(tools_files, [write_to_utf8_file/2]). | |
277 | ||
278 | save_as_classical_b(File,Machines,Contexts,Errors) :- | |
279 | /* first set the number of animated levels to 0*/ | |
280 | get_preference(number_animated_abstractions,OldNum), | |
281 | call_cleanup( ( set_preference(number_animated_abstractions,0), | |
282 | load_event_b_project(Machines,Contexts,[],Errors),!), | |
283 | set_preference(number_animated_abstractions,OldNum)), | |
284 | ( Errors==[] -> | |
285 | b_show_eventb_as_classicalb(Rep,true), | |
286 | write_to_utf8_file(File,Rep) | |
287 | ; otherwise -> | |
288 | /* Do nothing, but return the list of errors*/ | |
289 | true). | |
290 | ||
291 | ||
292 | load_eventb_file(Filename) :- | |
293 | clear_loaded_machines_wo_errors, | |
294 | set_animation_mode(b), set_animation_minor_mode(eventb), | |
295 | b_load_eventb_project(Filename), | |
296 | set_currently_opened_file(Filename). | |
297 | ||
298 | :- use_module(xtl_interface,[open_xtl_file/1]). | |
299 | load_xtl_file(Filename) :- | |
300 | clear_loaded_machines_wo_errors, | |
301 | set_animation_mode(xtl), | |
302 | xtl_interface:open_xtl_file(Filename), | |
303 | set_currently_opened_file(Filename). | |
304 | ||
305 | get_all_transitions(Transitions) :- | |
306 | findall(trans(TransId,Src,Event,PP,Dst,Infos), | |
307 | ( transition(Src,Event,TransId,Dst), | |
308 | translate_event(Event,PP), | |
309 | get_event_infos(TransId,Infos)), | |
310 | Transitions). | |
311 | ||
312 | get_event_infos(TransId,Infos) :- | |
313 | findall(Info, transition_info(TransId,Info), Infos1), | |
314 | filter_transition_infos(Infos1,Infos). | |
315 | ||
316 | filter_transition_infos([],[]). | |
317 | filter_transition_infos([I|Irest],[O|Orest]) :- | |
318 | filter_transition_info(I,O), | |
319 | filter_transition_infos(Irest,Orest). | |
320 | ||
321 | filter_transition_info(event(StackI),event(StackO)) :- !, | |
322 | filter_event_stack(StackI,StackO). | |
323 | filter_transition_info(I,I). | |
324 | ||
325 | filter_event_stack([],[]). | |
326 | filter_event_stack([event(Name,Params)|Irest],[event(Name,Strings)|Orest]) :- | |
327 | translate_bvalue_l(Params,Strings), | |
328 | filter_event_stack(Irest,Orest). | |
329 | ||
330 | translate_bvalue_l([],[]). | |
331 | translate_bvalue_l([V|Vrest],[S|Srest]) :- | |
332 | translate_bvalue(V,S), | |
333 | translate_bvalue_l(Vrest,Srest). | |
334 | ||
335 | :- use_module(visualize_graph,[tcltk_print_states_for_dot/1]). | |
336 | print_states_for_dot(X) :- visualize_graph:tcltk_print_states_for_dot(X). | |
337 | ||
338 | ||
339 | ||
340 | do_ltl_modelcheck(Formula,Max,Mode,Atomics,Structure,Result) :- | |
341 | typecheck_temporal_formula(Formula,TypeCheckedFormula,Status), | |
342 | ( Status=ok -> | |
343 | ltl_formula_structure(TypeCheckedFormula,Atomics,Structure), | |
344 | ltl_model_check_with_ce(TypeCheckedFormula,Max,Mode,Result1), | |
345 | ltl_adapt_operations(Result1,Result) | |
346 | ; otherwise -> | |
347 | Atomics=[], Structure=[], | |
348 | Result=typeerror([])). | |
349 | ||
350 | ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), counterexample(CE,LoopEntry,PathToCE)) :- !, | |
351 | filter_ops_and_ids(PathToCE1,root,PathToCE), | |
352 | ltl_adapt_ce(CE1,CE). | |
353 | ltl_adapt_operations(Result,Result). | |
354 | ||
355 | ltl_adapt_ce([],[]). | |
356 | ltl_adapt_ce([atom(State,Evals,OpTuple)|Irest],[atom(State,Evals,Transition)|Orest]) :- | |
357 | ltl_adapt_ce2(OpTuple,State,Transition), | |
358 | ltl_adapt_ce(Irest,Orest). | |
359 | ltl_adapt_ce2(none,_State,none). | |
360 | ltl_adapt_ce2((TransId,Action,DstId),State,Transition) :- | |
361 | create_operation_term(TransId,Action,State,DstId,Transition). | |
362 | ||
363 | ||
364 | find_shortest_trace_to_current_state(TraceStrings) :- | |
365 | find_shortest_trace_to_current_state2(TraceStrings, _). | |
366 | ||
367 | find_shortest_trace_to_current_state2(TraceStrings, TraceIDs) :- | |
368 | getCurrentStateID(ID), | |
369 | user:find_shortest_trace_to_node(root,ID,Trace,TraceIDs), | |
370 | translate_events(Trace,TraceStrings). | |
371 | ||
372 | ||
373 | % TODO: Should we put these predicates in another module? They are not called by any Java Interface | |
374 | :- use_module(state_space, [time_out_for_node/3]). | |
375 | ops_with_timeout(OpNameList) :- | |
376 | getCurrentStateID(StateId), | |
377 | ops_with_timeout(StateId,OpNameList,_). | |
378 | ops_with_virtual_timeout(OpNameList) :- | |
379 | getCurrentStateID(StateId), | |
380 | ops_with_timeout(StateId,OpNameList,virtual_time_out(_)). | |
381 | ops_with_real_timeout(OpNameList) :- | |
382 | getCurrentStateID(StateId), | |
383 | ops_with_timeout(StateId,OpNameList,time_out). | |
384 | % Note: possibilities are currently: time_out, user_interrupt_signal, virtual_time_out(_) | |
385 | ops_user_interrupt_occured :- | |
386 | getCurrentStateID(StateId), | |
387 | time_out_for_node(StateId,_,user_interrupt_signal). | |
388 | ops_with_timeout(StateId,OpNameList,Type) :- | |
389 | findall(OpName, time_out_for_node(StateId,OpName,Type), OpNameList). | |
390 | ||
391 | /* ------------------------- */ | |
392 | /* CSP Loading Interface */ | |
393 | /* ------------------------- */ | |
394 | ||
395 | :- use_module(probcspsrc(haskell_csp),[load_cspm_pl_file/1]). | |
396 | load_cspm_spec_from_pl_file(CSPMFile) :- | |
397 | clear_loaded_machines_wo_errors, | |
398 | specfile:set_animation_mode(cspm), | |
399 | load_cspm_pl_file(CSPMFile), | |
400 | set_currently_opened_file(CSPMFile). | |
401 | ||
402 | /* --------------------- */ | |
403 | /* Preferences Interface */ | |
404 | /* --------------------- */ | |
405 | ||
406 | :- use_module(preferences, | |
407 | [init_preferences/0,set_preference/2,get_preference/2]). | |
408 | ||
409 | :- use_module(state_space_exploration_modes,[reset_depth_breadth_first_mode/0]). | |
410 | init_eclipse_preferences :- preferences:init_preferences, reset_depth_breadth_first_mode. | |
411 | ||
412 | % set Cardinality of SET; a bit like scope_SET == Scope DEFINITION | |
413 | :- use_module(b_global_sets,[set_user_defined_scope/2]). | |
414 | :- use_module(tools_strings, [convert_cli_arg/2]). | |
415 | set_eclipse_card(Set,Scope) :- | |
416 | convert_cli_arg(Scope,Value), | |
417 | set_user_defined_scope(Set,Value). | |
418 | ||
419 | ||
420 | /* ------------------ */ | |
421 | /* getErrorMessages/1 */ | |
422 | /* ------------------ */ | |
423 | /* Returns a list of strings containing all error messages (of the error_manager). | |
424 | Clears all the errors. Returns the empty list if no errors occurred since | |
425 | the last call to getErrorMessages. | |
426 | ||
427 | TODO: This is equivalent with the get_error_messages predicate in prob2_interface | |
428 | We changed the name in the ProB 2.0 interface for coding convention. | |
429 | */ | |
430 | ||
431 | getErrorMessages(WarningsOnly,ListOfErrMsgs) :- | |
432 | (real_error_occurred -> WarningsOnly = false ; WarningsOnly = true), | |
433 | (get_all_errors_and_reset(ListOfErrMsgs) -> true ; ListOfErrMsgs=[]). | |
434 | ||
435 | ||
436 | ||
437 | /* ---------------------------- */ | |
438 | /* Syntax Information Interface */ | |
439 | /* ---------------------------- */ | |
440 | ||
441 | getAllOperations(L) :- | |
442 | (b_or_z_mode | |
443 | -> findall(OperationName, b_top_level_operation(OperationName), L) | |
444 | ; L=[]). % FIXME: provide list for CSP-M | |
445 | ||
446 | ||
447 | get_operation_infos(L) :- | |
448 | findall(op(Name,Results,Parameters),b_get_machine_operation(Name,Results,Parameters,_,_,_),L). | |
449 | ||
450 | ||
451 | ||
452 | ||
453 | getSetElements(L) :- /* get a list of all fd(N,S) elements of all sets and precompute their translation */ | |
454 | findall(fds(Nr,Set,String), | |
455 | (enum_global_type(fd(Nr,Set),_), translate_bvalue(fd(Nr,Set),String)), L). | |
456 | ||
457 | ||
458 | :- use_module(specfile,[get_internal_representation/1]). | |
459 | getInternalRep(X) :- get_internal_representation(X). | |
460 | ||
461 | get_classicalb_machine_objects(Constants, Variables) :- | |
462 | b_get_machine_constants(C),translate_list(C,Constants), | |
463 | b_get_machine_variables(V),translate_list(V,Variables). | |
464 | ||
465 | ||
466 | translate_list([],[]). | |
467 | translate_list([H|T],[HT|TT]) :- translate_bexpression(H,HT), translate_list(T,TT). | |
468 | ||
469 | ||
470 | ||
471 | get_machine_objects(Sections,SetElements,Constants,Variables,Operations) :- | |
472 | b_get_animated_sections(Sections), | |
473 | findall(TId, | |
474 | ( enum_global_type(fd(Nr,Set),_), | |
475 | translate_bvalue(fd(Nr,Set),String), | |
476 | create_texpr(identifier(String),global(Set),[],TId)), | |
477 | SetElements), | |
478 | b_get_machine_constants(Constants), | |
479 | b_get_machine_variables(Variables), | |
480 | b_get_promoted_machine_operations(Operations1), | |
481 | maplist(remove_op,Operations1,Operations). | |
482 | remove_op(TId,NTId) :- | |
483 | remove_bt(TId,identifier(Id),identifier(NId),NTId), | |
484 | remove_op2(Id,NId). | |
485 | remove_op2(op(Op),Op) :- !. | |
486 | remove_op2(Op,Op). | |
487 | ||
488 | /* ------------------- */ | |
489 | /* Animation Interface */ | |
490 | /* ------------------- */ | |
491 | ||
492 | ||
493 | get_invariants(List) :- %print(start),nl, | |
494 | b_get_invariant_from_machine(B), | |
495 | % print(got(B)),nl, | |
496 | conjunction_to_list(B,L), %print(L),nl, | |
497 | maplist(mk_inv,L,List). | |
498 | ||
499 | mk_inv(C,inv(Text,Pos)) :- translate_bexpression(C,Text),get_texpr_pos(C,P), (P=pos(Pos,_,_,_,_,_) -> true;Pos = P),!. | |
500 | mk_inv(C,_) :- add_internal_error(mk_inv,'Failed: ',C, unknown),fail. | |
501 | ||
502 | get_name(Name) :- b_machine_name(Name). | |
503 | ||
504 | /* get the ID of the current state */ | |
505 | getCurrentStateID(CurID) :- | |
506 | current_state_id(CurID). | |
507 | /* get the ID of the current state */ | |
508 | ||
509 | ||
510 | ||
511 | isRootState(ID) :- ID=root. | |
512 | ||
513 | :- use_module(specfile,[state_corresponds_to_set_up_constants/1, | |
514 | state_corresponds_to_initialised_b_machine/2]). | |
515 | ||
516 | isConstantsSetUpState(ID) :- | |
517 | % true if no constants exists or if all constants have been valued | |
518 | visited_expression(ID,State), | |
519 | specfile:state_corresponds_to_set_up_constants(State). | |
520 | ||
521 | ||
522 | ||
523 | ||
524 | /* compute enabled operations, if required, and return a list of | |
525 | strings of all possible operations and arguments */ | |
526 | computeOperations(Operations) :- | |
527 | user:tcltk_get_options(list(Operations)). | |
528 | ||
529 | ||
530 | executeOperationNr(Nr) :- | |
531 | user:compute_all_transitions_if_necessary, /* make sure options are computed; TO DO: improve */ | |
532 | user:tcltk_perform_nr(Nr). | |
533 | executeOperationNr_on_computed_node(Nr) :- % a version which does not recompute transitions if necessary | |
534 | user:tcltk_perform_nr(Nr). | |
535 | ||
536 | ||
537 | setCurrentState(ID) :- current_state_id(ID),!. % no need to jump | |
538 | setCurrentState(ID) :- /* jumps to the given node; can be backtracked */ | |
539 | visited_expression_id(ID), | |
540 | user:tcltk_goto_state(jump,ID). | |
541 | ||
542 | ||
543 | test_boolean_expression_in_node(ResID,BoolExpr) :- | |
544 | visited_expression(ResID,CurState), | |
545 | specfile:state_corresponds_to_initialised_b_machine(CurState,CurBState), | |
546 | b_interpreter:b_test_boolean_expression_wf(BoolExpr,[],CurBState). | |
547 | ||
548 | /* USED IN PROB 1.0*/ | |
549 | computeOperationsForState(StateID, OpsAndIDs) :- /* compute the enabled operations | |
550 | (without the backtrack options) for a state ID which is not necessarily the current one */ | |
551 | visited_expression_id(StateID), | |
552 | user:tcltk_compute_options(StateID,OpsSTAndIDs), | |
553 | print('OpsSTAndIDs: '),print(OpsSTAndIDs),nl, | |
554 | (filter_ops_and_ids(OpsSTAndIDs,StateID,OpsAndIDs) -> true | |
555 | ; print(filter_ops_and_ids_failed(OpsSTAndIDs)),nl,fail). | |
556 | ||
557 | /* | |
558 | op(140,io,23,23,[[in(r14_1m)],'SetRoute',multi_span(460,35,460,71,16934,36,src_span(460,31,460,32,16930,1))],['{<< in(r14_1m) >>}','<< SetRoute >>','<< multi_span(460,35,460,71,16934,36,src_span(460,31,460,32,16930,1)) >>'],[],') | |
559 | */ | |
560 | ||
561 | ||
562 | getOperationParameterNames(Operation,Paras) :- | |
563 | b_get_machine_operation_parameter_names(Operation,Paras). | |
564 | ||
565 | filter_ops_and_ids([],_,[]). | |
566 | filter_ops_and_ids([OpTuple|T],StateID,[FOp|FT]) :- | |
567 | ((OpTuple = (Id,OpTerm,Dst), create_operation_term(Id,OpTerm,StateID,Dst,FOp)) | |
568 | -> true | |
569 | ; print(filter_op_failed(OpTuple,StateID)),nl, FOp = ('?')), | |
570 | filter_ops_and_ids(T,StateID,FT). | |
571 | ||
572 | filter_op(TransId,OpTerm,Src,Dst,JavaOpTerm) :- | |
573 | (animation_mode(cspm) -> | |
574 | filter_op_csp(TransId,OpTerm,Src,Dst,JavaOpTerm) | |
575 | ; otherwise -> | |
576 | filter_op1(TransId,OpTerm,Src,Dst,JavaOpTerm)). | |
577 | ||
578 | filter_op1(TransId,OpTerm,Src,Dst, | |
579 | op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,State)) :- | |
580 | extract_args_and_return_values(OpTerm,Op,Arguments), | |
581 | get_state(Dst,BState), translate:translate_bstate(BState,State), | |
582 | prettyprint(Arguments,ArgumentsPretty), | |
583 | get_event_infos(TransId,Infos). | |
584 | ||
585 | filter_op_csp(TransId,OpTerm,Src,Dst,op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,CSPState)) :- | |
586 | extract_csp_args_and_return_values(OpTerm,Op,Arguments), | |
587 | translate:translate_event(OpTerm,PPEvent), | |
588 | tools: split_atom(PPEvent,['.','!'],[_Op|ArgumentsPretty]), | |
589 | get_state(Dst,CSPState), | |
590 | get_event_infos(TransId,Infos). | |
591 | ||
592 | extract_csp_args_and_return_values(io(Args,ChName,_SPAN),ChName,Args). | |
593 | extract_csp_args_and_return_values(start_cspm(Name),Name,[]). | |
594 | extract_csp_args_and_return_values(start_cspm_MAIN,'start_cspm_MAIN',[]). | |
595 | extract_csp_args_and_return_values(tick(_),tick,[]). | |
596 | extract_csp_args_and_return_values(tau(_),tau,[]). | |
597 | extract_csp_args_and_return_values(_OP,'?',[]). | |
598 | ||
599 | prettyprint([],[]). | |
600 | prettyprint([H|T],[P|R]) :- translate_bvalue(H,P), prettyprint(T,R). | |
601 | ||
602 | :- dynamic result_warning_emitted/0. | |
603 | ||
604 | extract_args_and_return_values(Term,OpName,Arguments) :- | |
605 | ( Term='-->'(OpTerm,Results) -> | |
606 | ( result_warning_emitted -> true | |
607 | ; otherwise -> | |
608 | print('Warning: results of operations are currently treated like arguments'),nl, | |
609 | assert(result_warning_emitted)), | |
610 | append(Results,Args,Arguments) | |
611 | ; otherwise -> Term=OpTerm,Args=Arguments | |
612 | ), | |
613 | OpTerm =.. [OpName|Args]. | |
614 | ||
615 | ||
616 | ||
617 | % returns all variables and their values of the given state as a list | |
618 | % - constants and variables that are defined for the machine but | |
619 | % not present in the given state get the value '?' | |
620 | % - for each variable a term of the form | |
621 | % binding(Id,Value,PPValue,Tag) | |
622 | % is in the result list, where | |
623 | % Id is the variable's name, | |
624 | % Value is its value a Prolog term | |
625 | % PPValue is its pretty-printed value | |
626 | % NOTE: Tag no longer generated: TO DO REVIEW: | |
627 | % Tag is one of (cst,var,unknown), depending on whether the | |
628 | % variable is a constant, a variable or not defined in the | |
629 | % machine description but present in the state | |
630 | getStateValues(CurID,VariableState) :- /* get variable values */ | |
631 | get_state(CurID,CurBState), | |
632 | findall( binding(Id,nope,PPValue), | |
633 | (member(bind(Id,Value),CurBState), | |
634 | ( translate_bvalue(Value,PPValue) -> true | |
635 | ; otherwise -> PPValue='**pretty-print failed**')), | |
636 | VariableState). | |
637 | ||
638 | getVarCstValue(ID,VarOrCst,TVals) :- | |
639 | /* a function to get the value of a particular Variable or Constant; | |
640 | treats relations specially: a list of relation pairs is returned */ | |
641 | get_state(ID,CurBState), | |
642 | member(bind(VarOrCst,Val),CurBState), | |
643 | (Val = [ (_,_) | _] /* check if it is a relation */ | |
644 | -> findall(TFact,relation_fact(_F,VarOrCst,Val,TFact),TVals) | |
645 | ; (TVals = [TVal], Val = TVal) | |
646 | ). | |
647 | ||
648 | relation_fact(_F,_VarOrCst,Val,TFact) :- | |
649 | member((L,R), Val), Fact = (L,R), | |
650 | Fact=TFact. | |
651 | ||
652 | applyVarCstValue(ID,VarOrCstFunction,DomValue,RanResult) :- | |
653 | /* a function to apply a particular Variable or Constant Function/Relation to a value; | |
654 | treats relations specially: a list of relation pairs is returned */ | |
655 | get_state(ID,CurBState), | |
656 | member(bind(VarOrCstFunction,Val),CurBState), | |
657 | member((DomValue,R),Val), | |
658 | R= RanResult. | |
659 | ||
660 | /* ------------------------------- */ | |
661 | ||
662 | /* evaluates an expression in Prolog format and computes the result in the current state */ | |
663 | evaluate_expression(Expression,Result) :- | |
664 | current_expression(_CurID,CurState), | |
665 | b_interpreter:b_compute_expression_nowf(Expression,[],CurState,Result). | |
666 | ||
667 | ||
668 | ||
669 | %% | |
670 | % Code for invariant debug | |
671 | % | |
672 | ||
673 | :- use_module(bvisual). | |
674 | ||
675 | % probably not used anymore ?!! -> was calling non-existing predicates | |
676 | evaluate_properties_as_tree(Tree):- | |
677 | b_get_properties_from_machine(TExpr), | |
678 | evaluate_expression_as_tree(root, [], TExpr, Tree). | |
679 | ||
680 | evaluate_invariant_as_tree(StateID, Tree):- | |
681 | b_get_invariant_from_machine(TExpr), | |
682 | evaluate_expression_as_tree(StateID, [], TExpr, Tree). | |
683 | ||
684 | evaluate_precondition_as_tree(StateID, OpName, Tree):- | |
685 | bvisual:get_operation_pre(OpName, TExpr, _), | |
686 | evaluate_expression_as_tree(StateID, [], TExpr, Tree). | |
687 | ||
688 | ||
689 | evaluate_raw_expression_as_tree(StateID, Raw, Tree):- | |
690 | bmachine:b_type_expression(Raw, [variables], _, TExpr, Errors), | |
691 | ( var(TExpr) -> | |
692 | print(error_while_typing_raw_expression(Errors)),nl, | |
693 | flush_output, | |
694 | !, | |
695 | fail | |
696 | ; | |
697 | evaluate_expression_as_tree(StateID, [], TExpr, Tree) | |
698 | ). | |
699 | ||
700 | ||
701 | evaluate_expression_as_tree(StateID, LocalState, Expr, Tree) :- | |
702 | get_state(StateID, State), | |
703 | get_tree_from_expr2(State, LocalState, Expr, T), | |
704 | get_tree_node_info(T, Children, NewLocalState, Metas), | |
705 | translate_bexpression(Expr, Pretty), | |
706 | create_tree_node(Tree, Children, NewLocalState, [pretty_long_desc(Pretty) | Metas]). | |
707 | ||
708 | evaluate_raw_expression(StateID, Raw, Val):- | |
709 | bmachine:b_type_expression(Raw, [variables], _, TExpr, Errors), | |
710 | ( var(TExpr) -> | |
711 | print(error_while_typing_raw_expression(Errors)),nl, | |
712 | flush_output, | |
713 | !, | |
714 | fail | |
715 | ; | |
716 | get_state(StateID, State), | |
717 | bvisual:x_get_value_of_expr(State, [], TExpr, Val) | |
718 | ). | |
719 | ||
720 | evaluate_raw_expressions(StateID, Raws, Vals):- | |
721 | maplist(evaluate_raw_expression(StateID), Raws, Vals). | |
722 | ||
723 | ||
724 | ||
725 | /* ------------------------- */ | |
726 | /* Execute Operation */ | |
727 | /* ------------------------- */ | |
728 | ||
729 | % MaxNrOfSolutions is the maximum number of solutions ProB returns. Also we should consider existing solutions if the Predicate holds. | |
730 | %:- use_module(succeed_max,[succeed_max_call/2]). | |
731 | ||
732 | /* PROB 1.0 */ | |
733 | execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, Errors) :- | |
734 | setCurrentState(CurID), | |
735 | ||
736 | ( (OpName = '$initialise_machine';OpName = '$setup_constants' ) -> Scope = [prob_ids(visible),variables]; | |
737 | otherwise -> b_top_level_operation(OpName), | |
738 | b_get_machine_operation(OpName,_,Parameters,_), | |
739 | Scope = [identifier(Parameters),prob_ids(visible),variables] % prob scope allows one to use identifiers for deferred set elements | |
740 | ), | |
741 | (MaxNrOfSolutions<1 | |
742 | -> add_message(eclipse_interface,'execute_custom_operations MaxNrOfSolutions < 1: ',MaxNrOfSolutions) | |
743 | ; true), | |
744 | bmachine:b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors), | |
745 | retractall(bmachine:b_machine_temp_predicate(_)), | |
746 | assert(bmachine:b_machine_temp_predicate(TypedPred)), | |
747 | %prob_socketserver:writeln_log(parsed_pred(ParsedPredicate)), %% | |
748 | %prob_socketserver:writeln_log(succeed_max_call(execute_custom_operation(CurID,OpName,TO),MaxNrOfSolutions)), %% | |
749 | findall(TO, execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations), | |
750 | %length(TOperations,Len), prob_socketserver:writeln_log(findall_length(Len)), | |
751 | retractall(bmachine:b_machine_temp_predicate(_)), | |
752 | clear_context_state. | |
753 | ||
754 | % TO DO: check if we need to recompute the operation effect: if the ParsedPredicate is TRUE | |
755 | % (TRUE = equal(none,integer(none,1),integer(none,1)) ) & MaxNrOfSolutions <= | |
756 | % what has already been used previously, we can simply reuse transition from the state space | |
757 | ||
758 | execute_custom_operation(CurID,OpName,Operation_op,Max) :- | |
759 | set_context_state(CurID), | |
760 | visited_expression(CurID,InState), | |
761 | specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max), | |
762 | % logger:writeln_log(sol(OpName,NewState)), %% | |
763 | user:add_trans_id(CurID,Operation,NewState,[],NewID,[],TransId), | |
764 | % logger:writeln_log(ids(OpName,Operation,NewID,TransId)), %% | |
765 | create_operation_term(TransId,Operation,CurID,NewID, Operation_op). | |
766 | ||
767 | ||
768 | ||
769 | % create a term op(...) with infos for Java interface about an operation-transition | |
770 | create_operation_term(TransId,Op,CurID,NewID, JavaOpTerm) :- | |
771 | (filter_op(TransId,Op,CurID,NewID, JavaOpTerm) -> true | |
772 | ; add_error(eclipse_interface,'filter_op failed: ', filter_op(TransId,Op,CurID,NewID, JavaOpTerm)),fail). | |
773 | ||
774 | /* ------------------------- */ | |
775 | /* SAP Testcase Generation */ | |
776 | /* ------------------------- */ | |
777 | :- use_module(sap). | |
778 | ||
779 | ||
780 | sap_generate_local_testcases(GFile,LFile,MaxNodes,Sat,Unsat) :- | |
781 | sap:tcl_create_local_testsuite(GFile,LFile,MaxNodes,Sat,Unsat). | |
782 | ||
783 | sap_find_test_path(Events,EndPredicate,Timeout,Operations) :- | |
784 | type_predicate(EndPredicate,TypedPredicate), | |
785 | ( create_testcase_path(init,Events,TypedPredicate,Timeout,Trace) -> true | |
786 | ; otherwise -> Trace = []), | |
787 | % Trace can be "timeout" or "interrupt", too | |
788 | ( is_list(Trace) -> op_tuples_to_full_operations(Trace,Operations) | |
789 | ; otherwise -> Operations=Trace). | |
790 | ||
791 | op_tuples_to_full_operations([],[]). | |
792 | op_tuples_to_full_operations([(Id,OpTerm,Src,Dst)|Trest],[Op|Orest]) :- | |
793 | create_operation_term(Id,OpTerm,Src,Dst,Op), | |
794 | op_tuples_to_full_operations(Trest,Orest). | |
795 | ||
796 | type_predicate(Predicate,TypedPredicate) :- | |
797 | b_type_expression(Predicate,[variables],pred,TypedPredicate,Errors), | |
798 | add_all_perrors(Errors,[],sap_target_predicate_type_error), | |
799 | no_real_perror_occurred(Errors). | |
800 | ||
801 | /* ------------------------- */ | |
802 | /* Formula evaluation */ | |
803 | /* ------------------------- */ | |
804 | evaluation_get_top_level(Tops) :- | |
805 | % Currently, we do not want to see the rodin information positons | |
806 | % in the expression viewer | |
807 | suppress_rodin_positions, | |
808 | bv_get_top_level(TopIds), | |
809 | findall( top(Id,Label,Children), | |
810 | ( member(Id,TopIds), bv_expand_formula(Id,Label,Children) ), | |
811 | Tops). | |
812 | evaluation_expand_formula(Id,Label,Children) :- | |
813 | % Currently, we do not want to see the rodin information positons | |
814 | % in the expression viewer | |
815 | suppress_rodin_positions, | |
816 | bv_expand_formula(Id,Label,Children). | |
817 | evaluation_get_values(Ids,StateId,Values) :- | |
818 | bv_get_values(Ids,StateId,Values). | |
819 | evaluation_insert_formula(AST,ParentId,Id) :- | |
820 | b_type_expression(AST,[variables],_,Typed,Errors), | |
821 | ( Errors == [] -> | |
822 | bv_insert_formula(Typed,ParentId,Id) | |
823 | ; otherwise -> | |
824 | add_error_and_fail(eclipse_interface,'Could not type-check AST','')). | |
825 | ||
826 | /* ------------------------------- */ | |
827 | /* Find state satisfying predicate */ | |
828 | /* ------------------------------- */ | |
829 | :- use_module(b_state_model_check,[b_set_up_valid_state_with_pred/2]). | |
830 | find_state_satisfying_predicate(Predicate,Result) :- | |
831 | b_type_expression(Predicate,[variables],pred,TPredicate,Errors), | |
832 | ( Errors == [] -> | |
833 | find_state_satisfying_predicate1(TPredicate,Result) | |
834 | ; otherwise -> | |
835 | Result = errors(Errors)). | |
836 | find_state_satisfying_predicate1(Predicate,Result) :- | |
837 | user_interruptable_call_det(user:catch_clpfd_overflow_call1(b_set_up_valid_state_with_pred(State,Predicate)), | |
838 | InterruptResult),!, | |
839 | ( InterruptResult = interrupted -> | |
840 | Result = interrupted | |
841 | ; State = time_out -> | |
842 | Result = interrupted | |
843 | ; otherwise -> | |
844 | Result = state_found(Transition,StateId), | |
845 | create_helper_transition(root,find_valid_state,State,StateId,Transition)). | |
846 | find_state_satisfying_predicate1(_Predicate,no_valid_state_found). | |
847 | ||
848 | ||
849 | /* ------------------------- */ | |
850 | /* Check for deadlocks */ | |
851 | /* ------------------------- */ | |
852 | ||
853 | :- use_module(solver_interface, [call_with_smt_mode_enabled/1]). | |
854 | ||
855 | deadlock_freedom_check(Result) :- | |
856 | create_texpr(truth,pred,[],Predicate), | |
857 | deadlock_freedom_check1(Predicate,Result). | |
858 | deadlock_freedom_check(Predicate,Result) :- | |
859 | b_type_expression(Predicate,[variables],pred,TPredicate,Errors), | |
860 | ( Errors == [] -> | |
861 | deadlock_freedom_check1(TPredicate,Result) | |
862 | ; otherwise -> | |
863 | Result = errors(Errors)). | |
864 | deadlock_freedom_check1(Predicate,Result) :- | |
865 | % always do a deadlock check with SMT mode enabled | |
866 | call_with_smt_mode_enabled(deadlock_freedom_check2(Predicate,Result)). | |
867 | deadlock_freedom_check2(Predicate,Result) :- | |
868 | user_interruptable_call_det(user:catch_clpfd_overflow_call1(cbc_deadlock_freedom_check(State,Predicate,0)), | |
869 | InterruptResult),!, | |
870 | ( InterruptResult = interrupted -> | |
871 | Result = interrupted | |
872 | ; State = time_out -> | |
873 | Result = interrupted | |
874 | ; otherwise -> | |
875 | Result = deadlock(Transition,StateId), | |
876 | create_helper_transition(root,deadlock_check,State,StateId,Transition)). | |
877 | deadlock_freedom_check2(_Predicate,no_deadlock_found). | |
878 | ||
879 | create_helper_transition(SrcId,Op,DstState,DstId,Transition) :- | |
880 | user:tcltk_add_new_transition_transid(SrcId,Op,DstId,DstState,[],TransId), | |
881 | transition(SrcId,Action,TransId,DstId),!, | |
882 | create_operation_term(TransId,Action,SrcId,DstId,Transition). | |
883 | ||
884 | ||
885 | /* ------------------------------- */ | |
886 | /* Find values */ | |
887 | /* ------------------------------- */ | |
888 | %find_values(Commands,Predicate,MaxNumberSolutions,Solutions) :- | |
889 | % setup_userdef_state_space(Commands,root,State,Ids,ConstantsId). | |
890 | ||
891 | %setup_userdef_state_space2(copy_state(Id),CState,State,Ids,ConstantsId) :- | |
892 | % visited_expression(Id,S), | |
893 | % ( S=concrete_constants(Constants) -> | |
894 | % ( CState=root -> ConstantsId = S | |
895 | % ; otherwise -> ConstantsId = CState), | |
896 | ||
897 | ||
898 | /* ------------------------------- */ | |
899 | /* Check for invariant violations */ | |
900 | /* ------------------------------- */ | |
901 | ||
902 | invariant_check(all,Result) :- | |
903 | findall(OpName,b_is_operation_name(OpName),Ops), | |
904 | invariant_check2(Ops,Result). | |
905 | invariant_check(ops(Ops),Result) :- | |
906 | invariant_check2(Ops,Result). | |
907 | invariant_check2(Ops,Result) :- | |
908 | call_with_smt_mode_enabled(user_interruptable_call_det(invariant_check3(Ops,Res,[]), Status)), | |
909 | ( Status = interrupted -> Result = interrupted | |
910 | ; otherwise -> Result = Res). | |
911 | invariant_check3([]) --> !. | |
912 | invariant_check3([Op|Rest]) --> | |
913 | invariant_check_for_single_op(Op), | |
914 | invariant_check3(Rest). | |
915 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]). | |
916 | invariant_check_for_single_op(OpName,In,Out) :- | |
917 | ( clpfd_interface:catch_clpfd_overflow_call1(b_state_model_check:state_model_check(OpName,State1,Operation,State2)) -> | |
918 | In = [counterexample(OpName,Trans1,Trans2)|Out], | |
919 | atom_concat( invariant_check_ , OpName, RootTrans), | |
920 | create_helper_transition(root, RootTrans,State1,StateId1,Trans1), | |
921 | create_helper_transition(StateId1,Operation,State2,_StateId2,Trans2) | |
922 | ; otherwise -> | |
923 | In = Out). | |
924 | ||
925 | /* ------------------------------- */ | |
926 | /* CBC Refinement Checking */ | |
927 | /* ------------------------------- */ | |
928 | :- use_module(cbc_refinement_checks, [cbc_refinement_check/2]). | |
929 | refinement_check(ResultsString,Result) :- | |
930 | call_with_smt_mode_enabled(cbc_refinement_check(ResultsString,Result)). | |
931 | ||
932 | /* ------------------------------- */ | |
933 | /* CBC Sets */ | |
934 | /* ------------------------------- */ | |
935 | ||
936 | :- use_module(library(sets), [list_to_set/2]). | |
937 | %:- use_module(prob2_interface, [initialise_specification/0]). | |
938 | load_sets_for_cbc(Sets) :- | |
939 | list_to_set(Sets,SetOfSets), | |
940 | load_sets_for_cbc_aux(SetOfSets). | |
941 | %initialise_specification. % now has to be called afterwards | |
942 | load_sets_for_cbc_aux([]) :- | |
943 | load_event_b_project([],[event_b_context(none,'CBCSets',[])],[exporter_version(3)],[]), !. | |
944 | load_sets_for_cbc_aux(SetOfSets) :- | |
945 | maplist(create_set_term,SetOfSets,SetTerms), | |
946 | load_event_b_project([],[event_b_context(none,'CBCSets',[sets(none,SetTerms)])],[exporter_version(3)],[]). | |
947 | ||
948 | create_set_term(Name,deferred_set(none,Name)). | |
949 | ||
950 | /* ----------------------------- */ | |
951 | /* CBC Static Assertion Checking */ | |
952 | /* ----------------------------- */ | |
953 | :- use_module(b_state_model_check, [cbc_static_assertions_check/1]). | |
954 | cbc_static_assertion_violation_checking(Result) :- | |
955 | user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_static_assertions_check(State)),InterruptResult), !, | |
956 | ( InterruptResult = interrupted -> | |
957 | Result = interrupted | |
958 | ; State = time_out -> | |
959 | Result = interrupted | |
960 | ; State = no_counterexample_found -> | |
961 | Result = no_counterexample_found | |
962 | ; State = no_counterexample_exists(_,_,_) -> | |
963 | Result = no_counterexample_exists | |
964 | ; otherwise -> | |
965 | State = counterexample_found(RealState), | |
966 | Result = counterexample_found(Transition,StateId), | |
967 | create_helper_transition(root,deadlock_check,RealState,StateId,Transition)). | |
968 | ||
969 | /* ------------------------- */ | |
970 | /* Generate Visualizations */ | |
971 | /* ------------------------- */ | |
972 | ||
973 | evaluate(In,Result,Warnings) :- user:tcltk_eval(In,Result,Warnings,_Solution). % seems no longer used | |
974 | ||
975 | ||
976 | /* ------------------------- */ | |
977 | /* Dot Printing */ | |
978 | /* ------------------------- */ | |
979 | ||
980 | dot_hierarchy(Filename) :- b_machine_hierarchy:write_dot_hierarchy_to_file(Filename). | |
981 | ||
982 | % not used: | |
983 | %:- use_module(evalstores,[evalstore_reset/0]). | |
984 | %es_reset :- evalstore_reset. | |
985 | ||
986 | get_vacuous_invariants(L) :- | |
987 | findall(I,vacuous_invariant(I),L). | |
988 | ||
989 | vacuous_invariant(Inv) :- | |
990 | b_get_invariant_from_machine(Invariant), | |
991 | b_interpreter:member_conjunct(Inv,Invariant,_), | |
992 | get_texpr_expr(Inv,implication(LHS,_RHS)), | |
993 | print('Checking vor vacuity: '), translate:print_bexpr(Inv),nl, | |
994 | (test_boolean_expression_in_node(ResID,LHS) | |
995 | -> print(lhs_true_in_state(ResID)),nl,nl, % Implication can be triggered in at least one state | |
996 | fail | |
997 | ; print(' *** VACUOUS *** '),nl,nl | |
998 | ). | |
999 | ||
1000 | get_vacuous_guards(L) :- | |
1001 | findall(G,vacuous_guard(_,G),L). | |
1002 | ||
1003 | :- use_module(probsrc(tools_strings),[ajoin/2]). | |
1004 | vacuous_guard(OpName,Result) :- | |
1005 | get_guard_with_one_negated(OpName,Guard,Neg), | |
1006 | translate:translate_bexpression_with_limit(Guard,GuardTS), | |
1007 | format('Checking vor vacuity: ~w : ~w~n',[OpName,GuardTS]), | |
1008 | %translate:print_bexpr(Neg),nl, | |
1009 | (test_boolean_expression_in_node(ResID,Neg) | |
1010 | -> print(guard_individually_false_in(ResID)),nl,nl, | |
1011 | fail | |
1012 | ; print(' *** VACUOUS *** '),nl,nl, | |
1013 | ajoin([OpName,' : ',GuardTS],Result) | |
1014 | ). | |
1015 | ||
1016 | ||
1017 | :- use_module(predicate_debugger,[get_operation_enabling_condition/7]). | |
1018 | %:- use_module(b_ast_cleanup, [clean_up/3]). | |
1019 | :- use_module(b_interpreter_components,[construct_optimized_exists/3]). | |
1020 | ||
1021 | % get a guard, by translating all parameters into existential quantifiers | |
1022 | get_guard_with_one_negated(OpName,SingleGuard,FullModifiedGuard) :- | |
1023 | get_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise,false,true), | |
1024 | % TO DO: partition; avoid lifting becomes_such_that conditions | |
1025 | % (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok) | |
1026 | negate_one_guard(EnablingCondition,SingleGuard,ModifiedEnablingCondition), | |
1027 | construct_optimized_exists(Parameters,ModifiedEnablingCondition,FullModifiedGuard). | |
1028 | ||
1029 | :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]). | |
1030 | negate_one_guard(Conjunct,SingleGuard,ModifiedConjunct) :- | |
1031 | conjunction_to_list(Conjunct,L), | |
1032 | append(Rest1,[SingleGuard|Rest2],L), | |
1033 | create_negation(SingleGuard,NegSingleGuard), | |
1034 | append(Rest1,[NegSingleGuard|Rest2],NewGuard), % TO DO: better treatment for well-definedness !? | |
1035 | conjunct_predicates(NewGuard,ModifiedConjunct). | |
1036 | ||
1037 | :- use_module(b_interpreter, [tcltk_quick_describe_unsat_properties/2, tcltk_unsatisfiable_components_exist/0]). | |
1038 | quick_describe_unsat_properties(Res) :- | |
1039 | tcltk_unsatisfiable_components_exist | |
1040 | -> tcltk_quick_describe_unsat_properties(list(TRes),_Status), % sometimes this can be 'The properties were satisfiable' if tcltk_unsatisfiable_components_exist faulty | |
1041 | Res = unsat_properties(TRes) % TO DO: use Status to say unsat or unknown_properties | |
1042 | ; Res = no_unsat_properties_found. | |
1043 | ||
1044 | ||
1045 | % This just bundles a few commands used by BMotionStudio. | |
1046 | % Should avoid communication overhead. | |
1047 | % Replaced by ProB 2.0 Api | |
1048 | :- use_module(prob2_interface,[state_property/3,op_timeout_occurred/2,get_state_errors/2]). | |
1049 | prob_construct_trace([],[],[],[],[],[]). | |
1050 | prob_construct_trace([Name|Names],[Pred|Preds],[NrOfSol|NrOfSols], | |
1051 | [state(NewStateId,StateValues,Initialised,InvKO,MaxOpsReached,Timeout,OpTimeout,StateErrors,UnsatProps,OperationsForState)|States], | |
1052 | [FirstOp|Ops],Errors) :- | |
1053 | getCurrentStateID(Id), | |
1054 | execute_custom_operations(Id,Name,Pred,NrOfSol,Op,LocalErrors), | |
1055 | Op = [FirstOp|_], | |
1056 | FirstOp = op(_,_,_,NewStateId,_,_,_,_), | |
1057 | % the following is essentially ExploreStateCommand | |
1058 | computeOperationsForState(NewStateId,OperationsForState), | |
1059 | getStateValues(NewStateId,StateValues), | |
1060 | state_property(initialised,NewStateId,Initialised), | |
1061 | state_property(invariantKO,NewStateId,InvKO), | |
1062 | state_property(max_operations_reached,NewStateId,MaxOpsReached), | |
1063 | state_property(timeout_occurred,NewStateId,Timeout), | |
1064 | op_timeout_occurred(NewStateId,OpTimeout), | |
1065 | get_state_errors(NewStateId,StateErrors), | |
1066 | quick_describe_unsat_properties(UnsatProps), | |
1067 | setCurrentState(NewStateId), | |
1068 | prob_construct_trace(Names,Preds,NrOfSols,States,Ops,FurtherErrors), | |
1069 | append(LocalErrors,FurtherErrors,Errors). |