1 | % Heinrich Heine Universitaet Duesseldorf | |
2 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(prob2_interface, | |
6 | [initialise_specification/0, | |
7 | get_version/7, | |
8 | get_prob_total_number_of_errors/1, | |
9 | ||
10 | load_classical_b_from_list_of_facts/2, | |
11 | update_preferences_from_spec/0, update_preferences_from_spec/1, | |
12 | ||
13 | load_event_b_project/4, | |
14 | ||
15 | load_cspm_spec_from_cspm_file/1, | |
16 | load_z_spec_from_tex_file/1, | |
17 | load_xtl_spec_from_prolog_file/1, | |
18 | load_alloy_spec_from_file/1, | |
19 | load_alloy_spec_from_term/2, | |
20 | ||
21 | reset_animator/0, clear_animator/0, start_animation/0, | |
22 | ||
23 | serialize/2, | |
24 | deserialize/2, | |
25 | ||
26 | get_state/2, | |
27 | get_b_state/2, | |
28 | ||
29 | compute_operations_for_state/2, | |
30 | prob2_execute_custom_operations/6, | |
31 | ||
32 | get_op_from_id/4, | |
33 | ||
34 | is_initialised_state/1, | |
35 | is_initialised_b_state/1, | |
36 | state_property/3, | |
37 | op_timeout_occurred/2, | |
38 | ||
39 | get_state_errors/2, | |
40 | ||
41 | evaluate_formula/3, evaluate_formulas/3, | |
42 | evaluate_registered_formulas/3, | |
43 | register_prob2_formula/2, register_prob2_formulas/2, | |
44 | deactivate_prob2_formula/1, deactivate_prob2_formulas/1, | |
45 | activate_prob2_formula/1, activate_prob2_formulas/1, | |
46 | unregister_prob2_formula/1, unregister_prob2_formulas/1, | |
47 | get_machine_formulas/1, | |
48 | get_animation_image_list/1, get_animation_image_matrix_for_state/6, | |
49 | get_react_to_item_right_click_options_for_state/4, | |
50 | react_to_item_right_click_option_for_state/6, | |
51 | ||
52 | evaluate_formula_typecheck/5, | |
53 | ||
54 | get_states_for_predicate/3, | |
55 | ||
56 | filter_states_for_predicate/3, | |
57 | ||
58 | insert_formula_for_expansion/2, | |
59 | expand_formula/3, | |
60 | ||
61 | do_modelchecking/4, | |
62 | set_goal_for_model_checking/1, | |
63 | compute_efficient_statespace_stats/3, | |
64 | compute_coverage/5, | |
65 | get_modelchecking_coverage/5, | |
66 | prob2_deadlock_freedom_check/2, | |
67 | prob2_invariant_check/2, | |
68 | prob2_redundant_invariants/2, | |
69 | ||
70 | ||
71 | ||
72 | get_enable_matrix/2, | |
73 | ||
74 | prob2_do_ltl_modelcheck/4, | |
75 | ||
76 | activate_plugin/1, % not working anymore | |
77 | get_plugin_output/2, % not working anymore | |
78 | ||
79 | find_trace_to_node/2, | |
80 | find_trace_from_node_to_node/3, | |
81 | find_state_for_predicate/3, | |
82 | ||
83 | cbc_disprove/5, cbc_disprove/6, | |
84 | cbc_solve/4, cbc_solve/5, % deprecated | |
85 | cbc_solve_with_opts/5, | |
86 | pretty_print_predicate/3, | |
87 | cbc_generate_test_cases/3, | |
88 | prob2_find_test_path/4, | |
89 | ||
90 | ||
91 | ||
92 | check_csp_assertions/3, | |
93 | ||
94 | list_eclipse_preferences/1, | |
95 | list_all_eclipse_preferences/1, % also includes advanced eclipse preferences | |
96 | list_current_eclipse_preferences/1, | |
97 | get_eclipse_preference/2, | |
98 | set_eclipse_preference/2, | |
99 | ||
100 | get_signature_merge_state_space/2, | |
101 | get_transition_diagram/2, | |
102 | ||
103 | write_dotty_transition_diagram/2, | |
104 | write_dotty_signature_merge/2, | |
105 | write_dot_for_state_viz/2, | |
106 | write_dotty_state_space/1, | |
107 | is_dotty_command/1, write_dotty/2, | |
108 | is_dotty_command_for_expr/1, write_dotty_for_expr/3, | |
109 | get_dot_commands_in_state/2, call_dot_command_and_dot_in_state/5, call_dot_command_in_state/4, | |
110 | %is_dot_command/5, call_dot_command_and_dot/4, % deprecated | |
111 | get_table_commands_in_state/2, call_table_command_in_state/4, | |
112 | ||
113 | get_error_messages/2, | |
114 | get_error_messages_with_span_info/2, | |
115 | ||
116 | es_copy_from_statespace/2, | |
117 | es_eval/4, | |
118 | evaluate_expression_prolog/3, | |
119 | ||
120 | generate_trace_until_condition_fulfilled/4, | |
121 | execute_model/5, execute_model/6, | |
122 | get_unsat_core_with_fixed_conjuncts/3, | |
123 | get_minimum_unsat_core_with_fixed_conjuncts/3, | |
124 | ||
125 | prob2_construct_trace/6, | |
126 | ||
127 | symbolic_model_check/2, | |
128 | ||
129 | % synthesis | |
130 | start_synthesis_from_ui_/13, | |
131 | start_synthesis_single_operation_from_ui_/11, | |
132 | get_valid_and_invalid_equality_predicates_for_operation_/6, | |
133 | get_valid_and_invalid_equality_predicates_for_invariants_/4, | |
134 | get_invariant_violating_vars_from_examples_/3, | |
135 | adapt_machine_code_for_operations_/2, | |
136 | reset_synthesis_context_/0, | |
137 | generate_synthesis_data_from_predicate_/5, | |
138 | ||
139 | % These predicates should probably not be exported after the end of the migration | |
140 | ||
141 | ||
142 | evalb_evaluate_formula/2, | |
143 | evalb_evaluate_tautology/2, | |
144 | ||
145 | get_pretty_print/1, | |
146 | ||
147 | get_primed_predicate/2, | |
148 | get_weakest_precondition/3, | |
149 | before_after_predicate/2, | |
150 | ||
151 | get_machine_operation_names/1, get_machine_operation_infos/1, | |
152 | get_machine_identifiers/2, | |
153 | get_machine_files/1, | |
154 | ||
155 | get_possible_completions/3, | |
156 | get_possible_fuzzy_matches/2 | |
157 | ]). | |
158 | ||
159 | ||
160 | :- use_module(module_information). | |
161 | :- module_info(group,cli). | |
162 | :- module_info(description,'This module provides the new ProB2 Prolog interface to Java and other languages (usually called via socket server).'). | |
163 | ||
164 | :- use_module(state_space, [time_out_for_node/1, time_out_for_node/3, | |
165 | time_out_for_invariant/1, max_reached_for_node/1, | |
166 | max_reached_or_timeout_for_node/1, | |
167 | visited_expression/2, transition/4, visited_expression_id/1, | |
168 | set_context_state/1, clear_context_state/0, | |
169 | state_error/3, current_state_id/1, | |
170 | get_state_space_stats/3 %, state_space_initialise/0 | |
171 | ]). | |
172 | % new profiler | |
173 | %:- use_module('../extensions/profiler/profiler.pl'). | |
174 | ||
175 | ||
176 | :- use_module(symmetry_marker, [precompile_marker_typing_info/0]). | |
177 | :- use_module(value_persistance, [initialise_operation_caching/0]). | |
178 | :- use_module(eventhandling, [announce_event/1]). | |
179 | %:- use_module(self_check, [turn_off_run_time_type_checks/0]). | |
180 | :- use_module(version, [version/4, revision/1, lastchangeddate/1]). | |
181 | :- use_module(pref_definitions, [b_get_preferences_from_machine/0, b_get_preferences_from_machine/1]). | |
182 | :- use_module(bsyntaxtree, [conjunct_predicates/2, get_texpr_ids/2, | |
183 | get_texpr_expr/2, | |
184 | find_identifier_uses/3]). | |
185 | :- use_module(evalstores, [evalstore_bindings/2, evalstore_create_store_by_state/2, evalstore_eval_formula/4]). | |
186 | %:- use_module(model_checker, [is_deadlocked/1]). | |
187 | :- use_module(state_space_exploration_modes,[set_depth_breadth_first_mode/1]). | |
188 | :- use_module(bmachine, [b_type_expression/5, b_get_machine_operation/4, b_get_machine_operation/6, | |
189 | b_type_open_predicate/5, b_top_level_operation/1, | |
190 | b_load_machine_from_list_of_facts/2, | |
191 | b_set_eventb_project_flat/3, load_additional_information/1, | |
192 | b_machine_precompile/0, other_spec_precompile/0, | |
193 | b_set_parsed_typed_machine_goal/1]). | |
194 | :- use_module(probltlsrc(ltl), [ltl_model_check_with_ce/4,preprocess_formula/2]). | |
195 | :- use_module(probltlsrc(ltl_tools), [typecheck_temporal_formula/3]). | |
196 | :- use_module(probltlsrc(ltl_verification), [evaluate_ltl_formula/6]). | |
197 | %:- use_module(b_interpreter, [b_compute_expression_nowf/4]). | |
198 | :- use_module(b_global_sets, [add_prob_deferred_set_elements_to_store/3]). | |
199 | :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2, | |
200 | ignore_user_interrupt_det/1]). | |
201 | :- use_module(library(lists), [maplist/3, maplist/4]). | |
202 | :- use_module(library(codesio), [read_from_codes/2, write_term_to_codes/4]). | |
203 | :- use_module(specfile, [expand_const_and_vars_to_full_store/2, animation_mode/1, | |
204 | b_or_z_mode/0, set_currently_opened_file/1, | |
205 | set_currently_opened_package/1, | |
206 | set_animation_mode/1, set_animation_minor_mode/1]). | |
207 | :- use_module(translate, [translate_bvalue/2, suppress_rodin_positions/0, | |
208 | translate_event/2, translate_bstate/2, translate_state_error/2, | |
209 | translate_bexpression/2, translate_bvalue_with_limit/3, | |
210 | translate_event_error/2, explain_event_trace/2, explain_state_error/3]). | |
211 | :- use_module(error_manager, [add_error_and_fail/3, get_all_errors_and_reset/1, | |
212 | get_all_errors_with_span_info_and_reset/1, | |
213 | add_error/3, add_error/2, add_error_and_fail/2, | |
214 | add_message/2, %reset_errors/0, | |
215 | add_warning/3, | |
216 | add_all_perrors/1, | |
217 | get_error/2, | |
218 | catch_enumeration_warning_exceptions/2, | |
219 | real_error_occurred/0]). | |
220 | :- use_module(tools, [string_concatenate/3, split_atom/3, | |
221 | safe_atom_codes/2,ajoin/2]). | |
222 | %:- use_module(kernel_tools, [map_over_bvalue/3]). % not used ?? | |
223 | :- use_module(bvisual2, [bv_insert_formula/3, bv_expand_formula/3, | |
224 | bv_get_values/3]). | |
225 | :- use_module(preferences, [eclipse_preference/2, get_preference/2, | |
226 | preference_description/2, preference_val_type/2, | |
227 | preference_default_value/2, preference_category/2, | |
228 | set_preference/2, advanced_eclipse_preference/2, | |
229 | obsolete_eclipse_preference/1]). | |
230 | :- use_module(disprover, [disprove/5, disprove_with_opts/6]). | |
231 | :- use_module(solver_interface, [solve_predicate/5, | |
232 | call_with_smt_mode_enabled/1]). | |
233 | :- use_module(probcspsrc(haskell_csp), [parse_and_load_cspm_file/1]). | |
234 | :- use_module(state_space_reduction, [reset_ignored_events/0, set_ignored_events/1, | |
235 | compute_signature_merge/0, compute_transition_diagram/1, | |
236 | get_reduced_node/4, reduced_trans/5, | |
237 | generate_node_color/5, generate_node_labels/3, | |
238 | generate_transition_label/3, generate_transition_color_and_style/6, | |
239 | write_signature_merge_to_dotfile/2]). | |
240 | :- use_module(graph_canon, [print_cstate_graph/2]). | |
241 | :- use_module(debug, [debug_println/2]). | |
242 | :- use_module(unsat_cores, [unsat_core_with_fixed_conjuncts/3, | |
243 | minimum_unsat_core_with_fixed_conjuncts/3]). | |
244 | :- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate_in_state/5, smt_solve_predicate/4]). | |
245 | ||
246 | :- use_module(typechecker). | |
247 | :- use_module(self_check). | |
248 | ||
249 | :- use_module(probsrc('synthesis/deep_learning/predicate_data_generator'), [generate_synthesis_data_from_predicate/5]). | |
250 | :- use_module(synthesis(b_synthesis),[start_synthesis_from_ui/13, | |
251 | start_synthesis_single_operation_from_ui/11, | |
252 | reset_synthesis_context/0]). | |
253 | :- use_module(synthesis(synthesis_util),[get_valid_and_invalid_equality_predicates_for_operation/6, | |
254 | get_valid_and_invalid_equality_predicates_for_invariants/4, | |
255 | get_invariant_violating_vars_from_examples/3, | |
256 | adapt_machine_code_for_operations/2]). | |
257 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
258 | ||
259 | /** | |
260 | Access information about the current version of the ProB core. | |
261 | ||
262 | #### called by: | |
263 | * ProB 2.0: GetVersionCommand | |
264 | */ | |
265 | get_version(Major,Minor,Service,Qualifier,GitRevision,LastChangedDate,PrologInfo) :- | |
266 | version(Major,Minor,Service,Qualifier), | |
267 | revision(GitRevision), lastchangeddate(LastChangedDate), prolog_flag(version,PrologInfo). | |
268 | ||
269 | ||
270 | % get the total number of errors of ProB's Prolog code; cannot be accidentally reset | |
271 | % useful for validation reports,... | |
272 | :- use_module(error_manager,[get_total_number_of_errors/1]). | |
273 | get_prob_total_number_of_errors(X) :- get_total_number_of_errors(X). | |
274 | ||
275 | /* ------------------------- */ | |
276 | /* B Loading Interface */ | |
277 | /* ------------------------- */ | |
278 | ||
279 | /** | |
280 | Loads a classical b model. | |
281 | ||
282 | #### called by: | |
283 | * ProB 2.0: LoadBProjectCommand | |
284 | */ | |
285 | :- mode load_classical_b_from_list_of_facts(+MainFilename,+ListOfFacts). | |
286 | load_classical_b_from_list_of_facts(MainFilename,ListOfFacts) :- | |
287 | clear_animator, | |
288 | b_load_machine_from_list_of_facts(MainFilename,ListOfFacts), | |
289 | set_currently_opened_file(MainFilename), % or should we use set_currently_opened_package | |
290 | update_preferences_from_spec. | |
291 | ||
292 | /** | |
293 | update preferences from SET_PREF Definitions in B machines: | |
294 | should be called after loading a model and before start_animation | |
295 | */ | |
296 | update_preferences_from_spec :- (b_or_z_mode -> b_get_preferences_from_machine ; true). | |
297 | update_preferences_from_spec(List) :- (b_or_z_mode -> b_get_preferences_from_machine(List) ; List=[]). | |
298 | ||
299 | /* ------------------------- */ | |
300 | /* Event-B Loading Interface */ | |
301 | /* ------------------------- */ | |
302 | ||
303 | /** | |
304 | Loads an Event-B model. | |
305 | ||
306 | #### called by: | |
307 | * ProB Plugin: de.prob.eventb.translator.internal.EventBTranslator, DisproverLoadCommand | |
308 | * ProB 2.0: de.prob.model.eventb.translate.EventBModelTranslator (LoadEventBProjectCommand) | |
309 | */ | |
310 | load_event_b_project(Machines,Contexts,Proofs,Errors) :- | |
311 | clear_animator, | |
312 | set_animation_mode(b), set_animation_minor_mode(eventb), | |
313 | b_set_eventb_project_flat(Machines,Contexts,Proofs), | |
314 | load_additional_information(Proofs), | |
315 | Errors = [], | |
316 | set_currently_opened_package(event_b_project). | |
317 | ||
318 | /* ------------------------- */ | |
319 | /* CSP Loading Interface */ | |
320 | /* ------------------------- */ | |
321 | ||
322 | /** | |
323 | Takes a path to a CSPM specification and loads the file using the CSPM parser. | |
324 | ||
325 | #### called by: | |
326 | * ProB 2.0: LoadCSPCommand | |
327 | */ | |
328 | :- mode load_cspm_spec_from_cspm_file(+CSPMFile). | |
329 | load_cspm_spec_from_cspm_file(CSPMFile) :- | |
330 | clear_animator, | |
331 | set_animation_mode(cspm), | |
332 | parse_and_load_cspm_file(CSPMFile), | |
333 | set_currently_opened_file(CSPMFile). | |
334 | ||
335 | /* ------------------------- */ | |
336 | /* Z Loading Interface */ | |
337 | /* ------------------------- */ | |
338 | ||
339 | load_z_spec_from_tex_file(TexFile) :- | |
340 | clear_animator, | |
341 | user:tcltk_open_z_tex_file(TexFile). | |
342 | ||
343 | /* ------------------------- */ | |
344 | /* XTL Loading Interface */ | |
345 | /* ------------------------- */ | |
346 | ||
347 | load_xtl_spec_from_prolog_file(PrologFile) :- | |
348 | clear_animator, | |
349 | user:tcltk_open_xtl_file(PrologFile). | |
350 | ||
351 | load_alloy_spec_from_file(PrologFile) :- | |
352 | clear_animator, | |
353 | user:tcltk_open_alloy_file(PrologFile). | |
354 | ||
355 | :- use_module(probsrc('alloy2b/alloy2b'),[load_alloy_model/2]). | |
356 | load_alloy_spec_from_term(PrologTerm,AlloyFile) :- | |
357 | clear_animator, | |
358 | load_alloy_model(PrologTerm,AlloyFile). | |
359 | /* ------------------------- */ | |
360 | /* Animation */ | |
361 | /* ------------------------- */ | |
362 | ||
363 | reset_animator :- announce_event(reset_specification). % just reset; keeping same spec | |
364 | clear_animator :- reset_animator,announce_event(clear_specification). | |
365 | ||
366 | start_animation :- %reset_errors, % we no longer reset_errors here ! | |
367 | initialise_specification,!. | |
368 | start_animation :- add_error(start_animation,'Start Animation Failed'). | |
369 | %NOW done by events: reset_flow, state_space_initialise, reduce_graph_reset, reset_runtime_profiler, | |
370 | % reset_refinement_checker reset_model_checker, | |
371 | % reset_dynamics, % new profiler | |
372 | ||
373 | :- use_module(eventhandling,[register_event_listener/3]). | |
374 | :- register_event_listener(clear_specification,reset_prob2_interface, | |
375 | 'Reset prob2_interface caches.'). | |
376 | reset_prob2_interface :- retractall(cached_registered_formula_result(_,_,_)). | |
377 | ||
378 | ||
379 | initialise_specification :- /* call once before starting animation or model checking */ | |
380 | announce_event(start_initialising_specification), | |
381 | ( b_or_z_mode -> b_machine_precompile | |
382 | ; otherwise -> | |
383 | preferences:get_preference(symmetry_mode,X), | |
384 | ( X=off -> true | |
385 | ; otherwise -> | |
386 | add_message(initialise_specification,'Symmetry can only be used for B & Z specifications'), | |
387 | preferences:set_preference(symmetry_mode,off) /* Turn symmetry off */ | |
388 | ), | |
389 | %tools:print_bt_message(other_spec_precompile), | |
390 | other_spec_precompile | |
391 | ), | |
392 | %TODO(DP,11.8.2008) | |
393 | user:initialise_operation_not_yet_covered, | |
394 | % now done via event_handline: reset_external_functions, | |
395 | preferences:get_preference(symmetry_mode,SymMode), | |
396 | precompile_marker_typing_info, % from symmetry_marker.pl | |
397 | ( SymMode=nauty -> | |
398 | (graph_canon:initialise_nauty -> true ; preferences:set_preference(symmetry_mode,off)) | |
399 | ; otherwise -> graph_canon:clear_nauty), | |
400 | announce_event(specification_initialised), | |
401 | ( initialise_operation_caching -> true | |
402 | ; otherwise -> add_error_and_fail(b_load_machine,'Initialising operation caching failed')). | |
403 | ||
404 | /* ------------------------- */ | |
405 | /* Handling States */ | |
406 | /* ------------------------- */ | |
407 | ||
408 | /** | |
409 | Produces a prolog serialization of a given state id | |
410 | ||
411 | #### called by: | |
412 | * ProB Plugin: SerializeStateCommand | |
413 | * ProB 2.0: SerializeStateCommand | |
414 | */ | |
415 | :- mode serialize(+Id,-SerializedState). | |
416 | serialize(Id,SerializedState) :- | |
417 | visited_expression(Id,State), | |
418 | write_term_to_codes(State,Codes,".",[quoted(true)]), | |
419 | atom_codes(SerializedState,Codes). | |
420 | ||
421 | /** | |
422 | Deserialize a state and add it if necessary | |
423 | ||
424 | #### called by: | |
425 | * ProB Plugin: DeserializeStateCommand | |
426 | * ProB 2.0: DeserializeStateCommand | |
427 | */ | |
428 | :- mode deserialize(-NewId,+SerializedState). | |
429 | deserialize(NewId,SerializedState) :- | |
430 | atom_codes(SerializedState,Codes), | |
431 | read_from_codes(Codes,State), | |
432 | user:get_id_of_node_and_add_if_required(State,NewId,_Res,root). | |
433 | ||
434 | get_state(ID,BState) :- get_state(ID,BState,_,_). | |
435 | get_state(es(ID),Store,full_initialised_state,-1) :- % use a store from the evalstore module instead of | |
436 | !,evalstore_bindings(ID,Store). % a state from the state space | |
437 | get_state(ID,BState,Kind,ConstID) :- | |
438 | if(visited_expression(ID,State),true,(ID=root,State=root)), | |
439 | get_state2(State,BState,Kind), | |
440 | get_constants_id(State,ID,ConstID). | |
441 | get_state2(csp_and_b(CSPState,BState),[bind('CSP_CONTROLLER',CSPState)|ExpandedBState],Kind) :- !, | |
442 | get_state2(BState,ExpandedBState,Kind). | |
443 | get_state2(concrete_constants(BState),BState,constants_only_state) :- !. | |
444 | get_state2(root,BState,empty_state) :- !, BState=[]. | |
445 | get_state2(State,Res,full_initialised_state) :- expand_const_and_vars_to_full_store(State,BState), | |
446 | (BState=[_|_] -> Res=BState ; Res=[] /* we have [] or a CSP process or similar */). | |
447 | ||
448 | get_constants_id(const_and_vars(ConstID,_),_,Res) :- !,Res=ConstID. | |
449 | get_constants_id(concrete_constants(_),ConstID,Res) :- !,Res=ConstID. | |
450 | get_constants_id(_,_,-1). | |
451 | ||
452 | /** | |
453 | Get the predicate representation of a BState | |
454 | ||
455 | #### called by: | |
456 | * ProB 2.0: GetBStateCommand | |
457 | */ | |
458 | get_b_state(StateId, BState) :- | |
459 | get_state(StateId, S), translate_bstate(S, BState). | |
460 | ||
461 | /** | |
462 | Compute the enabled operations (without the backtrack options) for a given state id. | |
463 | Transitions is a list of operation tuples with the form op(TransitionId,SrcId,DestId) | |
464 | ||
465 | #### called by: | |
466 | * ProB 2.0: GetEnabledOperationsCommand | |
467 | */ | |
468 | :- mode compute_operations_for_state(+StateID,-Transitions). | |
469 | compute_operations_for_state(StateID, Transitions) :- | |
470 | visited_expression_id(StateID), | |
471 | user:tcltk_compute_options(StateID,OpsSTAndIDs), | |
472 | (create_simple_op_terms(OpsSTAndIDs,StateID,Transitions) -> true | |
473 | ; add_error_and_fail(prob2_interface, 'Creating op terms failed', OpsSTAndIDs)). | |
474 | ||
475 | create_simple_op_terms([],_,[]). | |
476 | create_simple_op_terms([(Id,Op,Dst)|T],StateID,[op(Id,Name,StateID,Dst)|FT]) :- | |
477 | extract_op_name(Op,Name), | |
478 | create_simple_op_terms(T,StateID,FT). | |
479 | ||
480 | set_current_state(ID) :- current_state_id(ID),!. % no need to jump | |
481 | set_current_state(ID) :- /* jumps to the given node; can be backtracked */ | |
482 | visited_expression_id(ID), | |
483 | user:tcltk_goto_state(jump,ID). | |
484 | ||
485 | /** | |
486 | Calculates an operation given a predicate from the user. | |
487 | ||
488 | #### called by: | |
489 | * ProB 2.0: GetOperationByPredicateCommand | |
490 | */ | |
491 | :- use_module(bmachine,[b_is_operation_name/1]). | |
492 | :- mode prob2_execute_custom_operations(+CurID, +OpName, +ParsedPredicate, +MaxNrOfSolutions, -TOperations, -Errors). | |
493 | prob2_execute_custom_operations(_CurID, _OpName, _Pred, MaxNrOfSolutions, TOps, Errs) :- | |
494 | MaxNrOfSolutions < 1, | |
495 | !, | |
496 | TOps = [],Errs = ['max nr of solutions too small']. | |
497 | prob2_execute_custom_operations(_CurID, OpName, _Pred, _Max, TOps, Errs) :- | |
498 | \+ valid_op_name(OpName), | |
499 | !, | |
500 | TOps = [], | |
501 | (b_is_operation_name(OpName) -> ajoin(['Not a Top-Level Operation ', OpName], Msg) | |
502 | ; ajoin(['Unknown Operation ', OpName], Msg)), | |
503 | Errs = [Msg]. | |
504 | prob2_execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut) :- | |
505 | set_current_state(CurID), | |
506 | prob2_execute_custom_operations_aux(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut). | |
507 | ||
508 | % special case for TRUE=TRUE predicate to avoid parser overhead | |
509 | prob2_execute_custom_operations_aux(CurID, OpName, Pred, MaxNrOfSolutions, TOperations, ErrorsOut) :- | |
510 | raw_truth(Pred),!, | |
511 | findall(TO, prob2_execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations), | |
512 | clear_context_state, | |
513 | (TOperations = [] | |
514 | -> gen_exec_error_message(CurID,OpName,truth,Msg), | |
515 | ErrorsOut = [Msg] | |
516 | ; ErrorsOut = []). | |
517 | prob2_execute_custom_operations_aux(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut) :- | |
518 | ( is_special_op(OpName,_) | |
519 | -> Scope = [prob_ids(visible),variables] | |
520 | ; otherwise -> b_top_level_operation(OpName), | |
521 | b_get_machine_operation(OpName,_,Parameters,_), | |
522 | Scope = [identifier(Parameters),prob_ids(visible),variables] % prob scope allows one to use identifiers for deferred set elements | |
523 | ), | |
524 | b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors), | |
525 | (Errors = [] -> | |
526 | findall(TO, prob2_execute_custom_operation_with_predicate(CurID,OpName,TypedPred,TO,MaxNrOfSolutions), | |
527 | TOperations), | |
528 | retractall(bmachine:b_machine_temp_predicate(_)), | |
529 | clear_context_state, | |
530 | (TOperations = [] | |
531 | -> gen_exec_error_message(CurID,OpName,TypedPred,Msg), | |
532 | ErrorsOut = [Msg] | |
533 | ; ErrorsOut = []) | |
534 | ; TOperations = [], | |
535 | ErrorsOut = [typechecker_errors(Errors)] | |
536 | ). | |
537 | ||
538 | gen_exec_error_message(root,OpName,_,Msg) :- \+ is_special_op(OpName,_),!, | |
539 | ajoin(['Machine is not initialised, could not execute operation ', OpName], Msg). | |
540 | gen_exec_error_message(concrete_constants(_),OpName,_,Msg) :- \+ is_special_op(OpName,_),!, | |
541 | ajoin(['Machine is not initialised, could not execute operation ', OpName], Msg). | |
542 | gen_exec_error_message(concrete_constants(_),'$setup_constants',_,Msg) :- !, | |
543 | Msg = 'Constants are already set up, could not execute SETUP_CONSTANTS '. | |
544 | gen_exec_error_message(CurID,OpName,_,Msg) :- CurID \= root, CurID \= concrete_constants(_), | |
545 | is_special_op(OpName,OpS), !, | |
546 | ajoin(['Machine is already initialised, cannot execute ', OpS], Msg). | |
547 | gen_exec_error_message(_,OpName,truth,Msg) :- !, | |
548 | (is_special_op(OpName,OpS) -> true ; OpS=OpName), | |
549 | ajoin(['Could not execute operation ', OpS], Msg). | |
550 | gen_exec_error_message(_,OpName,_,Msg) :- (is_special_op(OpName,OpS) -> true ; OpS=OpName), | |
551 | ajoin(['Could not execute operation ', OpS, ' with additional predicate'], Msg). | |
552 | is_special_op('$setup_constants','SETUP_CONSTANTS'). | |
553 | is_special_op('$initialise_machine','INITIALISATION'). | |
554 | ||
555 | % true if a raw expression definitely represents truth | |
556 | raw_truth(equal(_,E1,E2)) :- raw_equals(E1,E2). | |
557 | raw_equals(boolean_true(_),boolean_true(_)). | |
558 | raw_equals(boolean_false(_),boolean_false(_)). | |
559 | raw_equals(integer(_,I),integer(_,I)). | |
560 | ||
561 | valid_op_name('$initialise_machine'). | |
562 | valid_op_name('$setup_constants'). | |
563 | valid_op_name(OpName) :- b_top_level_operation(OpName). | |
564 | %valid_op_name(OpName) :- b_get_promoted_machine_operations(OpName). | |
565 | ||
566 | /** | |
567 | ||
568 | Calculates a trace given a list of operation names and a list of guards. | |
569 | In case of errors, a partial trace is generated that jumps over the errornous operation / event. | |
570 | In addition, a list of integers should be given as argument that make possible to execute some | |
571 | operations in the oprations list multiple times or as long as they are disabled (in this case one should give -1). | |
572 | E.g. by calling prob2_construct_trace(0,[e1,e2,e3],[TRUE,TRUE,TRUE],[2,1,-1],OpsOut,ErrOut) the predicate calculates | |
573 | a trace starting at the state with the ID 0 where e1 is executed sequentially 2 times, after that e2 once, | |
574 | and finally e3 until it becomes disabled. | |
575 | ||
576 | #### called by: | |
577 | * ProB 2.0: ConstructTraceCommand | |
578 | */ | |
579 | ||
580 | prob2_construct_trace(CurId,Names,Preds,Nrs,OpsOut,ErrOut) :- | |
581 | construct_trace(CurId,Names,Preds,Nrs,[],OpsOut,[],ErrOut). | |
582 | ||
583 | construct_trace(_CurId,[],[],[],OpsOut,OpsOut,ErrOut,ErrOut). | |
584 | construct_trace(CurId,[Name|Names],[Pred|Preds],[NrName|NrNames],CurOpsOut,OpsOut,CurErrOut,ErrOut) :- | |
585 | execute_nr_of_custom_operations(CurId,Name,Pred,NrName,NewId,ListOfOps,ListOfErrs), | |
586 | append(CurOpsOut,ListOfOps,NewOpsOut), | |
587 | append(CurErrOut,ListOfErrs,NewErrOut), | |
588 | construct_trace(NewId,Names,Preds,NrNames,NewOpsOut,OpsOut,NewErrOut,ErrOut). | |
589 | ||
590 | execute_nr_of_custom_operations(CurId,_Name,_Pred,0,CurId,[],[]). | |
591 | execute_nr_of_custom_operations(CurId,Name,Pred,Nr,NewId,ListOfOps,ListOfErrs) :- | |
592 | ( Nr = -1 -> | |
593 | execute_until_disabled(CurId,Name,Pred,NewId,ListOfOps,ListOfErrs) | |
594 | ; otherwise -> % Nr is greater than 0 | |
595 | prob2_execute_custom_operations(CurId,Name,Pred,1,ListContainingSingleOp,SingleErr), | |
596 | ( ListContainingSingleOp = [] -> | |
597 | NextId=CurId | |
598 | ; ListContainingSingleOp = [op(_Trans,_Name,_From,To)], | |
599 | NextId = To | |
600 | ), | |
601 | append(ListContainingSingleOp,Ops,ListOfOps), | |
602 | append(SingleErr,Errs,ListOfErrs), | |
603 | NewNr is Nr - 1, | |
604 | execute_nr_of_custom_operations(NextId,Name,Pred,NewNr,NewId,Ops,Errs) | |
605 | ). | |
606 | ||
607 | ||
608 | execute_until_disabled(CurId,OpName,Pred,NewId,ListOfOps,ListOfErrs) :- | |
609 | execute_until_disabled(CurId,OpName,Pred,NewId,[],ListOfOps,ListOfErrs). | |
610 | ||
611 | execute_until_disabled(CurId,OpName,Pred,NewId,CurListOfOps,ListOfOps,ListOfErrs) :- | |
612 | prob2_execute_custom_operations(CurId,OpName,Pred,1,ListContainingSingleOp,SingleErr), | |
613 | ( ListContainingSingleOp = [] -> % reached a state where OpName is not executed | |
614 | NewId=CurId, | |
615 | ListOfOps=CurListOfOps, | |
616 | ajoin(['Could not execute Operation ', OpName, ' with additional predicate'], Msg), | |
617 | (member(Msg,SingleErr) -> % Error message generated because OpName is disabled at some state | |
618 | ListOfErrs = [] | |
619 | ; otherwise -> % unexpected error occurred, need to be reported | |
620 | ListOfErrs = SingleErr | |
621 | ) | |
622 | ; ListContainingSingleOp = [op(Trans,Name,From,To)], | |
623 | ( member(op(_T,_N,To,_To),CurListOfOps) -> % in case of a loop we terminate, otherwise we will go forever | |
624 | ListOfOps = CurListOfOps, | |
625 | NewId=From | |
626 | ; otherwise -> | |
627 | NextId = To, | |
628 | append(CurListOfOps,[op(Trans,Name,From,To)],NewCurListOfOps), | |
629 | execute_until_disabled(NextId,OpName,Pred,NewId,NewCurListOfOps,ListOfOps,ListOfErrs) | |
630 | ) | |
631 | ). | |
632 | ||
633 | % TO DO: check if we need to recompute the operation effect: if the ParsedPredicate is TRUE | |
634 | % (TRUE = equal(none,integer(none,1),integer(none,1)) ) & MaxNrOfSolutions <= | |
635 | % what has already been used previously, we can simply reuse transition from the state space | |
636 | ||
637 | prob2_execute_custom_operation(CurID,OpName,Transition,Max) :- | |
638 | statistics(walltime, [CurTime1,_]), | |
639 | set_context_state(CurID), | |
640 | visited_expression(CurID,InState), | |
641 | specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max), | |
642 | % logger:writeln_log(sol(OpName,NewState)), %% | |
643 | user:add_trans_id(CurID,Operation,NewState,[],NewID,[],TransId), | |
644 | % logger:writeln_log(ids(OpName,Operation,NewID,TransId)), %% | |
645 | statistics(walltime, [CurTime2,_]), | |
646 | log_executed_operation(CurID,Operation,NewID,CurTime1,CurTime2), % TODO? : log errors as comments | |
647 | Transition = op(TransId,OpName,CurID,NewID). | |
648 | ||
649 | :- use_module(succeed_max,[succeed_max_call_id/3]). | |
650 | :- use_module(b_state_model_check,[execute_operation_by_predicate_in_state/5]). | |
651 | prob2_execute_custom_operation_with_predicate(CurID,OpName,Predicate,Transition,Max) :- | |
652 | b_top_level_operation(OpName), | |
653 | !, | |
654 | statistics(walltime, [CurTime1,_]), | |
655 | set_context_state(CurID), | |
656 | visited_expression(CurID,InState), | |
657 | succeed_max_call_id(prob2_execute_custom_operation, | |
658 | execute_operation_by_predicate_in_state(InState,OpName,Predicate,Operation,NewState),Max), | |
659 | user:add_trans_id(CurID,Operation,NewState,[],NewID,[],TransId), | |
660 | statistics(walltime, [CurTime2,_]), | |
661 | log_executed_operation(CurID,Operation,NewID,CurTime1,CurTime2), | |
662 | Transition = op(TransId,OpName,CurID,NewID). | |
663 | prob2_execute_custom_operation_with_predicate(CurID,OpName,Predicate,Transition,MaxNrOfSolutions) :- | |
664 | retractall(bmachine:b_machine_temp_predicate(_)), % temporary fix: old style execution for INIT, setup_constants | |
665 | assert(bmachine:b_machine_temp_predicate(Predicate)), | |
666 | prob2_execute_custom_operation(CurID,OpName,Transition,MaxNrOfSolutions). | |
667 | ||
668 | :- dynamic last_trace_id/2. % if this fact is set, we assume we will log to a trace file | |
669 | ||
670 | :- use_module(preferences,[get_prob_application_type/1]). | |
671 | :- use_module(bmachine,[b_absolute_file_name_relative_to_main_machine/2]). | |
672 | :- register_event_listener(start_initialising_specification,reset_last_trace_id, | |
673 | 'Reset for logging.'). | |
674 | reset_last_trace_id :- retractall(last_trace_id(_,_)), | |
675 | (get_preference(prob2_trace_file,File),File \= '', | |
676 | get_prob_application_type(Type), Type \= tcltk, % logging not working, would overwrite Trace file | |
677 | b_absolute_file_name_relative_to_main_machine(File,AFile) | |
678 | -> reset_trace_file(AFile,WritableFile), | |
679 | assert(last_trace_id(root,WritableFile)) ; true). | |
680 | ||
681 | % log for later replay | |
682 | log_executed_operation(CurID,Operation,NewID,CurTime1,CurTime2) :- | |
683 | retract(last_trace_id(LastID,File)), !, | |
684 | (LastID=CurID -> true ; add_jump(LastID,CurID,File)), | |
685 | Delta is CurTime2 - CurTime1, | |
686 | detailed_print_to_trace_file(File,Operation,CurID,NewID,Delta), | |
687 | % TO DO: print some timing info,... in comments | |
688 | assert(last_trace_id(NewID,File)). | |
689 | log_executed_operation(_,_,_,_,_). | |
690 | ||
691 | :- use_module(state_space,[is_concrete_constants_state_id/1]). | |
692 | add_jump(X,X,_) :- !. | |
693 | add_jump(root,X,File) :- is_concrete_constants_state_id(X), % in case we missed a setup_constants | |
694 | !, print_to_trace_file(File,'$setup_constants'). | |
695 | add_jump(X,Y,File) :- nl, nl, print(add_jump(X,Y,File)),nl, | |
696 | (X=root ; is_concrete_constants_state_id(X)), % in case we missed an initialisation | |
697 | !, | |
698 | print_to_trace_file(File,'$initialise_machine'). | |
699 | add_jump(LastID,CurID,File) :- print_to_trace_file(File,'$jump'(LastID,CurID)). | |
700 | ||
701 | :- use_module(tools_printing,[print_time_stamp/1]). | |
702 | reset_trace_file(File,WritableFile) :- | |
703 | (get_preference(prob2_trace_file_gen_unique_name,true) | |
704 | -> open(File,write,Stream,[if_exists(generate_unique_name)]), | |
705 | stream_property(Stream,file_name(WritableFile)) | |
706 | ; open(File,write,Stream), WritableFile=File | |
707 | ), | |
708 | write(Stream,'% Created: '), print_time_stamp(Stream), nl(Stream), | |
709 | revision(GitRevision), | |
710 | format(Stream,'% ProB GIT revision: ~w~n',[GitRevision]), | |
711 | close(Stream). | |
712 | print_to_trace_file(File,Term) :- | |
713 | open(File,append,Stream), | |
714 | portray_clause(Stream,Term), | |
715 | close(Stream). | |
716 | detailed_print_to_trace_file(File,Term,CurID,NewID,Delta) :- | |
717 | open(File,append,Stream), | |
718 | format(Stream,'~n% Executed ~w -> ~w in ~w ms at ',[CurID,NewID,Delta]), print_time_stamp(Stream), nl(Stream), | |
719 | get_state_space_stats(NrNodes, NrTrans, NrProcessed), statistics(memory_used,V), VMb is V / 1048576, | |
720 | format(Stream,'% State space: nodes = ~w, transitions = ~w, processed = ~w, MB used: ~3f~n',[NrNodes,NrTrans,NrProcessed,VMb]), | |
721 | portray_clause(Stream,Term), % TO DO: also export in JSON format; drawback is we need to add closing brackets at the end, whereas in Prolog format we always have a valid trace file | |
722 | close(Stream). | |
723 | ||
724 | ||
725 | /** | |
726 | Extracts information about the parameters and return values for the | |
727 | specified transition. | |
728 | ||
729 | #### called by: | |
730 | * ProB 2.0: GetOpFromId | |
731 | */ | |
732 | :- mode get_op_from_id(+Id,+Truncate,-Params,-RetVals). | |
733 | get_op_from_id(Id,Truncate,Params,RetVals) :- | |
734 | transition(_Src,Op,Id,_Dest), | |
735 | create_op_tuple(Op,Truncate,Params,RetVals). | |
736 | ||
737 | /** | |
738 | Creates an operation tuple from transition id, source id, an op term, and a destination id. | |
739 | If creation is unsuccessful, an error is added and the predicate fails. | |
740 | See comment for extract_op_tuple for a description of OpTuple | |
741 | */ | |
742 | :- mode create_op_tuple(+OpTerm, +Truncate, -Params, -RetVals). | |
743 | create_op_tuple(OpTerm, Truncate, Params, RetVals) :- | |
744 | (extract_op_tuple(OpTerm, Truncate, Params, RetVals) -> true; | |
745 | add_error_and_fail(prob2_interface, 'Could not create OpTuple ', extract_op_tuple(OpTerm, Params, RetVals))). | |
746 | ||
747 | /** | |
748 | Extracts the parameters and return values of the operations | |
749 | */ | |
750 | :- mode extract_op_tuple(+OpTerm, +Truncate, -Params, -RetVals). | |
751 | extract_op_tuple(OpTerm, Truncate, Params, RetVals) :- | |
752 | (animation_mode(cspm) -> | |
753 | extract_csp_op(OpTerm, Params, RetVals) | |
754 | ; extract_b_op(OpTerm, Truncate, Params, RetVals) | |
755 | ). | |
756 | ||
757 | /** | |
758 | Extracts information for a CSP operation. | |
759 | */ | |
760 | :- mode extract_csp_op(+OpTerm, -Params, -RetVals). | |
761 | extract_csp_op(OpTerm, Params, []) :- | |
762 | %OpTuple = op(TransId, Src, Dest, Name, params(Source, Pretty), return([],[]), TargetState), /* TODO: CSP operations do not have return types, is this correct??? */ | |
763 | %extract_csp_name_and_args(OpTerm, _Name, _Source), | |
764 | translate_event(OpTerm, PPEvent), | |
765 | split_atom(PPEvent,['.','!'],[_Op|Params]). | |
766 | ||
767 | :- mode extract_csp_name_and_args(+OpTerm, -Name, -Args). | |
768 | extract_csp_name_and_args(io(Args,ChName,_SPAN),ChName,Args). | |
769 | extract_csp_name_and_args(start_cspm(Name), Name, []). | |
770 | extract_csp_name_and_args(start_cspm_MAIN,'start_cspm_MAIN',[]). | |
771 | extract_csp_name_and_args(tick(_),tick,[]). | |
772 | extract_csp_name_and_args(tau(_),tau,[]). | |
773 | extract_csp_name_and_args(_OP,'?',[]). | |
774 | ||
775 | /** | |
776 | Extracts information for a B operation. | |
777 | */ | |
778 | :- mode extract_b_op(+OpTerm, +Truncate, -Params, -RetVals). | |
779 | extract_b_op(OpTerm, Truncate, Params, RetVals) :- | |
780 | extract_b_op_infos(OpTerm, _Name, PSource, RSource), | |
781 | maplist(pretty_print_bvalue(Truncate), PSource, Params), | |
782 | maplist(pretty_print_bvalue(Truncate), RSource, RetVals). | |
783 | ||
784 | :- mode extract_b_op_infos(+Term, -Name, -Arguments, -RetVals). | |
785 | extract_b_op_infos(Term, Name, Arguments, RetVals) :- | |
786 | (Term = '-->'(OpTerm,RetVals) -> true; | |
787 | OpTerm = Term, RetVals = []), | |
788 | OpTerm =.. [Name|Arguments]. | |
789 | ||
790 | extract_op_name(OpTerm,Name) :- | |
791 | (animation_mode(cspm) -> | |
792 | extract_csp_name_and_args(OpTerm, Name, _Args) | |
793 | ; extract_b_op_infos(OpTerm, Name, _Params, _RetVals) | |
794 | ). | |
795 | ||
796 | pretty_print_bvalue_unicode(Truncate,Formula,Result) :- | |
797 | set_unicode_mode, | |
798 | call_cleanup(pretty_print_bvalue(Truncate,Formula,Result),unset_unicode_mode). | |
799 | pretty_print_bvalue(truncate,Formula,Result) :- | |
800 | translate_bvalue_with_limit(Formula,600,Result). | |
801 | %translate_bvalue(Formula, Result). | |
802 | pretty_print_bvalue(expand,Formula,Result) :- | |
803 | translate_bvalue_with_limit(Formula,-1,Result). | |
804 | ||
805 | /* ------------------------- */ | |
806 | /* Boolean Properties */ | |
807 | /* ------------------------- */ | |
808 | ||
809 | is_initialised_state(ID) :- b_mode,!, | |
810 | is_initialised_b_state(ID). | |
811 | is_initialised_state(ID) :- | |
812 | visited_expression_id(ID), ID \= root. | |
813 | ||
814 | is_initialised_b_state(ID) :- | |
815 | visited_expression(ID,State), ID \= root, | |
816 | (b_mode -> specfile:state_corresponds_to_initialised_b_machine(State) ; true). | |
817 | ||
818 | ||
819 | invariantKO(StateID) :- is_initialised_state(StateID), | |
820 | get_state(StateID,State), | |
821 | user:check_invariantKO(StateID,State), | |
822 | state_space:invariant_violated(StateID). | |
823 | ||
824 | /** | |
825 | Takes a state id and finds all of the operations for which a timeout occurred | |
826 | ||
827 | #### called by: | |
828 | * ProB Plugin: GetTimeoutedOperationsCommand | |
829 | * ProB 2.0: GetOperationsWithTimeout | |
830 | */ | |
831 | op_timeout_occurred(StateID,OpNameList) :- | |
832 | findall(OpName,time_out_for_node(StateID,OpName,_Type),OpNameList). | |
833 | ||
834 | inv_timeout_occurred(StateID) :- time_out_for_invariant(StateID). | |
835 | timeout_occurred(StateID) :- time_out_for_node(StateID). | |
836 | max_operations_reached(StateID) :- max_reached_for_node(StateID). | |
837 | ||
838 | /** | |
839 | Finds the status for a given property | |
840 | Properties can be: invariantKO, timeout_occurred, max_operations_reached, initialised | |
841 | Statuses are expected to be boolean values: either true or false | |
842 | ||
843 | #### called by: | |
844 | * ProB Plugin: CheckBooleanPropertyCommand | |
845 | * ProB 2.0: CheckBooleanPropertyCommand | |
846 | */ | |
847 | :- mode state_property(+Property,+StateId,-Status). | |
848 | state_property(Property,StateId,Status) :- | |
849 | ( state_property2(Property,StateId) -> Status = true | |
850 | ; otherwise -> Status = false). | |
851 | state_property2(invariantKO,StateId) :- invariantKO(StateId). | |
852 | state_property2(timeout_occurred,StateId) :- inv_timeout_occurred(StateId) ; timeout_occurred(StateId). | |
853 | state_property2(max_operations_reached,StateId) :- max_operations_reached(StateId). | |
854 | state_property2(valid_state,StateId) :- visited_expression(StateId, _State). | |
855 | state_property2(initialised,StateId) :- | |
856 | (specfile:csp_mode -> | |
857 | true % in CSP the content of the state is irrelevant for the semantic of the state space | |
858 | ; is_initialised_state(StateId) | |
859 | ). | |
860 | ||
861 | ||
862 | /** | |
863 | Takes a id for a given state in the state space and produces a list of all | |
864 | state based errors. | |
865 | ||
866 | #### called by: | |
867 | * ProB Plugin: GetStateBasedErrorsCommand | |
868 | * ProB 2.0: GetStateBasedErrorsCommand | |
869 | */ | |
870 | :- mode get_state_errors(+StateId,-Errors). | |
871 | get_state_errors(StateId,Errors) :- | |
872 | findall(E, (state_error(StateId,_,E),E \== invariant_violated), Errs), | |
873 | convert_errors(Errs,Errors). | |
874 | convert_errors([],[]). | |
875 | convert_errors([Error|InRest],[error(Event,Short,Long)|OutRest]) :- | |
876 | ( Error = eventerror(Event,EError,Trace) -> | |
877 | translate_event_error(EError,Short), | |
878 | explain_event_trace(Trace,LongStr), | |
879 | safe_atom_codes(Long,LongStr) | |
880 | ; otherwise -> | |
881 | Event = '*unknown*', | |
882 | translate_state_error(Error,Short), | |
883 | explain_state_error(Error,_Span,LongStr), | |
884 | safe_atom_codes(Long,LongStr)), | |
885 | convert_errors(InRest,OutRest). | |
886 | ||
887 | /* ------------------------- */ | |
888 | /* Evaluate Formulas */ | |
889 | /* ------------------------- */ | |
890 | ||
891 | % term in string (see String argument) should be terminated by full-stop!!! | |
892 | evaluate_csp_expression_string(PlClause,R) :- | |
893 | read_from_codes(PlClause,PlTerm), | |
894 | evaluate_csp_expression_aux(PlTerm,R). | |
895 | ||
896 | evaluate_csp_expression_aux(PlTerm,R) :- | |
897 | haskell_csp:evaluate_expression(PlTerm,Res), | |
898 | translate:translate_cspm_expression(Res, R). | |
899 | evaluate_csp_expression_aux(Other,_R) :- | |
900 | add_error_and_fail(prob2_interface, 'Unexpected CSP Expression: ', Other). | |
901 | ||
902 | /** | |
903 | Evaluate a formula given a state id and the raw prolog representation of the formula | |
904 | ||
905 | #### Params: | |
906 | * StateId - state for which the formula should be evaluated | |
907 | * Element - Triple in the form eval(Formula,Type,Code) | |
908 | * Formula - Prolog representation of non-typechecked formula | |
909 | * Type - csp,'#PREDICATE',or '#EXPRESSION' | |
910 | * Code - String representation of Formula | |
911 | * Truncate - if the result should be truncated or expanded | |
912 | * Result - Triple result(Value,Solutions,Code) | |
913 | * Value - String rep of the value calculated by ProB or tuple: v(SRes,Term) | |
914 | * SRes - String rep of the value calculated by ProB | |
915 | * Term - Prolog representation of the value | |
916 | * Solutions - List of solutions as a triple: bind(Name,Solution,PPSol) | |
917 | * Name - String free variable from formula | |
918 | * Solution - Prolog representation of the solution bound to the name | |
919 | * PPSol - String representation of the solution bound to the name | |
920 | * Code - String representation of evaluated formula | |
921 | ||
922 | #### called by: | |
923 | ProB 2.0: EvaluateFormulaCommand | |
924 | */ | |
925 | ||
926 | :- mode evaluate_formula(+StateId,+Element,-R). | |
927 | evaluate_formula(StateId,Element,R) :- | |
928 | get_state_with_deferred_sets(StateId,State,Kind,_), | |
929 | evaluate_formula_in_state(Kind,State,StateId,Element,R). | |
930 | ||
931 | % a list version of the above: advantage: state expanded only once | |
932 | :- mode evaluate_formulas(+StateId,+Elements,-Results). | |
933 | evaluate_formulas(StateId,Elements,Rs) :- | |
934 | get_state_with_deferred_sets(StateId,State,Kind,_ConstID), | |
935 | maplist(inline_machine(_Machine),Elements,Elements2), | |
936 | maplist(evaluate_formula_in_state(Kind,State,StateId),Elements2,Rs). | |
937 | ||
938 | % detect all expressions and insert machine term variable to avoid generating term multiple times | |
939 | % TO DO: maybe also inline Typechecker's type environment | |
940 | inline_machine(Machine,eval(Raw,Type,Code,Truncate),eval(Raw,for_machine(Machine,Type),Code,Truncate)) :- | |
941 | Type \= csp, !. | |
942 | inline_machine(_,E,E). | |
943 | ||
944 | :- use_module(runtime_profiler,[profile_single_call/3]). | |
945 | :- meta_predicate myprofile(-,-,0). | |
946 | myprofile(_,_,Call) :- call(Call). | |
947 | %myprofile(Source,StateId,Call) :- profile_single_call(Source,StateId,Call). | |
948 | evaluate_formula_in_state(_Kind, _State,_StateId, eval(Raw,csp,Code,_Truncate), R) :- !, | |
949 | ( evaluate_csp_expression_string(Raw,Res) -> | |
950 | R = result(Res,[]); | |
951 | R = [Code,"Unexpected CSP Expression"]). | |
952 | evaluate_formula_in_state(StateKind,State,StateId, eval_typed(Typed,Truncate), R) :- !, | |
953 | get_texpr_type(Typed, Type), | |
954 | myprofile(prob2_evaluate_typed_formula,StateId, | |
955 | prob2_interface:evaluate_typechecked_b_formula_in_state(StateKind,formula(Typed),State,Typed,Type,Truncate,R)). | |
956 | evaluate_formula_in_state(StateKind, State,StateId, eval(Raw,PredOrExpr,Code,Truncate), R) :- | |
957 | %logger:writeln_log_time(typechecking_raw(PredOrExpr)), | |
958 | myprofile(Raw,StateId, | |
959 | prob2_interface:evaluate_formula_typecheck2(PredOrExpr,Raw,Typed,Type,Errors)), | |
960 | %logger:writeln_log_time(evaluate_typechecked_b_formula_in_state(StateKind)), | |
961 | ( Errors=[] -> | |
962 | %print('EVAL:'),nl,translate:print_bexpr(Typed),nl, | |
963 | myprofile(prob2_evaluate_formula,StateId, | |
964 | prob2_interface:evaluate_typechecked_b_formula_in_state(StateKind,formula(Typed),State,Typed,Type,Truncate,R)) | |
965 | ; R = [Code|Errors]). | |
966 | ||
967 | get_state_with_deferred_sets(StateId,State,Kind,ConstID) :- | |
968 | get_state(StateId, State1,Kind,ConstID), % TO DO: we could try and get only those identifiers that are really used | |
969 | add_prob_deferred_set_elements_to_store(State1, State, visible). | |
970 | ||
971 | /** | |
972 | Type checks a given formula. | |
973 | ||
974 | #### Params: | |
975 | * PredOrExpr - '#PREDICATE' or '#EXPRESSION' | |
976 | * RawFormula - Prolog representation of non-typechecked formula | |
977 | * TypedFormula - Prolog representation of typechecked formula | |
978 | * Type - type of formula | |
979 | * Errors - any errors that have occured during typechecking | |
980 | ||
981 | #### called by: | |
982 | ProB 2.0: EvaluateFormulaCommand | |
983 | */ | |
984 | % can be expensive for big machines, as typechecking calls full_b_machine (20-30 ms for ZC scheduler) | |
985 | ||
986 | :- mode evaluate_formula_typecheck(+PredOrExpr,+RawFormula,-TypedFormula,-Type,-Errors). | |
987 | evaluate_formula_typecheck(PredOrExpr,RawFormula,TypedFormula,PPType,Errors) :- | |
988 | evaluate_formula_typecheck2(PredOrExpr,RawFormula,TypedFormula,Type,Errors), | |
989 | translate:pretty_type(Type,PPType). | |
990 | evaluate_formula_typecheck(PredOrExpr,RawFormula,TypedFormula,Errors) :- | |
991 | evaluate_formula_typecheck2(PredOrExpr,RawFormula,TypedFormula,_Type,Errors). | |
992 | ||
993 | :- use_module(bmachine,[b_is_variable/2, b_is_constant/2, b_type_expression_for_full_b_machine/6]). | |
994 | % this predicate returns the internal Prolog type: | |
995 | :- mode evaluate_formula_typecheck2(+PredOrExpr,+RawFormula,-TypedFormula,-Type,-Errors). | |
996 | evaluate_formula_typecheck2('#PREDICATE',Raw,Typed,Type,Errors) :- | |
997 | !, get_eval_scope(Scope), | |
998 | b_type_open_predicate(open(exists),Raw,Scope,Typed,PErrors), | |
999 | convert_perrors(PErrors, Errors), | |
1000 | Type=pred. | |
1001 | evaluate_formula_typecheck2(for_machine(M,'#PREDICATE'),Raw,Typed,Type,Errors) :- | |
1002 | !,get_eval_scope(Scope), | |
1003 | bmachine:b_type_open_predicate_for_full_b_machine(M,open(exists),Raw,Scope,Typed,PErrors), | |
1004 | convert_perrors(PErrors, Errors), | |
1005 | Type=pred. | |
1006 | evaluate_formula_typecheck2('#EXPRESSION',identifier(Pos,ID),Typed,Type,Errors) :- | |
1007 | (b_is_variable(ID,Type) ; b_is_constant(ID,Type)), | |
1008 | !, % hack to avoid type-checking simple identifiers which just need to be looked up in state | |
1009 | Errors=[], Typed = b(identifier(ID),Type,[nodeid(Pos)]). | |
1010 | evaluate_formula_typecheck2('#EXPRESSION',Raw,Typed,Type,Errors) :- | |
1011 | !,get_eval_scope(Scope), | |
1012 | b_type_expression(Raw,Scope,Type,Typed,PErrors), | |
1013 | convert_perrors(PErrors, Errors). | |
1014 | evaluate_formula_typecheck2(for_machine(_M,'#EXPRESSION'),identifier(Pos,ID),Typed,Type,Errors) :- | |
1015 | (b_is_variable(ID,Type) ; b_is_constant(ID,Type)), | |
1016 | !, % hack to avoid type-checking simple identifiers which just need to be looked up in state | |
1017 | Errors=[], Typed = b(identifier(ID),Type,[nodeid(Pos)]). | |
1018 | evaluate_formula_typecheck2(for_machine(M,'#EXPRESSION'),Raw,Typed,Type,Errors) :- | |
1019 | !,get_eval_scope(Scope), | |
1020 | b_type_expression_for_full_b_machine(M,Raw,Scope,Type,Typed,PErrors), | |
1021 | convert_perrors(PErrors, Errors). | |
1022 | evaluate_formula_typecheck2(Else,_Raw,_Typed,_Type,_Errors) :- | |
1023 | add_error_and_fail(prob2_interface,'expected #PREDICATE or #EXPRESSION instead of:', Else),fail. | |
1024 | ||
1025 | % get scope for typechecker: | |
1026 | get_eval_scope([prob_ids(visible),Scope]) :- get_main_eval_scope(Scope). | |
1027 | get_main_eval_scope(assertions_scope) :- get_preference(allow_operation_calls_in_expr,true),!. | |
1028 | get_main_eval_scope(variables). | |
1029 | ||
1030 | % FIXME This is a bit hacky, it would be better to implement this properly in error_manager. | |
1031 | convert_perrors(PErrors, Errors) :- | |
1032 | add_all_perrors(PErrors), | |
1033 | get_all_errors_with_span_info_and_reset(Errors). | |
1034 | ||
1035 | :- use_module(tools_meta,[safe_time_out/3]). | |
1036 | %evaluate_typechecked_b_formula(StateId,Typed,Type,Truncate,Result) :- | |
1037 | % get_state_with_deferred_sets(StateId,State), | |
1038 | % evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result). | |
1039 | ||
1040 | evaluate_typechecked_b_formula_in_state(StateKind,Requirements,State,Typed,Type,Truncate,Result) :- | |
1041 | (requirements_met(Requirements,StateKind) -> | |
1042 | evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result) | |
1043 | ; Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[]) | |
1044 | ). | |
1045 | evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result) :- | |
1046 | % should we use get_computed_preference(debug_time_out,DTO) instead of 1000 ? | |
1047 | % there seem to be two uses in ProB2: for state view, where we want a short time out, and LISB or maybe REPL where we want a longer time out or no time out | |
1048 | (Truncate=truncate -> TO = 1000, FORCE=limit(10000) ; TO = 30000, FORCE=force), | |
1049 | safe_time_out(evaluate_formula_eval(Type,State,Typed,FORCE,Res,Solution,EnumWarning),TO,TimeOutRes), | |
1050 | (TimeOutRes=time_out -> Res=time_out, EnumWarning=false ; true), | |
1051 | get_error_messages(_WarningsOnly,Errors), | |
1052 | extract_result(EnumWarning,Errors,Res,Solution,Truncate,Result). | |
1053 | ||
1054 | extract_result(true,_,_,_,_,enum_warning). | |
1055 | extract_result(_EnumW,[],v(_SRes,Term),[],Truncate,Result) :- % v/2 for value | |
1056 | pretty_print_bvalue_unicode(Truncate,Term,R), | |
1057 | Result = result(R,[]). | |
1058 | extract_result(_EnumW,[],SRes,Solutions,Truncate,Result) :- | |
1059 | prettyprint_solutions(Truncate,Solutions,PPSol), | |
1060 | Result = result(SRes,PPSol). | |
1061 | extract_result(_EnumW,Errors,v(SRes,_),_Sol,_Truncate,Result) :- | |
1062 | Result = errors(SRes, Errors). | |
1063 | extract_result(_EnumW,Errors,SRes,_Sol,_Truncate,Result) :- | |
1064 | Result = errors(SRes, Errors). | |
1065 | ||
1066 | %:- use_module(eval_strings,[eval_predicate/5]). % TODO: export and refactor | |
1067 | % TO DO: move this into another more general module: | |
1068 | evaluate_formula_eval(pred,State,Typed,_,Res,LocalState,EnumWarning) :- | |
1069 | !,catch_enumeration_warning_exceptions( | |
1070 | (eval_predicate(State,Typed,Res,EnumWarning,LocalState)->true), | |
1071 | (Res = time_out,EnumWarning = true)). | |
1072 | evaluate_formula_eval(_Type,State,Typed,FORCE,Res,[],EnumWarning) :- | |
1073 | catch_enumeration_warning_exceptions( | |
1074 | (evaluate_expression(State,Typed,FORCE,SRes,Term)->EnumWarning=false), | |
1075 | (SRes = time_out, EnumWarning = true)), | |
1076 | Res = v(SRes,Term). | |
1077 | ||
1078 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]). | |
1079 | :- use_module(error_manager,[enter_new_error_scope/2, exit_error_scope/3,clear_all_errors_in_error_scope/1, | |
1080 | event_occurred_in_error_scope/1]). | |
1081 | :- use_module(store,[normalise_value_for_var/4]). | |
1082 | % a simplified version of eval_strings:eval_expression | |
1083 | % evaluate an expression Typed in an expanded state EState giving string result Result and Prolog value NValue | |
1084 | % FORCE = force or e.g. limit(10000) | |
1085 | evaluate_expression(EState,Typed,FORCE,Result,NValue) :- | |
1086 | enter_new_error_scope(ScopeID,evaluate_expression), | |
1087 | clear_all_errors_in_error_scope(ScopeID), | |
1088 | %replace_expression_by_kodkod_if_enabled(Typed,Typed2), | |
1089 | catch_clpfd_overflow_call2(b_interpreter:b_compute_expression_nowf(Typed,[],EState,Value),fail), % We could return CLPFD overflow error result | |
1090 | !, | |
1091 | %logger:writeln_log_time(normalise_value_for_var(evaluate_expression)), | |
1092 | normalise_value_for_var(evaluate_expression,FORCE,Value,NValue), | |
1093 | exit_error_scope(ScopeID,ErrOcc,evaluate_expression), | |
1094 | (ErrOcc=true % TO DO: check which kind of error occured | |
1095 | -> Result = 'NOT-WELL-DEFINED' | |
1096 | ; translate:translate_bvalue_for_expression(NValue,Typed,Result) | |
1097 | ). | |
1098 | evaluate_expression(_,_,_,'NOT-WELL-DEFINED',error) :- | |
1099 | exit_error_scope(_ScopeID,_,evaluate_expression). | |
1100 | ||
1101 | % a simplified version of eval_strings:eval_predicate_aux | |
1102 | ||
1103 | eval_predicate(State, ExTyped,Result,EnumWarning,LocalState) :- | |
1104 | enter_new_error_scope(ScopeID,eval_predicate), clear_all_errors_in_error_scope(ScopeID), | |
1105 | (catch_clpfd_overflow_call2(prob2_interface:eval_predicate2(State, ExTyped,LocalState), | |
1106 | fail) | |
1107 | -> Res='TRUE', EnumWarning=false | |
1108 | ; event_occurred_in_error_scope(enumeration_warning(_,_,_,_,_Critical)) | |
1109 | -> Res= 'NOT-WELL-DEFINED', EnumWarning=true | |
1110 | ; Res='FALSE', EnumWarning=false | |
1111 | ), | |
1112 | exit_error_scope(ScopeID,ErrOcc,eval_predicate), | |
1113 | (ErrOcc=true % TO DO: check which kind of error occured | |
1114 | -> Result = 'NOT-WELL-DEFINED' | |
1115 | ; Result = Res | |
1116 | ). | |
1117 | ||
1118 | eval_predicate2(State, ExTyped,LocalState) :- | |
1119 | eval_strings:is_existential_quantifier(ExTyped,Parameters,Typed), % TO DO: move to module | |
1120 | !, | |
1121 | test_bool_exists(State, Parameters,Typed,LocalState). | |
1122 | eval_predicate2(State, Typed,LocalState) :- LocalState=[], | |
1123 | b_interpreter:b_test_boolean_expression_wf(Typed,LocalState,State). | |
1124 | ||
1125 | test_bool_exists(EState, Parameters,Typed,LocalState) :- | |
1126 | kernel_waitflags:init_wait_flags(WF), | |
1127 | b_interpreter:set_up_typed_localstate(Parameters,_FreshOutputVars,TypedVals,[],LocalState,positive), | |
1128 | b_enumerate:b_tighter_enumerate_values(TypedVals,WF), | |
1129 | b_interpreter:b_test_boolean_expression(Typed,LocalState,EState,WF), | |
1130 | kernel_waitflags:ground_wait_flags(WF). | |
1131 | ||
1132 | :- dynamic prob2_formula/4. | |
1133 | :- dynamic inactive_prob2_formula/1. | |
1134 | ||
1135 | /** | |
1136 | Type checks a specified formula and asserts so that it can be found later | |
1137 | and evaluated later. | |
1138 | ||
1139 | #### called by: | |
1140 | * ProB 2.0: RegisterFormulaCommand | |
1141 | */ | |
1142 | ||
1143 | :- mode register_prob2_formula(+FormulaUUID, +Formula). | |
1144 | register_prob2_formula(FormulaUUID, _) :- prob2_formula(FormulaUUID,_,_,_),!. | |
1145 | register_prob2_formula(FormulaUUID, eval(Raw,PredOrExpr,Truncate)) :- | |
1146 | evaluate_formula_typecheck(PredOrExpr,Raw,Typed,Errors), | |
1147 | ( Errors=[] -> | |
1148 | register_prob2_formula2(FormulaUUID, Typed, Truncate) | |
1149 | ; otherwise -> | |
1150 | add_error_and_fail(register_prob2_formula, 'Type-Errors: ', Errors) | |
1151 | ). | |
1152 | register_prob2_formula(FormulaUUID, eval_typed(Typed,Truncate)) :- | |
1153 | register_prob2_formula2(FormulaUUID,Typed,Truncate). | |
1154 | ||
1155 | :- use_module(bmachine, [determine_type_of_formula/2]). | |
1156 | register_prob2_formula2(FUUID, Typed, Truncate) :- | |
1157 | determine_type_of_formula(Typed,Requirements), | |
1158 | assert(prob2_formula(FUUID, Typed, Truncate,Requirements)). | |
1159 | ||
1160 | :- mode register_prob2_formulas(+FormulaUUIDs, +Formulas). | |
1161 | register_prob2_formulas(FormulaUUIDs,Formulas) :- | |
1162 | maplist(inline_machine(_Machine),FormulaUUIDs,FormulaUUIDs2), | |
1163 | maplist(register_prob2_formula,FormulaUUIDs2,Formulas). | |
1164 | ||
1165 | ||
1166 | % TO DO: determine upon registering whether a formula reads nothing, just constants, or also variables | |
1167 | ||
1168 | % unregister a single or a list of formula ids: | |
1169 | unregister_prob2_formula(FormulaUUID) :- retractall(prob2_formula(FormulaUUID,_,_,_)). | |
1170 | unregister_prob2_formulas(Fs) :- maplist(unregister_prob2_formula,Fs). | |
1171 | ||
1172 | % mark certain formulas as inactive; will not be computed by evaluate_registered_formula | |
1173 | % useful when certain information currently not needed (e.g., in state view the formula is not visible/shown) | |
1174 | deactivate_prob2_formulas(Fs) :- maplist(deactivate_prob2_formula,Fs). | |
1175 | deactivate_prob2_formula(FormulaUUID) :- prob2_formula(FormulaUUID,_,_,_),!, | |
1176 | (inactive_prob2_formula(FormulaUUID) -> print(formula_already_inactive(FormulaUUID)),nl | |
1177 | ; assert(inactive_prob2_formula(FormulaUUID))). | |
1178 | deactivate_prob2_formula(FormulaUUID) :- | |
1179 | add_internal_error('Cannot deactivate unknown formula: ',deactivate_prob2_formula(FormulaUUID)). | |
1180 | ||
1181 | % mark certain formulas as active again; will not be computed by evaluate_registered_formula | |
1182 | activate_prob2_formulas(Fs) :- maplist(activate_prob2_formula,Fs). | |
1183 | activate_prob2_formula(FormulaUUID) :- prob2_formula(FormulaUUID,_,_,_),!, | |
1184 | (retract(inactive_prob2_formula(FormulaUUID)) -> true ; print(formula_already_active(FormulaUUID)),nl). | |
1185 | activate_prob2_formula(FormulaUUID) :- add_internal_error('Cannot activate unknown formula: ',activate_prob2_formula(FormulaUUID)). | |
1186 | ||
1187 | /** | |
1188 | Takes a state id and a list of formula ids (that were registered already) | |
1189 | via register_prob2_formula predicate. Then it evaluates all of the formulas | |
1190 | for the given state id. | |
1191 | ||
1192 | #### called by: | |
1193 | * ProB 2.0: EvaluateRegisteredFormulasCommand | |
1194 | */ | |
1195 | :- mode evaluate_registered_formulas(+StateId, +FormIds, -Results). | |
1196 | evaluate_registered_formulas(StateId,FormIds,Results) :- | |
1197 | get_state_with_deferred_sets(StateId,State,Kind,ConstID), | |
1198 | maplist(evaluate_registered_formula(State,Kind,ConstID), FormIds, Results). | |
1199 | ||
1200 | :- use_module(probsrc(bsyntaxtree),[get_texpr_type/2]). | |
1201 | evaluate_registered_formula(_,_,_,FormulaUUID,Result) :- inactive_prob2_formula(FormulaUUID),!, | |
1202 | Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[]). % TO DO: maybe other return value | |
1203 | %evaluate_registered_formula(State,StateKind,FormulaUUID,Result) :- | |
1204 | % prob2_formula(FormulaUUID,Typed,Truncate,Requirements),!, | |
1205 | % tools:ajoin([Requirements,':',StateKind],R), Result = result(R,[]). | |
1206 | evaluate_registered_formula(State,StateKind,ConstID,FormulaUUID,Result) :- | |
1207 | prob2_formula(FormulaUUID,Typed,Truncate,Requirements),!, | |
1208 | get_texpr_type(Typed,Type), | |
1209 | (cached_registered_formula_result(FormulaUUID,ConstID,R) -> Result = R | |
1210 | ; requirements_met(Requirements,StateKind) -> | |
1211 | evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result), | |
1212 | store_result_in_cache(Requirements,ConstID,FormulaUUID,Type,Result) | |
1213 | ; StateKind=requires_constants -> | |
1214 | Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[]) %Result = errors('CONSTANTS NOT INITIALISED',[]) | |
1215 | ; Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[])). | |
1216 | evaluate_registered_formula(_State,_StateKind,_ConstID,FormulaUUID,Result) :- | |
1217 | add_error(prob2_interface,'Unknown formula id:',FormulaUUID), | |
1218 | Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[]). | |
1219 | ||
1220 | % check whether we can evaluate the formula in the state: | |
1221 | requirements_met(requires_nothing,_). | |
1222 | requirements_met(requires_constants,constants_only_state). | |
1223 | requirements_met(requires_constants,full_initialised_state). | |
1224 | requirements_met(requires_variables,full_initialised_state). | |
1225 | requirements_met(formula(Typed),State) :- | |
1226 | (State=full_initialised_state -> true | |
1227 | ; determine_type_of_formula(Typed,Requirements), requirements_met(Requirements,State)). | |
1228 | ||
1229 | :- dynamic cached_registered_formula_result/3. | |
1230 | store_result_in_cache(requires_nothing,ConstID,FormulaUUID,Type,Result) :- cache_this_type(Type), !, | |
1231 | assert(cached_registered_formula_result(FormulaUUID,ConstID,Result)). | |
1232 | store_result_in_cache(requires_constants,ConstID,FormulaUUID,Type,Result) :- cache_this_type(Type), ConstID>=0,!, | |
1233 | assert(cached_registered_formula_result(FormulaUUID,ConstID,Result)). | |
1234 | store_result_in_cache(_,_,_,_,_). | |
1235 | ||
1236 | cache_this_type(pred). % currently we only cache predicates, anyway: it makes no sense to cache identifiers (their values are stored in the state anyway) | |
1237 | ||
1238 | % return a list of nodes for the hierarchical state viewer: | |
1239 | % NODES ::= category(NAME, list(INFO), list(NODES)) | formula(AST,PP) | |
1240 | % INFO ::= expanded | propagated | |
1241 | % (expanded means: by default this category is expanded, propagated means: if it is not expanded, still show summary info) | |
1242 | ||
1243 | get_machine_formulas(Structure) :- | |
1244 | findall(category(Desc,Infos,Subs),category(_,Desc,Infos,Subs),Structure). | |
1245 | ||
1246 | :- type prob2_nodes +--> (category(atomic,list(atomic),list(prob2_nodes)) ; formula(b(ground,ground,list(ground)),atomic)). | |
1247 | :- assert_must_succeed( (get_machine_formulas(S), type_check(S,list(prob2_nodes)) )). | |
1248 | ||
1249 | :- use_module(specfile,[b_mode/0, csp_mode/0, get_specification_description/2]). | |
1250 | :- use_module(probcspsrc(haskell_csp),[channel_type_list/2]). | |
1251 | :- use_module(translate,[translate_cspm_expression/2]). | |
1252 | category(Category,Desc,Infos,ProcessedSubNodes) :- b_mode, | |
1253 | b_category(Category,Infos,Subs), | |
1254 | Subs \= [], | |
1255 | get_specification_description(Category,Desc), | |
1256 | maplist(process_formula,Subs,ProcessedSubNodes). | |
1257 | category(operations,Desc,Infos,Subs) :- Infos = [], % not expanded | |
1258 | b_mode, | |
1259 | get_specification_description(operations,Desc), | |
1260 | findall(category(OpName,[propagated],Guards), get_guards(OpName,Guards), Subs), Subs \= []. | |
1261 | category(variants,Desc,Infos,Subs) :- Infos = [], % not expanded | |
1262 | b_mode, | |
1263 | get_specification_description(variants,Desc), | |
1264 | findall(category(OpNameV,[propagated],[PF]), | |
1265 | (b_get_operation_variant(OpName,ConvOrAnt,Variant), | |
1266 | (ConvOrAnt=convergent -> string_concatenate(OpName,' (<)',OpNameV) | |
1267 | ; string_concatenate(OpName,' (<=)',OpNameV)), | |
1268 | process_formula(Variant,PF)), Subs), Subs \= []. | |
1269 | category(definitions,Desc,[],Subs) :- b_mode, | |
1270 | get_specification_description(definitions,Desc), | |
1271 | findall(Def,b_definition(Def),Subs), Subs \= []. | |
1272 | category(channels,'CHANNELS',[],Channels) :- csp_mode, | |
1273 | findall( formula(b(string(ChannelDescr),string,[]),Channel), | |
1274 | (channel_type_list(Channel,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] | |
1275 | translate_cspm_expression(dotTuple(TypeList),TypeString), | |
1276 | ajoin([Channel,' : ', TypeString],ChannelDescr) | |
1277 | ), Channels). | |
1278 | ||
1279 | ||
1280 | %get_csp_datatype(bind(DT,string(TypeString))) :- | |
1281 | % haskell_csp:dataTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] | |
1282 | % translate_cspm_expression(dataTypeDef(TypeList),TypeString). | |
1283 | %get_csp_subtype(bind(DT,string(TypeString))) :- | |
1284 | % haskell_csp:subTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType] | |
1285 | % translate_cspm_expression(dataTypeDef(TypeList),TypeString). | |
1286 | ||
1287 | ||
1288 | :- use_module(translate,[translate_bexpression_to_unicode/2]). | |
1289 | process_formula(AST,formula(AST,PPString)) :- translate_bexpression_to_unicode(AST,PPString). % TO DO: we could also return location info | |
1290 | ||
1291 | :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]). | |
1292 | :- use_module(bmachine,[b_get_properties_from_machine/1,get_all_assertions_from_machine/1, | |
1293 | b_get_invariant_from_machine/1, b_get_machine_goal/1, | |
1294 | b_get_machine_heuristic_function/1, b_get_machine_searchscope/1, | |
1295 | b_get_machine_variables/1, b_get_machine_constants/1, | |
1296 | b_get_machine_set/2, b_machine_has_variables/0, | |
1297 | b_get_operation_variant/3]). | |
1298 | b_category(sets,Exp,Subs) :- findall(ST,b_get_machine_or_int_set(ST),Subs), | |
1299 | (b_machine_has_variables -> Exp = [] ; Exp=[expanded]). | |
1300 | b_category(constants,Exp,Subs) :- b_get_machine_constants(Subs), | |
1301 | (b_machine_has_variables -> Exp = [] ; Exp=[expanded]). | |
1302 | b_category(variables,[expanded],Subs) :- b_get_machine_variables(Subs). | |
1303 | b_category(properties,[],Subs) :- | |
1304 | b_get_properties_from_machine(Props), | |
1305 | conjunction_to_list(Props,Subs). | |
1306 | b_category(assertions,[],Subs) :- get_all_assertions_from_machine(Subs). | |
1307 | b_category(invariants,[],Subs) :- | |
1308 | b_get_invariant_from_machine(Inv), | |
1309 | conjunction_to_list(Inv,Subs). | |
1310 | % TO DO: add guard theorems,... | |
1311 | ||
1312 | :- use_module(specfile,[animation_minor_mode/1]). | |
1313 | b_get_machine_or_int_set(STyped) :- b_get_machine_set(_,STyped). | |
1314 | %b_get_machine_or_int_set(b(integer_set('INT'),set(integer),[])) :- | |
1315 | % \+ animation_minor_mode(_). % INT only exists in pure B mode | |
1316 | b_get_machine_or_int_set(b(interval(L,U),set(integer),[])) :- % INT is usually not expanded by interpreter: better provide interval directly | |
1317 | \+ animation_minor_mode(_), % INT only exists in pure B mode | |
1318 | % get_preference(maxint,MAXINT), get_preference(minint,MININT), | |
1319 | L = b(min_int,integer,[]), | |
1320 | U = b(max_int,integer,[]). | |
1321 | ||
1322 | :- use_module(pref_definitions,[b_get_set_pref_definition/3]). | |
1323 | :- use_module(bmachine,[b_get_machine_animation_function/2]). | |
1324 | b_definition(category('GOAL',[propagated],ProcessedSubNodes)) :- | |
1325 | b_get_machine_goal(G), | |
1326 | conjunction_to_list(G,Subs), | |
1327 | maplist(process_formula,Subs,ProcessedSubNodes). | |
1328 | b_definition(category('SCOPE',[propagated],[PF])) :- | |
1329 | b_get_machine_searchscope(F), process_formula(F,PF). | |
1330 | b_definition(category('HEURISTIC_FUNCTION',[propagated],[PF])) :- | |
1331 | b_get_machine_heuristic_function(F), process_formula(F,PF). | |
1332 | b_definition(category('ANIMATION_FUNCTIONS',[],PFS)) :- | |
1333 | findall(PF,(b_get_machine_animation_function(AF,_Nr), process_formula(AF,PF)),PFS), | |
1334 | PFS \= []. | |
1335 | b_definition(category('ANIMATION_IMAGES',[],PFS)) :- | |
1336 | get_animation_images(L), L \= [], | |
1337 | findall(formula(b(string(File),string,[]),Nr),(member(image_file(Nr,File),L)),PFS), | |
1338 | PFS \= []. | |
1339 | b_definition(category(DefName,[propagated],[PF])) :- | |
1340 | b_get_set_pref_definition(DefName,_String,F), process_formula(F,PF). | |
1341 | % TO DO: add ANIMATION Images,... ? | |
1342 | ||
1343 | :- use_module(predicate_debugger,[get_unsimplified_operation_guard/2]). | |
1344 | get_guards(OpName,ProcessedSubNodes) :- | |
1345 | get_unsimplified_operation_guard(OpName,Guard), | |
1346 | \+ is_initialisation_op(OpName), | |
1347 | conjunction_to_list(Guard,Subs), | |
1348 | maplist(process_formula,Subs,ProcessedSubNodes). | |
1349 | ||
1350 | is_initialisation_op('$setup_constants'). | |
1351 | is_initialisation_op('$initialise_machine'). | |
1352 | ||
1353 | ||
1354 | % API for showing Tk Animation Images in Java FX (or other): | |
1355 | :- use_module(state_viewer_images,[get_animation_images/1, | |
1356 | get_animation_image_grid/6, get_react_to_item_right_click_options/4, react_to_item_right_click/6]). | |
1357 | get_animation_image_list(ImageList) :- get_animation_images(ImageList). | |
1358 | % Format: [image_file(0,'images/empty_box_white.gif'),...,image_file(6,'images/F.gif')] | |
1359 | ||
1360 | get_animation_image_matrix_for_state(ID,Matrix,MinRow,MaxRow,MinCol,MaxCol) :- | |
1361 | (get_animation_image_grid(ID,M,M1,M2,M3,M4) | |
1362 | -> Matrix=M, MinRow=M1, MaxRow=M2, MinCol=M3, MaxCol=M4 | |
1363 | ; Matrix=[], MinRow = -1, MaxRow = 0, MinCol = -1, MaxCol = 0). | |
1364 | % Format: [entry(1,1,image(0)),... entry(2,3,text(some_atom)),...], entry(Row,Col,ImgOrText) | |
1365 | ||
1366 | % returns a list of atoms (strings) for the various options that are available in the state ID | |
1367 | % for Row/Col (Y/X) | |
1368 | get_react_to_item_right_click_options_for_state(ID,Row,Col,Options) :- | |
1369 | get_react_to_item_right_click_options(ID,Col,Row,Options). | |
1370 | ||
1371 | % should be called for one option provided by get_react_to_item_right_click_options_for_state | |
1372 | react_to_item_right_click_option_for_state(ID,Row,Col,Option,TransitionID,NewID) :- | |
1373 | react_to_item_right_click(ID,Col,Row,Option,TransitionID,NewID). | |
1374 | ||
1375 | % | ?- prob2_interface:get_react_to_item_right_click_options_for_state(3,1,1,L). | |
1376 | % L = ['Set(1,1,1)','Set(1,1,2)','Set(1,1,3)','Solve'|...] ? | |
1377 | % | ?- prob2_interface:react_to_item_right_click_option_for_state(3,1,1,'Set(1,1,1)',NewID). | |
1378 | % Performed: Set(int(1),int(1),int(1)) | |
1379 | % NewID = ..., TransitionID=... | |
1380 | ||
1381 | /** | |
1382 | Takes a predicate and finds a list of all state ids for which the | |
1383 | predicate holds. The states that are not intitialized (i.e. root) are | |
1384 | included in the list. The list that is returned is therefore the union | |
1385 | of the uninitialised states and the states for which the predicate holds. | |
1386 | ||
1387 | #### called by: | |
1388 | * ProB 2.0: GetStatesFromPredicate | |
1389 | */ | |
1390 | :- mode get_states_for_predicate(+Raw,-States,-Errors). | |
1391 | get_states_for_predicate(Raw,States,Errors) :- | |
1392 | evaluate_formula_typecheck('#PREDICATE',Raw,Typed,Errors), | |
1393 | findall(StateId,get_state_for_predicate(StateId,Typed),States). | |
1394 | ||
1395 | get_state_for_predicate(StateId,Typed) :- | |
1396 | state_space:visited_expression(StateId,StatePacked), | |
1397 | ( is_initialised_state(StateId) -> | |
1398 | expand_const_and_vars_to_full_store(StatePacked,State), | |
1399 | eval_predicate(State,Typed,'TRUE',_,_) | |
1400 | ; | |
1401 | true | |
1402 | ). | |
1403 | ||
1404 | /** | |
1405 | This cycles through all of the solutions and extracts the string | |
1406 | representation of the solutions. | |
1407 | */ | |
1408 | prettyprint_solutions(_Truncate,[],[]). | |
1409 | prettyprint_solutions(Truncate,[bind(Name,Res)|T],[PP|R]) :- | |
1410 | pretty_print_bvalue(Truncate,Res,PPRes), % pretty_print_bvalue_unicode ? | |
1411 | PP = solution(Name,PPRes), | |
1412 | prettyprint_solutions(Truncate,T,R). | |
1413 | ||
1414 | /** | |
1415 | Allows Strings to be parsed and evaluated. Used for EvalB | |
1416 | ||
1417 | #### called by: | |
1418 | * ProB 2.0: RemoteEvaluateCommand | |
1419 | */ | |
1420 | :- use_module(eval_strings). | |
1421 | evalb_evaluate_formula(Codes, result(R,Solutions,Quantor,Vars,Warn)):- | |
1422 | eval_strings:eval_codes(Codes,exists,R,Warn,LocalState,TypeInfo), | |
1423 | extract_typeinfo(TypeInfo,Quantor,Vars), | |
1424 | prettyprint_solutions(truncate,LocalState,Solutions). | |
1425 | ||
1426 | evalb_evaluate_tautology(Codes, result(R,Solutions,Quantor,Vars,Warn)):- | |
1427 | eval_strings:eval_codes(Codes,forall,R,Warn,LocalState,TypeInfo), | |
1428 | extract_typeinfo(TypeInfo,Quantor,Vars), | |
1429 | prettyprint_solutions(truncate,LocalState,Solutions). | |
1430 | ||
1431 | extract_typeinfo(expression(_),expression,[]). | |
1432 | extract_typeinfo(predicate(forall(BL)),forall,L) :- translate_list(BL,L). | |
1433 | extract_typeinfo(predicate(exists(BL)),exists,L) :- translate_list(BL,L). | |
1434 | extract_typeinfo(predicate(no_outer_quantifier),predicate,[]). | |
1435 | ||
1436 | translate_list([],[]). | |
1437 | translate_list([H|T],[HT|TT]) :- translate_bexpression(H,HT), translate_list(T,TT). | |
1438 | ||
1439 | /** | |
1440 | Takes a list of state ids and a predicate and finds all of the states | |
1441 | for which the predicate is true | |
1442 | ||
1443 | #### called by: | |
1444 | * ProB 2.0: FilterStatesForPredicateCommand | |
1445 | */ | |
1446 | :- mode filter_states_for_predicate(+Raw,+States,-Filtered). | |
1447 | filter_states_for_predicate(Raw,States,Filtered) :- | |
1448 | evaluate_formula_typecheck('#PREDICATE',Raw,Typed,Errors), | |
1449 | (Errors=[] -> | |
1450 | filter_states_for_typed_predicate(Typed,States,Filtered) | |
1451 | ; | |
1452 | Filtered = errors(Errors) | |
1453 | ). | |
1454 | ||
1455 | filter_states_for_typed_predicate(_,[],[]). | |
1456 | filter_states_for_typed_predicate(Typed,[Id|States],Filtered) :- | |
1457 | get_state_with_deferred_sets(Id,State,Kind,_), | |
1458 | ( Kind = full_initialised_state -> %is_initialised_state(Id) -> | |
1459 | (eval_predicate(State,Typed,'TRUE',_,_) -> | |
1460 | Filtered = [Id|Rest] ; | |
1461 | Filtered = Rest | |
1462 | ) | |
1463 | ; Filtered = [Id|Rest] | |
1464 | ), | |
1465 | filter_states_for_typed_predicate(Typed,States,Rest). | |
1466 | ||
1467 | /* ------------------------- */ | |
1468 | /* Formula Expansion */ | |
1469 | /* ------------------------- */ | |
1470 | ||
1471 | /** | |
1472 | Inserts a formula into bvisual2 module | |
1473 | The formula is inserted as a child of level "user" in bvisual2 | |
1474 | ||
1475 | #### called by: | |
1476 | * ProB 2.0: InsertFormulaForVisualizationCommand | |
1477 | */ | |
1478 | :- mode insert_formula_for_expansion(+AST,-Id). | |
1479 | insert_formula_for_expansion(Typed,Id) :- Typed = b(_,_,_),!, | |
1480 | suppress_rodin_positions, | |
1481 | bv_insert_formula(Typed,user,Id). | |
1482 | ||
1483 | insert_formula_for_expansion(AST,Id) :- | |
1484 | suppress_rodin_positions, | |
1485 | b_type_expression(AST,[variables],_,Typed,Errors), | |
1486 | ( Errors == [] -> | |
1487 | bv_insert_formula(Typed,user,Id) | |
1488 | ; otherwise -> | |
1489 | add_error_and_fail(eclipse_interface,'Could not type-check AST','')). | |
1490 | ||
1491 | /** | |
1492 | Uses the bvisual2 module to recursively expand and evaluate a specified formula. | |
1493 | This formula must first be inserted into the bvisual2 module using the predicate | |
1494 | insert_formula_for_expansion. The formula is then identified by the Id specified | |
1495 | at the time of insertion. | |
1496 | ||
1497 | #### called by: | |
1498 | * ProB 2.0: ExpandFormulaCommand | |
1499 | */ | |
1500 | :- mode expand_formula(+Id,+StateId,-Tree). | |
1501 | expand_formula(Id,StateId,Tree) :- | |
1502 | bv_expand_formula(Id,Label,Children), | |
1503 | bv_get_values([Id],StateId,[Value]), | |
1504 | bv_get_values(Children,StateId,ChildrenValues), | |
1505 | find_all_subformulas(StateId,Children,ChildrenValues,AsTrees), | |
1506 | Tree = formula(Label,Value,Id,AsTrees). | |
1507 | ||
1508 | find_all_subformulas(_,[],_,[]). | |
1509 | find_all_subformulas(StateId,[Id|RestI],[Value1|RestV],[formula(Label,Value1,Id,Trees)|RestT]) :- | |
1510 | bv_expand_formula(Id,Label,Children), | |
1511 | bv_get_values(Children,StateId,CValues), | |
1512 | find_all_subformulas(StateId,Children,CValues,Trees), | |
1513 | find_all_subformulas(StateId,RestI,RestV,RestT). | |
1514 | ||
1515 | ||
1516 | /* ------------------------- */ | |
1517 | /* Model Checking */ | |
1518 | /* ------------------------- */ | |
1519 | ||
1520 | /** | |
1521 | #### do_modelchecking(+Time,+Options,-Result,stats(-NrNodes,-NrTrans,-NrProcessed)) | |
1522 | * +Time : Timeout specified by the user in ms | |
1523 | * +Options : List of options specified by the user. Used for predicate do_modelchecking(Time,Options,Result) | |
1524 | * -NrNodes : total number of nodes in state space. Calculated with get_state_space_stats | |
1525 | * -NrTrans : total number of nodes in state space. Calculated with get_state_space_stats | |
1526 | * -NrProcessed : total number of calculated nodes in state space. Calculated with get_state_space_stats | |
1527 | When Time Milliseconds have elapsed the modelchecker should stop after its next step | |
1528 | ||
1529 | #### called by: | |
1530 | * ProB Plugin: ModelCheckingCommand | |
1531 | * ProB 2.0: ModelCheckingStepCommand | |
1532 | */ | |
1533 | :- mode do_modelchecking(+Time,+Options,-Result,-Stats). | |
1534 | do_modelchecking(Time, Options, Result, stats(NrNodes,NrTrans,NrProcessed)) :- | |
1535 | statistics(walltime, [CurTime,_]), /* get current time in ms */ | |
1536 | LimitTime is CurTime+Time, | |
1537 | option_set(find_deadlocks, Options, Deadlock), | |
1538 | option_set(find_invariant_violations, Options, Invariant), | |
1539 | option_set(find_assertion_violations, Options, Assertions), | |
1540 | option_set(inspect_existing_nodes, Options, InspectExistingNodes), | |
1541 | option_set(stop_at_full_coverage, Options, StopAtFullCoverage), | |
1542 | (option_set(breadth_first_search, Options, 1) -> set_depth_breadth_first_mode(breadth_first) ; | |
1543 | option_set(depth_first_search, Options, 1) -> set_depth_breadth_first_mode(depth_first) ; | |
1544 | set_depth_breadth_first_mode(mixed)), | |
1545 | option_set(find_goal, Options, Goal), | |
1546 | (option_set(partial_guard_evaluation, Options, 1) | |
1547 | -> preferences:get_preference(pge,PartialGuardEvaluation) | |
1548 | ; PartialGuardEvaluation = off), | |
1549 | (option_set(partial_order_reduction, Options, 1) | |
1550 | -> preferences:get_preference(por,WithPOR) | |
1551 | ; WithPOR = off), | |
1552 | % no partial guards evaluation | |
1553 | MaxNumberOfStatesToCheck=100000, | |
1554 | user:do_model_check(MaxNumberOfStatesToCheck, _, LimitTime, Res, Deadlock, Invariant, Goal,Assertions, | |
1555 | StopAtFullCoverage, WithPOR, PartialGuardEvaluation, InspectExistingNodes), | |
1556 | build_modelcheck_return(Res, Result), | |
1557 | get_state_space_stats(NrNodes, NrTrans, NrProcessed). | |
1558 | ||
1559 | /** | |
1560 | Sets the goal for model checking. The Option search_for_goal needs to be set when starting | |
1561 | model checking in order for this to have an effect on the model checking. | |
1562 | ||
1563 | #### called by: | |
1564 | * ProB 2.0: SetBGoalCommand | |
1565 | */ | |
1566 | :- mode set_goal_for_model_checking(+Goal). | |
1567 | set_goal_for_model_checking(Goal) :- | |
1568 | evaluate_formula_typecheck('#PREDICATE',Goal,TypedGoal,Errors), | |
1569 | (Errors = [] -> | |
1570 | b_set_parsed_typed_machine_goal(TypedGoal); | |
1571 | add_error_and_fail(set_goal_for_model_checking,typeerror,Errors) | |
1572 | ). | |
1573 | ||
1574 | /** | |
1575 | Takes an atom and unifies Result with 1 if the atom is in the List. | |
1576 | Otherwise, Result is unified with 0. | |
1577 | */ | |
1578 | :- mode option_set(+Element, +List, -Result). | |
1579 | option_set(Element, List, Result) :- | |
1580 | ( member(Element,List) | |
1581 | -> Result = 1 | |
1582 | ; Result = 0). | |
1583 | ||
1584 | :- mode build_modelcheck_return(+MCRes, -JavaResult). | |
1585 | build_modelcheck_return(MCRes, JavaResult) :- | |
1586 | build_modelcheck_return2(MCRes, JavaResult) -> true | |
1587 | ; nl, print('### Unknown Model Check Error Result:'), print(MCRes), nl, /* TODO: Why do we print something here? Can we get rid of this print? (Q? from Joy)*/ | |
1588 | current_state_id(State), JavaResult=general_error(State, MCRes). | |
1589 | ||
1590 | build_modelcheck_return2(no, not_yet_finished(100000)). | |
1591 | build_modelcheck_return2([timeout,N], not_yet_finished(N1)) :- N1 is 100000 - N. | |
1592 | build_modelcheck_return2(deadlock, deadlock(State)):- current_state_id(State). | |
1593 | build_modelcheck_return2(invariant_violation, invariant_violation(State)):- current_state_id(State). | |
1594 | build_modelcheck_return2(assertion_violation, assertion_violation(State)):- current_state_id(State). | |
1595 | build_modelcheck_return2(state_error, state_error(State)):- current_state_id(State). | |
1596 | build_modelcheck_return2(state_error(_), state_error(State)):- current_state_id(State). | |
1597 | build_modelcheck_return2(goal_found, goal_found(State)) :- current_state_id(State). | |
1598 | build_modelcheck_return2(well_definedness_error, well_definedness_error(State)) :- current_state_id(State). | |
1599 | build_modelcheck_return2(general_error_occurred, general_error(State)):- current_state_id(State). | |
1600 | build_modelcheck_return2(full_coverage, full_coverage). | |
1601 | build_modelcheck_return2(all, Res) :- max_reached_or_timeout_for_node(_),!, Res=ok_not_all_nodes_considered. | |
1602 | build_modelcheck_return2(all, ok). | |
1603 | ||
1604 | :- use_module(symbolic_model_checker(bmc),[bmc_symbolic_model_check/1]). | |
1605 | :- use_module(symbolic_model_checker(kinduction), [kinduction_symbolic_model_check/1, tinduction_symbolic_model_check/1]). | |
1606 | :- use_module(symbolic_model_checker(ic3), [ic3_symbolic_model_check/1]). | |
1607 | symbolic_model_check(bmc,Result) :- | |
1608 | bmc_symbolic_model_check(Result). | |
1609 | symbolic_model_check(kinduction,Result) :- | |
1610 | kinduction_symbolic_model_check(Result). | |
1611 | symbolic_model_check(tinduction,Result) :- | |
1612 | tinduction_symbolic_model_check(Result). | |
1613 | symbolic_model_check(ic3,Result) :- | |
1614 | ic3_symbolic_model_check(Result). | |
1615 | ||
1616 | /** | |
1617 | Computes the coverage statistics of the current state space at any given time. | |
1618 | The information of interest includes the total number of nodes and transitions, as well as | |
1619 | a list of statistics about the nodes and operations and a list of the operations that have been uncovered sofar. | |
1620 | ||
1621 | #### called by: | |
1622 | * ProB Plugin: ComputeCoverageCommand | |
1623 | * ProB 2.0: ComputeCoverageCommand | |
1624 | */ | |
1625 | :- use_module(coverage_statistics, [compute_the_coverage/5, operation_hit/2,query_node_hit/2, uncovered_operation/1]). | |
1626 | ||
1627 | :- mode compute_efficient_statespace_stats(-NrNodes, -NrTrans, -NrProcessed). | |
1628 | compute_efficient_statespace_stats(NrNodes, NrTrans, NrProcessed) :- | |
1629 | get_state_space_stats(NrNodes, NrTrans, NrProcessed). | |
1630 | ||
1631 | :- mode compute_coverage(-TotalNodeNr,-TotalTransSum,-NodeStat,-OpStat,-Uncovered). | |
1632 | compute_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :- | |
1633 | compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false), | |
1634 | findall(S2,(operation_hit(OpS,Nr),string_concatenate(':',Nr,S1),string_concatenate(OpS,S1,S2)),OpStat), | |
1635 | findall(S2,(query_node_hit(Prop,Nr),string_concatenate(':',Nr,S1),string_concatenate(Prop,S1,S2)),NodeStat), | |
1636 | findall(OpName, uncovered_operation(OpName),Uncovered). | |
1637 | ||
1638 | ||
1639 | get_modelchecking_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :- | |
1640 | compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false), | |
1641 | findall(entry(OpS,Nr),operation_hit(OpS,Nr),OpStat), | |
1642 | findall(entry(Prop,Nr),query_node_hit(Prop,Nr),NodeStat), | |
1643 | findall(OpName, uncovered_operation(OpName),Uncovered). | |
1644 | ||
1645 | ||
1646 | /** | |
1647 | Performs deadlock freedom checking with constraint Predicate and calulates the Result. | |
1648 | ||
1649 | #### called by: | |
1650 | * ProB 2.0: ConstraintBasedDeadlockCheckCommand | |
1651 | */ | |
1652 | :- mode prob2_deadlock_freedom_check(+Predicate,-Result). | |
1653 | prob2_deadlock_freedom_check(Predicate,Result) :- | |
1654 | b_type_expression(Predicate,[variables],pred,TPredicate,Errors), | |
1655 | ( Errors == [] -> | |
1656 | prob2_deadlock_freedom_check1(TPredicate,Result) | |
1657 | ; otherwise -> | |
1658 | Result = errors(Errors)). | |
1659 | prob2_deadlock_freedom_check1(Predicate,Result) :- | |
1660 | % always do a deadlock check with SMT mode enabled | |
1661 | call_with_smt_mode_enabled(prob2_deadlock_freedom_check2(Predicate,Result)). | |
1662 | prob2_deadlock_freedom_check2(Predicate,Result) :- | |
1663 | user_interruptable_call_det(user:catch_clpfd_overflow_call1(cbc_deadlock_freedom_check(State,Predicate,0)), | |
1664 | InterruptResult),!, | |
1665 | ( InterruptResult = interrupted -> | |
1666 | Result = interrupted | |
1667 | ; State = time_out -> | |
1668 | Result = interrupted | |
1669 | ; otherwise -> | |
1670 | Result = deadlock(Transition,StateId), | |
1671 | add_artificial_transition(root,deadlock_check,State,StateId,Transition)). | |
1672 | prob2_deadlock_freedom_check2(_Predicate,no_deadlock_found). | |
1673 | ||
1674 | ||
1675 | ||
1676 | ||
1677 | ||
1678 | ||
1679 | /** | |
1680 | Performs invariant checking for either for all operations or a list of operations. | |
1681 | ||
1682 | #### called by: | |
1683 | * ProB 2.0: ConstraintBasedInvariantCheckCommand | |
1684 | */ | |
1685 | :- mode prob2_invariant_check(+Ops,-Result). | |
1686 | prob2_invariant_check(all,Result) :- | |
1687 | findall(OpName,b_is_operation_name(OpName),Ops), | |
1688 | prob2_invariant_check2(Ops,Result). | |
1689 | prob2_invariant_check(ops(Ops),Result) :- | |
1690 | prob2_invariant_check2(Ops,Result). | |
1691 | prob2_invariant_check2(Ops,Result) :- | |
1692 | call_with_smt_mode_enabled(prob2_invariant_check3(Ops,Result,[])). | |
1693 | prob2_invariant_check3([]) --> !. | |
1694 | prob2_invariant_check3([Op|Rest]) --> | |
1695 | prob2_invariant_check_for_single_op(Op), | |
1696 | prob2_invariant_check3(Rest). | |
1697 | prob2_invariant_check_for_single_op(OpName,In,Out) :- | |
1698 | ( clpfd_interface:catch_clpfd_overflow_call1(b_state_model_check:state_model_check(OpName,State1,Operation,State2)) -> | |
1699 | In = [counterexample(OpName,Trans1,Trans2)|Out], | |
1700 | atom_concat( invariant_check_ , OpName, RootTrans), | |
1701 | add_artificial_transition(root, RootTrans,State1,StateId1,Trans1), | |
1702 | add_artificial_transition(StateId1,Operation,State2,_StateId2,Trans2) | |
1703 | ; otherwise -> | |
1704 | In = Out). | |
1705 | ||
1706 | ||
1707 | prob2_redundant_invariants(Redundant, Timeout) :- | |
1708 | b_state_model_check:cbc_find_redundant_invariants(Redundant, Timeout). | |
1709 | ||
1710 | /** | |
1711 | creates a helper transition that is artificially added to the state space (e.g. during deadlock checking) | |
1712 | This transition is added to the state space. | |
1713 | A triple TransitionTuple in the form op(TransId,OpName,SrcId,DstId) for this transition is generated. | |
1714 | */ | |
1715 | :- mode add_artificial_transition(+SrcId,+Operation,+DstState,+DstId,-TransitionTuple). | |
1716 | add_artificial_transition(SrcId,Operation,DstState,DstId,TransitionTuple) :- | |
1717 | user:tcltk_add_new_transition_transid(SrcId,Operation,DstId,DstState,[],TransId), | |
1718 | extract_op_name(Operation,OpName), | |
1719 | TransitionTuple = op(TransId,OpName,SrcId,DstId). | |
1720 | ||
1721 | /** | |
1722 | computes the enabling relation information for the provided operations of interest | |
1723 | get_enable_matrix(-PairsOfOperations,+EnableResult) | |
1724 | PairsOfOperations: list of pair(Op1,Op2) of operations pairs for which the enable relation is to be computed | |
1725 | EnableResult: list of terms enable_edges(Op1,Op2,enable_edges(E,KE,D,KD)) of same length | |
1726 | */ | |
1727 | get_enable_matrix(PairsOfOperations,EnableResult) :- | |
1728 | maplist(compute_enable_matrix_entry(100),PairsOfOperations,EnableResult). | |
1729 | ||
1730 | :- use_module(probsrc(enabling_analysis),[compute_cbc_enable_rel/4]). | |
1731 | compute_enable_matrix_entry(ExtraTimeout,pair(OpName1,OpName2), | |
1732 | enable_rel(OpName1,OpName2, | |
1733 | enable_edges(Enable,KeepEnabled,Disable,KeepDisabled))) :- | |
1734 | compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,[Enable,KeepEnabled,Disable,KeepDisabled]). | |
1735 | ||
1736 | /** | |
1737 | Performs an LTL model checking step. | |
1738 | ||
1739 | #### called by: | |
1740 | * ProB 2.0: LtlCheckingCommand | |
1741 | */ | |
1742 | :- mode prob2_do_ltl_modelcheck(+Formula,+Max,-Result,-Errors). | |
1743 | prob2_do_ltl_modelcheck(Formula,Max,Result,Errors) :- | |
1744 | typecheck_temporal_formula(Formula,TypeCheckedFormula,Status), | |
1745 | ( Status=ok -> | |
1746 | ltl_model_check_with_ce(TypeCheckedFormula,Max,init,Result1), | |
1747 | prob2_ltl_adapt_operations(Result1,Result), | |
1748 | get_error_messages(_WarningsOnly,Errors) | |
1749 | ; otherwise -> | |
1750 | Result=typeerror, | |
1751 | get_error_messages(_WarningsOnly,Errors)). | |
1752 | ||
1753 | prob2_ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), Res) :- !, | |
1754 | Res = counterexample(CE,LoopEntry,PathToCE), | |
1755 | create_simple_op_terms(PathToCE1,root,PathToCE), | |
1756 | prob2_ltl_adapt_ce(CE1,CE). | |
1757 | prob2_ltl_adapt_operations(Result,Result). | |
1758 | ||
1759 | prob2_ltl_adapt_ce([],[]). | |
1760 | prob2_ltl_adapt_ce([atom(StateId,_,OpTuple)|Irest],[Transition|Orest]) :- | |
1761 | prob2_ltl_adapt_ce2(OpTuple,StateId,Transition), | |
1762 | prob2_ltl_adapt_ce(Irest,Orest). | |
1763 | prob2_ltl_adapt_ce2(none,_StateId,none). | |
1764 | prob2_ltl_adapt_ce2((TransId,Action,DestId),StateId,op(TransId,Name,StateId,DestId)) :- | |
1765 | extract_op_name(Action,Name). | |
1766 | ||
1767 | /* ------------------------- */ | |
1768 | /* Plugin Handling */ | |
1769 | /* ------------------------- */ | |
1770 | ||
1771 | /** | |
1772 | Activates a plugin with the given ID | |
1773 | ||
1774 | #### called by: | |
1775 | * ProB Plugin: ActivateUnitPluginCommand | |
1776 | * ProB 2.0: ActivateUnitPluginCommand | |
1777 | */ | |
1778 | :- mode activate_plugin(+ID). | |
1779 | activate_plugin(ID) :- add_internal_error('Plugins no longer supported',activate_plugin(ID)). | |
1780 | ||
1781 | /** | |
1782 | Gets the output for a given plugin | |
1783 | ||
1784 | #### called by: | |
1785 | * ProB Plugin: GetPluginResultCommand | |
1786 | * ProB 2.0: GetPluginResultCommand | |
1787 | */ | |
1788 | :- mode get_plugin_output(+OutputID,-Output). | |
1789 | get_plugin_output(OutputID,Output) :- | |
1790 | add_internal_error('Plugins no longer supported',get_plugin_output(OutputID,Output)). | |
1791 | ||
1792 | ||
1793 | /* ------------------------- */ | |
1794 | /* Find Traces */ | |
1795 | /* ------------------------- */ | |
1796 | ||
1797 | /** | |
1798 | Finds a trace from the root state to the specified state in the current state space. | |
1799 | ||
1800 | #### Parameters: | |
1801 | * StateId | |
1802 | * Trace - List of op tuples op(OpId,SrcId,DestId) corresponding to the trace calculated by ProB or atom no_trace_found if the call was unsuccessful | |
1803 | ||
1804 | #### called by: | |
1805 | * ProB 2.0: GetShortestTraceCommand | |
1806 | */ | |
1807 | :- mode find_trace_to_node(+StateId,-Trace). | |
1808 | find_trace_to_node(StateId, Trace) :- | |
1809 | find_trace_from_node_to_node(root, StateId, Trace). | |
1810 | ||
1811 | /** | |
1812 | Finds a trace from one state to a goal state in the current state space. | |
1813 | ||
1814 | #### Parameters: | |
1815 | * FromId - Id of source node | |
1816 | * ToId - Id of destination node | |
1817 | * Trace - List of op tuples op(OpId,SrcId,DestId) corresponding to the trace calculated by ProB or atom no_trace_found if the call was unsuccessful | |
1818 | ||
1819 | #### called by: | |
1820 | * ProB 2.0: GetShortestTraceCommand | |
1821 | */ | |
1822 | :- mode find_trace_from_node_to_node(+FromId,+ToId,-Trace). | |
1823 | find_trace_from_node_to_node(FromId, ToId, Trace) :- | |
1824 | (user:find_shortest_trace_to_node(FromId, ToId, OpIDs, _TraceIDs) -> | |
1825 | trace_to_op_triple(OpIDs,FromId,Trace); | |
1826 | Trace = no_trace_found | |
1827 | ). | |
1828 | ||
1829 | /** | |
1830 | Translates a list of transition ids to a list of op tuples op(TransId,OpName,SrcId,DestId) | |
1831 | */ | |
1832 | :- mode trace_to_op_triple(+ListOpIds,+CurID,-ListTuples). | |
1833 | trace_to_op_triple([],_,[]). | |
1834 | trace_to_op_triple([OpID|T], SrcID, [op(OpID,Name,SrcID,Dest)|OpT]) :- | |
1835 | transition(SrcID,Action,OpID,Dest), | |
1836 | extract_op_name(Action,Name), | |
1837 | trace_to_op_triple(T,Dest,OpT). | |
1838 | ||
1839 | /** | |
1840 | Takes a given predicate and finds a state in the state space that satisfies the predicate. | |
1841 | A helper transition is then added to go to the goal state. | |
1842 | ||
1843 | #### called by: | |
1844 | * ProB 2.0: FindValidStateCommand | |
1845 | */ | |
1846 | find_state_for_predicate(Predicate,UseInvariant,Result) :- | |
1847 | evaluate_formula_typecheck('#PREDICATE',Predicate,TPredicate,Errors), | |
1848 | ( Errors == [] -> | |
1849 | find_state_for_predicate1(TPredicate,UseInvariant,Result) | |
1850 | ; otherwise -> | |
1851 | Result = errors(Errors)). | |
1852 | find_state_for_predicate1(Predicate,UseInvariant,Result) :- | |
1853 | user_interruptable_call_det(user:catch_clpfd_overflow_call1( | |
1854 | b_set_up_valid_state_with_pred(State,Predicate,UseInvariant,none)), % TODO: pass UseConstantsFromStateID | |
1855 | InterruptResult),!, | |
1856 | ( InterruptResult = interrupted -> | |
1857 | Result = interrupted | |
1858 | ; State = time_out -> | |
1859 | Result = interrupted | |
1860 | ; otherwise -> | |
1861 | Result = state_found(Transition,StateId), | |
1862 | add_artificial_transition(root,find_valid_state,State,StateId,Transition)). | |
1863 | find_state_for_predicate1(_Predicate,_,no_valid_state_found). | |
1864 | ||
1865 | /** | |
1866 | #### called by: | |
1867 | * ProB Plugin (de.prob.eventb.disprover.core): DisproverCommand | |
1868 | */ | |
1869 | :- mode cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult). | |
1870 | cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult) :- | |
1871 | disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult), | |
1872 | % remove the warning regarding double check, in rodin it is shown in the proof tree anyway | |
1873 | (get_error(warning(disprover_inconsistent_hypotheses),_) ; true). | |
1874 | ||
1875 | :- mode cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult). | |
1876 | cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult) :- | |
1877 | disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult), | |
1878 | % remove the warning regarding double check, in rodin it is shown in the proof tree anyway | |
1879 | (get_error(warning(disprover_inconsistent_hypotheses),_) ; true). | |
1880 | ||
1881 | /** | |
1882 | Takes a predicates and produces a result from the selected solver | |
1883 | #### called by: | |
1884 | * ProB 2.0: CbcSolveCommand | |
1885 | */ | |
1886 | :- mode cbc_solve(+Solver,+Predicate,-Identifiers,-Result). | |
1887 | cbc_solve(Solver,Predicate,Identifiers,Result) :- | |
1888 | cbc_solve(Solver,Predicate,_State,Identifiers,Result). | |
1889 | cbc_solve(Solver,Predicate,State,Identifiers,Result) :- | |
1890 | cbc_solve(Solver,Predicate,State,1,Identifiers,Result). | |
1891 | cbc_solve(Solver,Predicate,State,TimeoutFactor,Identifiers,Result) :- | |
1892 | cbc_solve_type(Solver,Predicate,TPredicate), | |
1893 | find_identifier_uses(TPredicate,[],Identifiers), | |
1894 | (atomic(State) -> Options = [solve_in_visited_state(State)] ; LState=State), | |
1895 | cbc_solve_typed(Solver,TPredicate,LState,TimeoutFactor,Options,Result). | |
1896 | ||
1897 | :- assert_must_succeed((cbc_solve_with_opts('PROB',[truncate(10)], | |
1898 | equal(none,identifier(none,x),integer(none,10)),Identifiers,Result), | |
1899 | Identifiers == [x], | |
1900 | Result == solution([binding(x,int(10),'10')]))). | |
1901 | ||
1902 | % This should be the new entry point for CbcSolveCommand, cbc_solve is no longer used | |
1903 | :- mode cbc_solve_with_opts(+Solver,+Options,+Predicate,-Identifiers,-Result). | |
1904 | cbc_solve_with_opts(Solver,Options,Predicate,Identifiers,Result) :- | |
1905 | maplist(prob2_interface:check_cbc_solve_opts,Options), | |
1906 | cbc_solve_type(Solver,Predicate,TPredicate), | |
1907 | find_identifier_uses(TPredicate,[],Identifiers), | |
1908 | (select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options), | |
1909 | cbc_solve_typed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result). | |
1910 | ||
1911 | check_cbc_solve_opts(full_machine_state) :- !. | |
1912 | check_cbc_solve_opts(solve_in_visited_state(ID)) :- !,atomic(ID). | |
1913 | check_cbc_solve_opts(timeout_factor(Nr)) :- !,number(Nr). | |
1914 | check_cbc_solve_opts(truncate(Nr)) :- !,number(Nr). % truncate pretty printing | |
1915 | check_cbc_solve_opts(truncate) :- !. % truncate pretty printing | |
1916 | check_cbc_solve_opts(force_evaluation) :- !. % force evaluation of symbolic results | |
1917 | check_cbc_solve_opts(IO) :- add_internal_error('Illegal cbc_solve option:',IO). | |
1918 | ||
1919 | cbc_solve_typed('PROB',Predicate,State,TimeoutFactor,Options,Result) :- | |
1920 | solve_predicate(Predicate,State,TimeoutFactor,['SMT','CLPFD'|Options],Result). | |
1921 | cbc_solve_typed('KODKOD',Predicate,State,TimeoutFactor,Options,Result) :- | |
1922 | solve_predicate(Predicate,State,TimeoutFactor,['KODKOD','SMT','CLPFD'|Options],Result). | |
1923 | cbc_solve_typed('SMT_SUPPORTED_INTERPRETER',Predicate,State,TimeoutFactor,Options,Result) :- | |
1924 | solve_predicate(Predicate,State,TimeoutFactor,['SMT_SUPPORTED_INTERPRETER','SMT','CLPFD'|Options],Result). | |
1925 | cbc_solve_typed(SOLVER,Predicate,_StateID,_,Options,Result) :- recognised_smt_solver(SOLVER,InternalName), | |
1926 | (member(solve_in_visited_state(ID),Options) -> | |
1927 | smt_solve_predicate_in_state(ID,InternalName,Predicate,_State,Result) | |
1928 | ; smt_solve_predicate(InternalName,Predicate,_State,Result)). | |
1929 | ||
1930 | recognised_smt_solver('Z3',z3). | |
1931 | recognised_smt_solver('CVC4',cvc4). | |
1932 | ||
1933 | :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]). | |
1934 | cbc_solve_type('KODKOD',Pred,TPred) :- !, | |
1935 | temporary_set_preference(try_kodkod_on_load,true,C), | |
1936 | call_cleanup(cbc_solve_type2(Pred,TPred), | |
1937 | reset_temporary_preference(try_kodkod_on_load,C)). | |
1938 | cbc_solve_type(_,Pred,TPred) :- cbc_solve_type2(Pred,TPred). | |
1939 | cbc_solve_type2(Pred,TPred) :- | |
1940 | !, get_eval_scope(Scope), | |
1941 | b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors), | |
1942 | (Errors=[] -> true ; add_error_and_fail(register_prob2_formula, 'Type-Errors: ', Errors)). | |
1943 | ||
1944 | /** | |
1945 | Takes a predicates and generates a pretty printed string | |
1946 | */ | |
1947 | :- assert_must_succeed((pretty_print_predicate(equal(none,identifier(none,x),integer(none,1)),[],Result), | |
1948 | Result == 'x = 1')). | |
1949 | :- assert_must_succeed((pretty_print_predicate(not_equal(none,identifier(none,x),integer(none,1)),[latex],Result), | |
1950 | Result == '\\mathit{x} \\neq 1')). | |
1951 | :- assert_must_succeed((pretty_print_predicate(not_equal(pos(2,-1,1,1,1,7),integer(pos(3,-1,1,1,1,2),1), | |
1952 | integer(pos(4,-1,1,6,1,7),2)),[latex,nopt],PPString), | |
1953 | PPString == '1 \\neq 2' )). | |
1954 | ||
1955 | pretty_print_predicate(Pred,Options,PPString) :- | |
1956 | select(nopt,Options,Opts2), | |
1957 | !, | |
1958 | temporary_set_preference(optimize_ast,false,CHNG1), | |
1959 | pretty_print_predicate(Pred,Opts2,PPString), | |
1960 | reset_temporary_preference(optimize_ast,CHNG1). | |
1961 | pretty_print_predicate(Pred,Options,PPString) :- | |
1962 | get_eval_scope(Scope), | |
1963 | b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors), | |
1964 | (Errors=[] -> true ; add_error_and_fail(pretty_print_predicate, 'Type-Errors: ', Errors)), | |
1965 | translate_pred(TPred,Options,PPString). | |
1966 | ||
1967 | :- use_module(translate,[set_unicode_mode/0, unset_unicode_mode/0, unicode_mode/0, | |
1968 | set_latex_mode/0, unset_latex_mode/0, latex_mode/0]). | |
1969 | translate_pred(TPred,Options,PPString) :- | |
1970 | select(unicode,Options,Opts2), \+ unicode_mode, | |
1971 | !, | |
1972 | set_unicode_mode,translate_pred(TPred,Opts2,PPString),unset_unicode_mode. | |
1973 | translate_pred(TPred,Options,PPString) :- | |
1974 | select(latex,Options,Opts2), \+ latex_mode, | |
1975 | !, | |
1976 | set_latex_mode,translate_pred(TPred,Opts2,PPString),unset_latex_mode. | |
1977 | translate_pred(TPred,_,PPString) :- | |
1978 | translate_bexpression(TPred,PPString). | |
1979 | ||
1980 | % Constraint-Based Test-case generation | |
1981 | % TO DO: return values | |
1982 | :- use_module(sap,[cbc_gen_test_cases/5]). | |
1983 | cbc_generate_test_cases(TargetPred,MaxDepth,OutputFile) :- | |
1984 | % I am not sure whether we should call b_parse_machine_predicate(TargetPred,...) or not | |
1985 | Events = all, | |
1986 | cbc_gen_test_cases(Events,TargetPred,MaxDepth,OutputFile,_Uncovered). | |
1987 | ||
1988 | ||
1989 | ||
1990 | :- use_module(sap,[create_testcase_path/5]). | |
1991 | % example call | ?- prob2_interface:prob2_find_test_path([enter1],truth(unknown),200,R). | |
1992 | :- mode prob2_find_test_path(+Events,+EndPredicate,+TimeoutMs,-ResultOpTerms). | |
1993 | % Result is either errors(Errors), timeout, interrupt, infeasible_path, or list of Operation IDs | |
1994 | prob2_find_test_path(Events,EndPredicate,TimeoutMs,ResultOpTerms) :- | |
1995 | evaluate_formula_typecheck('#PREDICATE',EndPredicate,TPredicate,Errors), | |
1996 | ( Errors == [] -> | |
1997 | prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResultOpTerms) | |
1998 | ; ResultOpTerms = errors(Errors)). | |
1999 | ||
2000 | prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResOperationIds) :- | |
2001 | ( create_testcase_path(init,Events,TPredicate,TimeoutMs,Trace) | |
2002 | -> (is_list(Trace) -> maplist(extract_opid,Trace,ResOperationIds) | |
2003 | % Trace can be "timeout" or "interrupt", too | |
2004 | ; ResOperationIds=Trace) | |
2005 | ; ResOperationIds = infeasible_path). | |
2006 | ||
2007 | extract_opid((TransId,OpTerm,StateId,DestId),op(TransId,Name,StateId,DestId)) :- extract_op_name(OpTerm,Name). | |
2008 | ||
2009 | /* ------------------------- */ | |
2010 | /* Check CSP Assertion */ | |
2011 | /* ------------------------- */ | |
2012 | ||
2013 | /** | |
2014 | Takes a list of assertions and produce a list of results and result traces. | |
2015 | ||
2016 | TODO: We should modify the result traces so that they are useful for ProB 2.0. (or at least document what the result traces mean) | |
2017 | ||
2018 | #### called by: | |
2019 | * ProB 2.0: CSPAssertionsCommand | |
2020 | */ | |
2021 | :- mode check_csp_assertions(+Assertions,-Results,-ResultTraces). | |
2022 | check_csp_assertions(Assertions,Results,ResultTraces) :- | |
2023 | maplist(check_csp_assertion,Assertions,Results,ResultTraces). | |
2024 | ||
2025 | check_csp_assertion(AssClause,Res,ResTrace1) :- | |
2026 | read_from_codes(AssClause,Assertion), | |
2027 | user:checkAssertion(Assertion,_PP,_Negated,Res,ResTrace), | |
2028 | (ResTrace = no_counter_example -> ResTrace1 = []; ResTrace1=ResTrace). | |
2029 | ||
2030 | /* ------------------------- */ | |
2031 | /* Preferences Interface */ | |
2032 | /* ------------------------- */ | |
2033 | ||
2034 | /** | |
2035 | Returns a list of all the preferences with their current values | |
2036 | ||
2037 | #### called by: | |
2038 | * ProB 2.0: GetCurrentPreferencesCommand | |
2039 | */ | |
2040 | :- mode list_current_eclipse_preferences(-L). | |
2041 | list_current_eclipse_preferences(L) :- | |
2042 | findall(preference(A,B),find_eclipse_preference(A,B),L). | |
2043 | ||
2044 | find_eclipse_preference(A,B) :- | |
2045 | list_all_eclipse_preferences(X), | |
2046 | member(preference(A,_,_,_,_),X), | |
2047 | get_eclipse_preference(A,B). | |
2048 | ||
2049 | /** | |
2050 | Returns the current value of a specified preference. | |
2051 | ||
2052 | #### called by: | |
2053 | * ProB 2.0: GetPreferenceCommand | |
2054 | */ | |
2055 | get_eclipse_preference(PrefS,PrefVal) :- | |
2056 | if(eclipse_preference(PrefS,PS), | |
2057 | get_preference(PS,PrefVal), | |
2058 | add_error_and_fail(get_eclipse_preference,'Unknown preference:',PrefS)). | |
2059 | ||
2060 | /** | |
2061 | Returns a list of all normal eclipse preferences as well as their information | |
2062 | (i.e. type, description, category, and default value) | |
2063 | ||
2064 | #### called by: | |
2065 | * ProB Plugin: GetPreferencesCommand | |
2066 | * ProB 2.0: GetDefaultPreferencesCommand | |
2067 | */ | |
2068 | :- mode list_eclipse_preferences(-L). | |
2069 | list_eclipse_preferences(L) :- | |
2070 | findall(preference(A,B,C,D,E), | |
2071 | (get_eclipse_preference_infos(A,B,C,D,E), | |
2072 | \+ advanced_eclipse_preference(A,_)), L). | |
2073 | :- mode list_all_eclipse_preferences(-L). % also includes advanced eclipse preferences | |
2074 | list_all_eclipse_preferences(L) :- | |
2075 | findall(preference(A,B,C,D,E),get_eclipse_preference_infos(A,B,C,D,E),L). | |
2076 | ||
2077 | get_eclipse_preference_infos(PrefString,Type,Description,Category,DefaultValue) :- | |
2078 | eclipse_preference(PrefString,PS), | |
2079 | %\+ advanced_eclipse_preference(PrefString,PS), % we now want to show all preferences in ProB 2 | |
2080 | preference_val_type(PS,Type), | |
2081 | preference_description(PS,Description), | |
2082 | preference_category(PS,Category), | |
2083 | preference_default_value(PS,DefaultValue). | |
2084 | ||
2085 | /** | |
2086 | Sets a preference | |
2087 | ||
2088 | #### called by: | |
2089 | * ProB Plugin: SetPreferenceCommand | |
2090 | * ProB 2.0: SetPreferenceCommand | |
2091 | */ | |
2092 | :- use_module(tools_strings, [convert_cli_arg/2]). | |
2093 | :- mode set_eclipse_preference(+PrefS,+PrefVal). | |
2094 | set_eclipse_preference(PrefS,PrefVal) :- | |
2095 | convert_cli_arg(PrefVal,Value), | |
2096 | convert_pref_value(Value,CValue), | |
2097 | ? | (eclipse_preference(PrefS,P) |
2098 | -> (set_preference(P,CValue) | |
2099 | -> true | |
2100 | ; add_error(eclipse_preference,'Could not set preference: ',Value)) | |
2101 | ; obsolete_eclipse_preference(PrefS) | |
2102 | -> add_warning(eclipse_preference,'Obsolete preference: ',PrefS) | |
2103 | ; add_error_and_fail(eclipse_preference,'Unknown preference: ',PrefS) | |
2104 | ). | |
2105 | ||
2106 | convert_pref_value('TRUE',V) :- !, V=true. | |
2107 | convert_pref_value('FALSE',V) :- !, V=false. | |
2108 | convert_pref_value(X,X). | |
2109 | ||
2110 | /* ------------------------- */ | |
2111 | /* Apply Graph reduction */ | |
2112 | /* ------------------------- */ | |
2113 | ||
2114 | /** | |
2115 | Takes a list of ignored events, and applies the signature merge algorithm | |
2116 | from module `state_space_reduction` to the current state space. | |
2117 | ||
2118 | #### called by: | |
2119 | * ProB 2.0: ApplySignatureMergeCommand | |
2120 | */ | |
2121 | :- mode get_signature_merge_state_space(+IgnoredEvents,-Space). | |
2122 | get_signature_merge_state_space(IgnoredEvents,Space) :- | |
2123 | reset_ignored_events, | |
2124 | set_ignored_events(IgnoredEvents), | |
2125 | compute_signature_merge, | |
2126 | findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,simple_list,Labels),Nodes), | |
2127 | findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(true,TransId,Src,Dest,Label,Style,Color),Trans), | |
2128 | Space = [Nodes,Trans]. | |
2129 | ||
2130 | /** | |
2131 | Takes a list of ignored events, and calculates a transition diagram | |
2132 | using module `state_space_reduction` for the current state space. | |
2133 | ||
2134 | #### called by: | |
2135 | * ProB 2.0: CalculateTransitionDiagramCommand | |
2136 | */ | |
2137 | :- mode get_transition_diagram(+ParsedExpr,-Space). | |
2138 | get_transition_diagram(ParsedExpr,Space) :- | |
2139 | evaluate_formula_typecheck('#EXPRESSION',ParsedExpr,TypedExpr,Errors), | |
2140 | (Errors = [] -> true; add_error_and_fail(get_transition_diagram,typeerror,Errors)), | |
2141 | compute_transition_diagram(TypedExpr), | |
2142 | findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,gen_label,Labels),Nodes), | |
2143 | findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(false,TransId,Src,Dest,Label,Style,Color),Trans), | |
2144 | Space = [Nodes,Trans]. | |
2145 | ||
2146 | write_dotty_transition_diagram(Expression,Filename) :- | |
2147 | write_dotty_for_expr(transition_diagram,Expression,Filename). | |
2148 | ||
2149 | write_dotty_signature_merge(IgnoredEvents,Filename) :- | |
2150 | write_signature_merge_to_dotfile(IgnoredEvents,Filename). | |
2151 | ||
2152 | write_dotty_state_space(Filename) :- | |
2153 | write_dotty(state_space,Filename). | |
2154 | ||
2155 | :- use_module(meta_interface,[is_dot_command/1, call_dot_command/3]). | |
2156 | % find out which commands only require a filename: | |
2157 | is_dotty_command(Command) :- is_dot_command(Command). | |
2158 | % call commands which generate a dot file (without requiring further arguments, such as an expression) | |
2159 | write_dotty(Command,Filename) :- OptionalArgs=[], | |
2160 | call_dot_command(Command,Filename,OptionalArgs). | |
2161 | ||
2162 | ||
2163 | :- use_module(meta_interface,[is_dot_command_for_expr/1, call_dot_command_for_expr/4]). | |
2164 | % find out which commands only require an expression and a filename: | |
2165 | is_dotty_command_for_expr(Command) :- is_dot_command_for_expr(Command). | |
2166 | % call commands which generate a dot file from an expression: | |
2167 | write_dotty_for_expr(Command,Expr,Filename) :- OptionalArgs=[], | |
2168 | call_dot_command_for_expr(Command,Expr,Filename,OptionalArgs). | |
2169 | ||
2170 | ||
2171 | :- use_module(meta_interface,[command_additional_info/2, command_unavailable/2]). | |
2172 | ||
2173 | % -------------------------------------------------------- | |
2174 | % New preferred API for calling DOT / TABLE commands in ProB2 JFX: | |
2175 | % get_dot_commands_in_state/2 and call_dot_command_and_dot_in_state/5 | |
2176 | % get_table_commands_in_state/2 and call_table_command_in_state/4 | |
2177 | ||
2178 | ||
2179 | % example call: prob2_interface:get_dot_commands_in_state(1,List). | |
2180 | get_dot_commands_in_state(StateID,List) :- get_commands_in_state(dot,StateID,List). | |
2181 | get_commands_in_state(Category,StateID,List) :- | |
2182 | user:tcltk_goto_node_with_id(StateID), | |
2183 | findall(command(Command,Name,Description,NumberOfFormulaArgs,RelevantEclipsePrefs,AdditionalInfo,AvailMsg), | |
2184 | (is_a_command(Category,Command,Name,Description,NumberOfFormulaArgs,RelevantPrefs,AdditionalInfo), | |
2185 | maplist(convert_pref,RelevantPrefs,RelevantEclipsePrefs), | |
2186 | (command_unavailable(Command,AvailMsg) -> true ; AvailMsg = available)), | |
2187 | List). | |
2188 | % example call: prob2_interface:get_table_commands_in_state(1,List). | |
2189 | get_table_commands_in_state(StateID,List) :- get_commands_in_state(table,StateID,List). | |
2190 | ||
2191 | convert_pref(Pref,Res) :- eclipse_preference(ECLIPSEPREF,Pref),!,Res=ECLIPSEPREF. | |
2192 | convert_pref(P,P) :- print(cannot_convert_pref(P)),nl. | |
2193 | ||
2194 | :- use_module(meta_interface,[is_dot_command/6, is_table_command/6]). | |
2195 | is_a_command(dot,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :- | |
2196 | is_dot_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo). | |
2197 | is_a_command(table,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :- | |
2198 | is_table_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo). | |
2199 | ||
2200 | ||
2201 | % example call: prob2_interface:call_dot_command_and_dot_in_state(1,invariant,[],svg,'~/Desktop/out.svg'). | |
2202 | call_dot_command_and_dot_in_state(StateID,Command,Formulas,OutputType,OutputFile) :- | |
2203 | user:tcltk_goto_node_with_id(StateID), | |
2204 | call_dot_command_and_dot(Command,Formulas,OutputType,OutputFile). | |
2205 | ||
2206 | call_dot_command_in_state(StateID,Command,Formulas,DotFile) :- | |
2207 | user:tcltk_goto_node_with_id(StateID), | |
2208 | call_dot_command_for_dotfile(Command,Formulas,DotFile). | |
2209 | ||
2210 | % call a dot command for generating a DotFile; used by call_dot_command_and_dot | |
2211 | call_dot_command_for_dotfile(Command,[],DotFile) :- | |
2212 | is_dot_command(Command), !, OptionalArgs=[], | |
2213 | call_dot_command(Command,DotFile,OptionalArgs). | |
2214 | call_dot_command_for_dotfile(Command,[Expr],DotFile) :- | |
2215 | is_dot_command_for_expr(Command), !, OptionalArgs=[], | |
2216 | call_dot_command_for_expr(Command,Expr,DotFile,OptionalArgs). | |
2217 | call_dot_command_for_dotfile(Command,Formulas,DotFile) :- | |
2218 | add_internal_error('Illegal dot call: ',call_dot_command_for_dotfile(Command,Formulas,DotFile)), | |
2219 | fail. | |
2220 | ||
2221 | % call a dot command and generate dot, canon, png, svg, pdf output file | |
2222 | % example call: prob2_interface:call_dot_command_and_dot(state_space,[],dot,'~/Desktop/out.dot'). | |
2223 | % prob2_interface:call_dot_command_and_dot(state_space,[],svg,'~/Desktop/out.svg') | |
2224 | :- use_module(tools_commands,[gen_dot_output_env/6]). | |
2225 | :- use_module(system_call,[get_temporary_filename/2]). | |
2226 | %call_dot_command_and_dot(Command,Formulas,dot,DotFile) :- !, call_dot_command_for_dotfile(Command,Formulas,DotFile). | |
2227 | call_dot_command_and_dot(Command,Formulas,OutputType,OutputFile) :- | |
2228 | get_temporary_filename('prob2_dot_output.dot',DotFile), | |
2229 | call_dot_command_for_dotfile(Command,Formulas,DotFile), % generate Dotfile | |
2230 | (command_additional_info(Command,preferred_dot_type(Cmd)) ; Cmd=default), | |
2231 | gen_dot_output_env(DotFile,Cmd,OutputType,OutputFile,[detached(false)],no_process_wait). % layout and convert Dotfile to target output | |
2232 | ||
2233 | ||
2234 | % example call: prob2_interface:call_table_command_in_state(1,expr_as_table,[integer(pos,1)],Table). | |
2235 | :- use_module(meta_interface,[call_command/5]). | |
2236 | call_table_command_in_state(StateID,Command,Formulas,TableResult) :- | |
2237 | (user:tcltk_goto_node_with_id(StateID) -> true | |
2238 | ; add_error(call_table_command_in_state,'Could not reach state: ',StateID) | |
2239 | ), | |
2240 | (Formulas=[_|_],is_table_command(Command,_,_,0,_,_) | |
2241 | -> ActualArgs = [TableResult] % correct bug in ProB2 Java code | |
2242 | ; append(Formulas,[TableResult],ActualArgs) | |
2243 | ), OptionalArgs=[], | |
2244 | debug_println(9,call_command(table,Command,_,ActualArgs,OptionalArgs)), | |
2245 | call_command(table,Command,_,ActualArgs,OptionalArgs), debug_println(9,result(TableResult)), | |
2246 | !. | |
2247 | call_table_command_in_state(StateID,Command,Formulas,TableResult) :- | |
2248 | add_error(call_table_command_in_state,'Table command failed:',call_table_command_in_state(StateID,Command,Formulas,TableResult)), | |
2249 | TableResult = list([list(['ERROR OCCURED'])]). | |
2250 | ||
2251 | ||
2252 | /** | |
2253 | Writes a dot representation of the given state to the specified file. | |
2254 | ||
2255 | */ | |
2256 | :- mode write_dot_for_state_viz(+StateId, +Filename). | |
2257 | write_dot_for_state_viz(StateId, Filename) :- | |
2258 | get_state(StateId, State), | |
2259 | print_cstate_graph(State, Filename). | |
2260 | ||
2261 | /** | |
2262 | Generates information about the nodes found during state space reduction | |
2263 | ||
2264 | #### Generated Information: | |
2265 | * Count - number of concrete states combined in the abstract state | |
2266 | * Color - the color used to represent this state type in a visualization | |
2267 | * Labels - determine the labels that should appear on a node in a visualization | |
2268 | */ | |
2269 | :- mode extract_node_info(+NodeId,-Count,-Color,+LabelGenerator,-Labels). | |
2270 | extract_node_info(NodeId,Count,Color,LabelGenerator,Labels) :- | |
2271 | get_reduced_node(AbsState,Count,Witness,NodeId), | |
2272 | generate_node_color(NodeId,Witness,AbsState,Count,Color), | |
2273 | generate_node_labels(LabelGenerator,AbsState,Labels). | |
2274 | ||
2275 | /** | |
2276 | Generates information about the transitions created during state space reduction | |
2277 | ||
2278 | #### Generated Information: | |
2279 | * Src - ID corresponding to the abstract state that is the source of the abstract transition with TransId | |
2280 | * Dest - ID corresponding to the abstract state that is the destination of the abstract transition with TransId | |
2281 | * Label - the label that should appear on a transition in a visualization | |
2282 | * Style - the style that should be applied to a transition of this type in a visualization (e.g. dashed) | |
2283 | * Color - the color used to represent a transition of this type in a visualization | |
2284 | */ | |
2285 | :- mode extract_trans_info(+ShowSelfLoops,+TransId,-Src,-Dest,-Label,-Style,-Color). | |
2286 | extract_trans_info(ShowSelfLoops,TransId,Src,Dest,Label,Style,Color) :- | |
2287 | reduced_trans(Src,AbsAction,Count,Dest,TransId), | |
2288 | generate_transition_label(AbsAction,Count,Label), | |
2289 | generate_transition_color_and_style(ShowSelfLoops,Src,AbsAction,Dest,Color,Style). | |
2290 | ||
2291 | ||
2292 | /* ------------------ */ | |
2293 | /* Get Errors */ | |
2294 | /* ------------------ */ | |
2295 | ||
2296 | /** | |
2297 | Returns a list of strings containing all error messages (of the error_manager). | |
2298 | Clears all the errors. Returns the empty list if no errors occurred since | |
2299 | the last call to get_error_messages. | |
2300 | ||
2301 | #### called by: | |
2302 | * ProB 2.0: GetErrorsCommand | |
2303 | */ | |
2304 | :- mode get_error_messages(-WarningsOnly,-ListOfErrMsgs). | |
2305 | get_error_messages(WarningsOnly,ListOfErrMsgs) :- | |
2306 | (real_error_occurred -> WarningsOnly = false ; WarningsOnly = true), | |
2307 | ignore_user_interrupt_det((get_all_errors_and_reset(ListOfErrMsgs) -> true ; ListOfErrMsgs=[])). | |
2308 | ||
2309 | % each error is of the form: error(ErrMsg,ErrType,ErrLocations) | |
2310 | % ErrMsg is an atom (aka string) | |
2311 | % ErrType is warning, internal_error or error | |
2312 | % ErrLocations is a list of terms error_span(Filename,StartLine,StartCol,EndLine,EndCol) | |
2313 | % Note: Filename is '' when not known | |
2314 | :- mode get_error_messages_with_span_info(-WarningsOnly,-ListOfErrMsgTerms). | |
2315 | get_error_messages_with_span_info(WarningsOnly,ListOfErrMsgTerms) :- | |
2316 | (real_error_occurred -> WarningsOnly = false ; WarningsOnly = true), | |
2317 | ignore_user_interrupt_det(get_all_errors_with_span_info_and_reset(ListOfErrMsgTerms)). | |
2318 | ||
2319 | ||
2320 | ||
2321 | /* ------------------------- */ | |
2322 | /* Evalstore */ | |
2323 | /* ------------------------- */ | |
2324 | ||
2325 | /** | |
2326 | TODO: Please document what this does. | |
2327 | ||
2328 | #### called by: | |
2329 | * ProB 2.0: EvalstoreCreateByStateCommand | |
2330 | */ | |
2331 | es_copy_from_statespace(StateId,EvalstoreId) :- | |
2332 | evalstore_create_store_by_state(StateId,EvalstoreId). | |
2333 | ||
2334 | /** | |
2335 | TODO: Please document what this does. | |
2336 | ||
2337 | #### called by: | |
2338 | * ProB 2.0: EvalstoreEvalCommand | |
2339 | */ | |
2340 | :- mode es_eval(+EvalstoreId,+UntypedFormula,+Timeout,-Result). | |
2341 | es_eval(EvalstoreId,UntypedFormula,Timeout,Result) :- | |
2342 | evalstore_eval_formula(EvalstoreId,UntypedFormula,Timeout,Result1), !, | |
2343 | (Result1 = ok(V,TypedIds,StoreId) -> | |
2344 | Result = ok(V,PP,Ids,StoreId), | |
2345 | get_texpr_ids(TypedIds,Ids), | |
2346 | es_eval_translate(V,PP) | |
2347 | ; otherwise -> Result = Result1). | |
2348 | es_eval_translate(pred(V),V). | |
2349 | es_eval_translate(value(V),PP) :- | |
2350 | translate_bvalue(V,PP). | |
2351 | ||
2352 | % #################### | |
2353 | ||
2354 | /** | |
2355 | ||
2356 | Animates randomly number of steps until a certain (LTL?) condition is fulfilled. | |
2357 | ||
2358 | #### Called by: | |
2359 | * ProB 2.0: ExecuteUntilCommand | |
2360 | ||
2361 | #### Arguments | |
2362 | * CurState - the ID of the current state | |
2363 | * Condition - a condition that should be satisfied at some point (this come as parsed term from the ProB2) | |
2364 | ||
2365 | #### Generated Information: | |
2366 | * Trace - a list of triples representing a trace in the state space of the model being analysed | |
2367 | * Result - the result found: ltl_found, typeerror, max_nr_of_steps_reached, deadlock | |
2368 | */ | |
2369 | :- mode generate_trace_until_condition_fulfilled(+CurState,+Condition,-Trace,-Result). | |
2370 | generate_trace_until_condition_fulfilled(CurState,Condition,Trace,Result) :- | |
2371 | typecheck_temporal_formula(Condition,TypeCheckedCondition,Status), | |
2372 | ( Status=ok -> find_trace1(CurState,TypeCheckedCondition,no_loop,100000,Trace, Result) %FIXME: turn maximal numver of steps into an argument? | |
2373 | ; otherwise -> get_error_messages(_WOnly,_Errors), % Reset errors. We don't want to throw a ProBError on the Java side because the result is capsuled in Result. | |
2374 | Result=typeerror, Trace=[]). | |
2375 | ||
2376 | find_trace1(StateId,Ltl,Type,MaxSteps,OpTripleResultTrace, Result) :- | |
2377 | (MaxSteps =< 0 | |
2378 | -> add_error(find_trace,'Number of maximum animation steps should be a positive integer. The number of steps which was given is ',MaxSteps) | |
2379 | ; true), | |
2380 | set_current_state(StateId), !, % can be backtracked | |
2381 | % negate -> counterexample is the trace we are looking for | |
2382 | preprocess_formula(Ltl,Ltl2), | |
2383 | find_trace_aux(StateId,not(Ltl2),Type,0,MaxSteps,ResultTrace,ResultTrace,Names,Result), | |
2384 | gen_op_triples(ResultTrace,Names,OpTripleResultTrace). | |
2385 | %(gen_op_triples(ResultTrace,OpTripleResultTrace) -> print(ok(OpTripleResultTrace,result(Result))),nl | |
2386 | % ; add_error_and_fail(prob2_interface,'trace not correctly generated',ResultTrace)). | |
2387 | ||
2388 | find_trace_aux(CurID,Condition,Type,_N,_Max,StateTransitionHistory,[],[],RESULT) :- | |
2389 | debug_println(9,checking_ltl_formula(CurID,StateTransitionHistory)), | |
2390 | evaluate_ltl_formula(Condition,StateTransitionHistory,Type,ltl:check_ap,ltl:callback_tp,EvResult), | |
2391 | EvResult = false, | |
2392 | !, | |
2393 | RESULT=ltl_found. | |
2394 | find_trace_aux(CurID,Condition,Type,N,Max,StateTransitionHistory,STTail,Names,RESULT) :- | |
2395 | user:tcltk_compute_options(CurID,ActionsAndIDs), | |
2396 | debug_println(9,opts(ActionsAndIDs)), | |
2397 | ( N=Max | |
2398 | -> debug_println(9,'Maximum number of animation steps reached.'), | |
2399 | Names = [], | |
2400 | RESULT = maximum_nr_of_steps_reached | |
2401 | ; pick_action(random,ActionsAndIDs,ActionId,Name,DstID) % pick first one; we could do random | |
2402 | -> debug_println(9,performing_action(ActionId,from_to(CurID,DstID),opts(ActionsAndIDs))), | |
2403 | STTail = [strans(CurID,ActionId)|STTail2], | |
2404 | Names = [Name|Names2], | |
2405 | N1 is N+1, | |
2406 | find_trace_aux(DstID,Condition,Type,N1,Max,StateTransitionHistory,STTail2,Names2,RESULT) | |
2407 | ; otherwise | |
2408 | -> STTail=[], Names = [], RESULT = deadlock | |
2409 | ). | |
2410 | ||
2411 | gen_op_triples([],[],[]). | |
2412 | gen_op_triples([_X],[_Y],[]). | |
2413 | gen_op_triples([strans(CurID,ActionId),strans(DstID,ActId)|T],[Name|NameT],[op(ActionId,Name,CurID,DstID)|Rest]) :- | |
2414 | gen_op_triples([strans(DstID,ActId)|T],NameT,Rest). | |
2415 | ||
2416 | :- use_module(library(random)). | |
2417 | :- use_module(library(lists)). | |
2418 | pick_action(first,[(ActionId,Term,DstID)|_], ActionId, Name, DstID) :- extract_op_name(Term,Name). | |
2419 | pick_action(random,Options,ActionId, Name, DstID) :- | |
2420 | length(Options,Len), | |
2421 | L1 is Len+1, | |
2422 | random(1,L1,RanChoice), | |
2423 | debug_println(9,random(RanChoice,Len)), | |
2424 | nth1(RanChoice,Options,(ActionId,ActionAsTerm,DstID)), | |
2425 | extract_op_name(ActionAsTerm,Name). | |
2426 | ||
2427 | ||
2428 | % ------------------------------------- | |
2429 | ||
2430 | % an execution engine with minimal overhead: states are not stored in visited_expression database, only first enabled operation is taken | |
2431 | :- mode execute_model(+CurStateID,+MaxNrSteps,-TransitionInfo,-ExecutedSteps,-Result). | |
2432 | execute_model(CurStateID,MaxNrSteps,TransitionInfo,ExecutedSteps,Result) :- | |
2433 | execute_model(CurStateID,MaxNrSteps,[],TransitionInfo,ExecutedSteps,Result). | |
2434 | ||
2435 | :- mode execute_model(+CurStateID,+MaxNrSteps,+Options,-TransitionInfo,-ExecutedSteps,-Result). | |
2436 | % Options can contain continue_after_errors, timeout(MS) | |
2437 | % Result is either maximum_nr_of_steps_reached, deadlock, error, internal_error, time_out | |
2438 | execute_model(CurStateID,MaxNrSteps,Options,TransitionInfo,ExecutedSteps,Result) :- | |
2439 | visited_expression(CurStateID,CurState), | |
2440 | % we could do something like prepare_state_for_specfile_trans(CurState,CurState2) + ensure that the individual steps do not repack constants | |
2441 | execute_model_steps(0,CurState,MaxNrSteps,Options,NewState,ExecutedSteps,Result), | |
2442 | (ExecutedSteps>0 | |
2443 | -> user:tcltk_add_new_transition_transid(CurStateID,'$JUMP'('EXECUTE'(ExecutedSteps)),ToID,NewState,[],TransId), | |
2444 | debug_println(4,added_transition_for_execute(ExecutedSteps,ToID)), | |
2445 | user:tcltk_goto_state('$JUMP'('EXECUTE'(ExecutedSteps)),ToID), | |
2446 | TransitionInfo = op(TransId,'EXECUTE',CurStateID,ToID) | |
2447 | ; TransitionInfo = none). | |
2448 | ||
2449 | execute_model_steps(StepNr,CurState,MaxNrSteps,_Options,NewState,ExecutedSteps,Result) :- | |
2450 | StepNr >= MaxNrSteps,!, | |
2451 | NewState=CurState, | |
2452 | ExecutedSteps=StepNr, Result=maximum_nr_of_steps_reached. | |
2453 | execute_model_steps(StepNr,CurState,MaxNrSteps,Options,NewState,ExecutedSteps,Result) :- | |
2454 | cli_trans_aux(StepNr,CurState,Options,ActionName,_Act,State2,ErrorRes), | |
2455 | !, | |
2456 | debug_println(20,execute(StepNr,ActionName)), | |
2457 | %print(step(StepNr,Act,State2)),nl, | |
2458 | S1 is StepNr+1, | |
2459 | (nonvar(ErrorRes) -> Result=ErrorRes, ExecutedSteps=StepNr, NewState=CurState | |
2460 | ; execute_model_steps(S1,State2,MaxNrSteps,Options,NewState,ExecutedSteps,Result)). | |
2461 | execute_model_steps(Steps,CurState,_,_Options,CurState,Steps,deadlock). | |
2462 | ||
2463 | :- use_module(specfile,[specfile_trans_or_partial_trans/6]). | |
2464 | :- use_module(error_manager,[throw_enumeration_warnings_in_current_scope/0, add_internal_error/2, error_occurred_in_error_scope/0]). | |
2465 | :- use_module(tools_meta,[safe_time_out/3]). | |
2466 | ||
2467 | cli_trans_aux(StepNr,CurState,Options,ActionName,Act,NewState,ErrorRes) :- | |
2468 | catch_enumeration_warning_exceptions( | |
2469 | (throw_enumeration_warnings_in_current_scope, | |
2470 | (member(timeout(MS),Options) -> | |
2471 | safe_time_out(specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo,Residue),MS,TR) | |
2472 | ; specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo,Residue) % no time-out ! | |
2473 | ), | |
2474 | (TR==time_out | |
2475 | -> add_error(execute,'Timeout occured during execute after step: ',StepNr),ErrorRes=time_out | |
2476 | ; error_occurred_in_error_scope -> | |
2477 | (member(continue_after_errors,Options) -> true | |
2478 | ; add_error(execute,'Error occured during execute after step: ',StepNr),ErrorRes=error) | |
2479 | ; true) | |
2480 | ), | |
2481 | (add_error(virtual_time_out_execute,'Virtual TIME-OUT occured during execute after step: ',StepNr), | |
2482 | ActionName = '*** VIRTUAL_TIME_OUT ***', Act=ActionName, | |
2483 | ErrorRes=time_out) | |
2484 | ), | |
2485 | (Residue=[] -> true | |
2486 | ; add_internal_error('Residue during execute after step: ',StepNr:Residue), | |
2487 | (nonvar(ErrorRes) -> true ; ErrorRes=internal_error)). | |
2488 | ||
2489 | % ------------------------------------- | |
2490 | ||
2491 | get_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :- | |
2492 | typecheck_pred_for_unsat_core(Pred,TypedPred), | |
2493 | maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds), | |
2494 | conjunct_predicates(TypedFixedPreds,Conj), | |
2495 | unsat_core_with_fixed_conjuncts(TypedPred,Conj,Core), | |
2496 | translate_bexpression(Core,CoreOut). | |
2497 | ||
2498 | get_minimum_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :- | |
2499 | typecheck_pred_for_unsat_core(Pred,TypedPred), | |
2500 | maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds), | |
2501 | conjunct_predicates(TypedFixedPreds,Conj), | |
2502 | minimum_unsat_core_with_fixed_conjuncts(TypedPred,Conj,Core), | |
2503 | translate_bexpression(Core,CoreOut). | |
2504 | ||
2505 | typecheck_pred_for_unsat_core(PIn,POut) :- | |
2506 | evaluate_formula_typecheck('#PREDICATE',PIn,POutT,[]), | |
2507 | get_texpr_expr(POutT,exists(_,POut)). | |
2508 | ||
2509 | /** | |
2510 | Access information about the current version of the ProB core. | |
2511 | ||
2512 | #### called by: | |
2513 | * ProB 2.0: GetInternalRepresentationPrettyPrintCommand | |
2514 | */ | |
2515 | :- use_module(specfile,[get_internal_representation/1]). | |
2516 | get_pretty_print(PP) :- | |
2517 | get_internal_representation(PPC), | |
2518 | atom_codes(PP,PPC). | |
2519 | ||
2520 | :- use_module(symbolic_model_checker(predicate_handling)). | |
2521 | get_primed_predicate(Pred,PrimedPredOut) :- | |
2522 | evaluate_formula_typecheck('#PREDICATE',Pred,POutT,[]), | |
2523 | prime_predicate(POutT,PrimedPred), | |
2524 | translate_bexpression(PrimedPred,PrimedPredOut). | |
2525 | ||
2526 | :- use_module(weakest_preconditions). | |
2527 | :- use_module(preferences, [call_with_preference/3]). | |
2528 | get_weakest_precondition(OpName,Pred,WPOut) :- % TODO: call with preference can be removed once ProB 2 reads ASTs instead of reparsing | |
2529 | call_with_preference(get_weakest_precondition_aux(OpName,Pred,WPOut),translate_ids_to_parseable_format,true). | |
2530 | get_weakest_precondition_aux(OpName,Pred,WPOut) :- | |
2531 | b_get_machine_operation(OpName,_Results,_Parameters,OpBody), | |
2532 | evaluate_formula_typecheck('#PREDICATE',Pred,POutT,[]), | |
2533 | weakest_precondition(OpBody,POutT,WP), | |
2534 | translate_bexpression(WP,WPOut). | |
2535 | ||
2536 | :- use_module(before_after_predicates,[before_after_predicate_for_operation/2]). | |
2537 | before_after_predicate(OpName,PredicateOut) :- | |
2538 | call_with_preference(before_after_predicate_aux(OpName,PredicateOut),translate_ids_to_parseable_format,true). | |
2539 | before_after_predicate_aux(OpName,PredicateOut) :- | |
2540 | before_after_predicate_for_operation(OpName,Predicate), | |
2541 | translate_bexpression(Predicate,PredicateOut). | |
2542 | ||
2543 | /** Synthesis Commands: | |
2544 | * | |
2545 | #### b_synthesis:start_synthesis_from_ui/13 called by: | |
2546 | * ProB 2.0: BSynthesisCommand | |
2547 | */ | |
2548 | start_synthesis_from_ui_(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing) :- | |
2549 | start_synthesis_from_ui(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing). | |
2550 | ||
2551 | /* | |
2552 | #### b_synthesis:start_synthesis_single_operation_from_ui/11 called by: | |
2553 | * BSynthesis: StartSynthesisCommand | |
2554 | */ | |
2555 | start_synthesis_single_operation_from_ui_(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing) :- | |
2556 | start_synthesis_single_operation_from_ui(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing). | |
2557 | ||
2558 | /* | |
2559 | #### b_synthesis:reset_synthesis_context/0 called by: | |
2560 | * ProB 2.0: ResetBSynthesisCommand | |
2561 | */ | |
2562 | reset_synthesis_context_ :- reset_synthesis_context. | |
2563 | ||
2564 | /* | |
2565 | #### synthesis_util:get_invariant_violating_vars_from_examples/3 called by: | |
2566 | * BSynthesis: GetViolatingVarsFromExamples | |
2567 | */ | |
2568 | get_invariant_violating_vars_from_examples_(Positive,Negative,ViolatingVarNames) :- | |
2569 | get_invariant_violating_vars_from_examples(Positive,Negative,ViolatingVarNames). | |
2570 | ||
2571 | /* | |
2572 | #### synthesis_util:get_valid_and_invalid_equality_predicates_for_operation/6 called by: | |
2573 | * BSynthesis: VisualizeOperationCommand | |
2574 | */ | |
2575 | get_valid_and_invalid_equality_predicates_for_operation_(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs) :- | |
2576 | get_valid_and_invalid_equality_predicates_for_operation(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs). | |
2577 | ||
2578 | /* | |
2579 | #### synthesis_util:get_valid_and_invalid_equality_predicates_for_invariants/4 called by: | |
2580 | * BSynthesis: VisualizeInvariantsCommand | |
2581 | */ | |
2582 | get_valid_and_invalid_equality_predicates_for_invariants_(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities) :- | |
2583 | get_valid_and_invalid_equality_predicates_for_invariants(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities). | |
2584 | ||
2585 | /* | |
2586 | #### synthesis_util:adapt_machine_code_for_operations/2 called by: | |
2587 | * BSynthesis: AdaptMachineCodeForOperationsCommand | |
2588 | */ | |
2589 | adapt_machine_code_for_operations_(Operations,NewMachineAtom) :- | |
2590 | adapt_machine_code_for_operations(Operations,NewMachineAtom). | |
2591 | ||
2592 | /* | |
2593 | #### predicate_data_generator:generate_synthesis_data_from_predicate_/5 called by: | |
2594 | * BSynthesisDataGenerator: SynthesisDataFromPredicateCommand | |
2595 | */ | |
2596 | generate_synthesis_data_from_predicate_(MachinePath, AugmentRecords, SolverTimeoutMs, RawPredicate, AugmentedSetOfData) :- | |
2597 | generate_synthesis_data_from_predicate(MachinePath, AugmentRecords, SolverTimeoutMs, RawPredicate, AugmentedSetOfData). | |
2598 | ||
2599 | /* | |
2600 | #### called by: | |
2601 | * ProB 2.0: GetMachineOperationNamesCommand | |
2602 | */ | |
2603 | :- use_module(probcspsrc(haskell_csp),[channel/2]). | |
2604 | ||
2605 | csp_channel_or_start('start_cspm_MAIN'). | |
2606 | csp_channel_or_start('start_cspm'). % TO DO: do we also need to support print channel ? | |
2607 | csp_channel_or_start(Name) :- channel(Name,_). | |
2608 | ||
2609 | get_machine_operation_names(MachineOperationNames) :- b_mode,!, | |
2610 | findall(MachineOperationName,b_is_operation_name(MachineOperationName),MachineOperationNames). | |
2611 | get_machine_operation_names(ChannelNames) :- csp_mode,!, | |
2612 | findall(Name, csp_channel_or_start(Name),ChannelNames). | |
2613 | get_machine_operation_names([]). | |
2614 | ||
2615 | :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]). | |
2616 | :- use_module(probsrc(bmachine),[b_get_operation_non_det_modifies/2, b_get_operation_normalized_read_write_info/3]). | |
2617 | % get list of operation info terms of the form | |
2618 | % operation_info(Name,ResultNames,ParameterNames,TopLevel,OType) | |
2619 | % where ResultNames and ParameterNames are list of atomic names | |
2620 | % TopeLevel is true if the operation is a top-level operation for animation/model checking | |
2621 | % OType is classic, csp or eventb_operation %was eventb_operation(ChangeSet,ParaValues,Operation) | |
2622 | get_machine_operation_infos(MachineOperationInfos) :- b_mode,!, | |
2623 | % TODO: ensure that we do not need to consider preference(show_eventb_any_arguments,EVENTB) | |
2624 | % TODO: examine what happens for CSP||B | |
2625 | findall(operation_info(Name,ResultNames,ParameterNames,TopLevel,OTypeF,Read,Modified,NonDetModifies), | |
2626 | (b_get_machine_operation(Name,Results,RealParameters,_RealBody,OType,_OpPos), | |
2627 | maplist(get_texpr_id,Results,ResultNames), | |
2628 | maplist(get_texpr_id,RealParameters,ParameterNames), | |
2629 | functor(OType,OTypeF,_), | |
2630 | % TO DO: obtain machine file or machine name | |
2631 | (b_top_level_operation(Name) -> TopLevel = true ; TopLevel=false), | |
2632 | (b_get_operation_normalized_read_write_info(Name,OpRead,Modified) | |
2633 | -> exclude(op_id,OpRead,Read) | |
2634 | % exclude query operations called in expressions (allow_operation_calls_in_expr); | |
2635 | %ProB2 Java cannot deal with it and raises exception for non-atomic identifiers | |
2636 | ; (Read,Modified)=(unknown,unknown)), | |
2637 | (b_get_operation_non_det_modifies(Name,NonDetModifies) -> true ; NonDetModifies=unknown) | |
2638 | ), | |
2639 | MachineOperationInfos). | |
2640 | get_machine_operation_infos(ChannelInfos) :- csp_mode,!, | |
2641 | findall(operation_info(Name,[],[],true,csp,[],[],[]), csp_channel_or_start(Name),ChannelInfos). | |
2642 | get_machine_operation_infos([]). | |
2643 | ||
2644 | op_id(op(_)). | |
2645 | ||
2646 | :- use_module(b_global_sets,[b_global_set/1, is_b_global_constant/3]). | |
2647 | :- use_module(bmachine,[b_get_machine_constants/1,b_get_machine_variables/1,b_get_definition/5,b_filenumber/4]). | |
2648 | ||
2649 | :- mode get_machine_identifiers(+Category, -ListOfIdentifiers). | |
2650 | get_machine_identifiers(machines,MN) :- | |
2651 | findall(FID, (b_filenumber(FID,Type,_,_),Type \= def),MN). | |
2652 | get_machine_identifiers(definition_files,DFN) :- | |
2653 | findall(FID, b_filenumber(FID,def,_,_),DFN). | |
2654 | get_machine_identifiers(definitions,DN) :- | |
2655 | findall(DefID,b_get_definition(DefID,_,_,_,_),DN). | |
2656 | get_machine_identifiers(sets,Sets) :- | |
2657 | findall(GS,b_global_set(GS),Sets). | |
2658 | get_machine_identifiers(set_constants,Csts) :- | |
2659 | findall(Cst,is_b_global_constant(_GS,_,Cst),Csts). | |
2660 | get_machine_identifiers(constants,CN) :- | |
2661 | b_get_machine_constants(Constants), | |
2662 | get_texpr_ids(Constants,CN). | |
2663 | get_machine_identifiers(variables,VN) :- | |
2664 | b_get_machine_variables(Variables), | |
2665 | get_texpr_ids(Variables,VN). | |
2666 | get_machine_identifiers(operations,Ops) :- | |
2667 | findall(Op,b_top_level_operation(Op),Ops). | |
2668 | ||
2669 | get_all_machine_identifiers(SortedAllIDs) :- | |
2670 | findall(ID,get_machine_identifiers(_,ID),LIds), append(LIds,AllIDs), | |
2671 | sort(AllIDs,SortedAllIDs). | |
2672 | ||
2673 | % get a list of all machine files: TO DO: extend for CSP, ... | |
2674 | get_machine_files(Files) :- | |
2675 | findall(b_file(Name,Extension,Filename),b_filenumber(Name,Extension,_,Filename), Files). | |
2676 | ||
2677 | % a predicate to obtain possible identifier completions for current machine: | |
2678 | :- use_module(tools_matching,[fuzzy_match_codes_lower_case/2, codes_to_lower_case/2, get_current_keywords/1]). | |
2679 | get_possible_completions(ID,Options,Completions) :- | |
2680 | get_match_ids(Options,SortedAllIDs), | |
2681 | atom_codes(ID,IDCodes0), | |
2682 | (member(lower_case,Options) -> codes_to_lower_case(IDCodes0,IDCodes), Opt=lower_case | |
2683 | ; Opt=case_sensitive, IDCodes = IDCodes0), | |
2684 | findall(Target,(member(Target,SortedAllIDs),atom_codes(Target,TargetCodes), | |
2685 | match(Opt,IDCodes,TargetCodes)),Completions). | |
2686 | ||
2687 | match(case_sensitive,Pattern,TargetCodes) :- !, prefix(TargetCodes,Pattern). | |
2688 | match(lower_case,Pattern,TargetCodes) :- codes_to_lower_case(TargetCodes,TC2), prefix(TC2,Pattern). | |
2689 | ||
2690 | get_possible_fuzzy_matches(ID,FuzzyMatches) :- | |
2691 | get_match_ids([keywords],SortedAllIDs), | |
2692 | atom_codes(ID,IDCodes), | |
2693 | findall(Target,(member(Target,SortedAllIDs),atom_codes(Target,TargetCodes), | |
2694 | fuzzy_match_codes_lower_case(IDCodes,TargetCodes)),FuzzyMatches). | |
2695 | ||
2696 | :- use_module(library(ordsets),[ord_union/3]). | |
2697 | get_match_ids(Options,Ids) :- member(keywords,Options),!, | |
2698 | get_all_machine_identifiers(SortedAllIDs), | |
2699 | get_current_keywords(Keywords), | |
2700 | ord_union(SortedAllIDs,Keywords,Ids). | |
2701 | get_match_ids(_,SortedAllIDs) :- get_all_machine_identifiers(SortedAllIDs). | |
2702 | % ----------------------- | |
2703 | ||
2704 | % preliminary predicate for obtaining values as raw Prolog terms | |
2705 | % sample call: prob2_interface:evaluate_expression_prolog(0,boolean_true(pos(13,1,6,5,6,7)),R). | |
2706 | evaluate_expression_prolog(StateId,RawAST,NValuePrologTerm) :- | |
2707 | evaluate_expression_prolog(StateId,RawAST,_,NValuePrologTerm). | |
2708 | evaluate_expression_prolog(StateId,RawAST,TypedAST,NValuePrologTerm) :- | |
2709 | get_eval_scope(Scope), | |
2710 | b_type_expression(RawAST,Scope,_Type,TypedAST,Errors), | |
2711 | Errors=[], | |
2712 | get_state(StateId, State), | |
2713 | evaluate_expression(State,TypedAST,force,_SRes,NValuePrologTerm). |