1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(state_space, | |
6 | [get_state_space_stats/3, get_state_space_stats/4, | |
7 | gen_new_state_id/1, | |
8 | history/1, forward_history/1, | |
9 | get_action_trace/1, % old trace/1 | |
10 | get_action_trace_with_limit/2, | |
11 | get_action_term_trace/1, | |
12 | op_trace_ids/1, add_to_op_trace_ids/1, remove_from_op_trace_ids/1, reset_op_trace_ids/0, | |
13 | get_state_id_trace/1, | |
14 | current_state_id/1, current_expression/2, | |
15 | set_current_state_id/1, | |
16 | current_options/1, set_current_options/1, | |
17 | get_current_predecessor_state_id/1, | |
18 | ||
19 | add_id_at_front/1, add_id_at_end/1, | |
20 | add_id_random/1, /* from state_space_open_nodes_c */ | |
21 | add_id_with_weight/2, add_id_to_process/3, | |
22 | pop_id_from_front/1, pop_id_from_end/1, pop_id_oldest/1, | |
23 | retract_open_node/1, open_ids_empty/0, | |
24 | top_front_id/1, top_front_weight/1, | |
25 | ||
26 | visited_expression/3, visited_expression/2, visited_expression_id/1, | |
27 | find_hashed_packed_visited_expression/3, | |
28 | retract_visited_expression/2, | |
29 | not_all_transitions_added/1, | |
30 | not_invariant_checked/1, set_invariant_checked/1, | |
31 | invariant_not_yet_checked/1, invariant_still_to_be_checked/1, | |
32 | not_interesting/1, % nodes ignored because they do not satisfy a user-provided scope predicate | |
33 | mark_as_not_interesting/1, | |
34 | max_reached_for_node/1, | |
35 | max_reached_or_timeout_for_node/1, | |
36 | use_no_timeout/1, time_out_for_node/1, time_out_for_node/3, | |
37 | hash_to_id/2,id_to_marker/2, hash_to_nauty_id/2, | |
38 | invariant_violated/1, time_out_for_invariant/1, time_out_for_assertions/1, | |
39 | set_invariant_violated/1, | |
40 | ||
41 | state_error_exists/0, state_error/3, store_state_error/3, | |
42 | set_context_state/1, set_context_state/2, | |
43 | update_context_state/1, clear_context_state/0, get_current_context_state/1, | |
44 | store_error_for_context_state/2, | |
45 | copy_current_errors_to_state/2, | |
46 | store_abort_error_for_context_state_if_possible/4, | |
47 | ||
48 | transition/3,transition/4, any_transition/3, | |
49 | store_transition/4, | |
50 | deadlocked_state/1, % no outgoing edge | |
51 | is_initial_state_id/1, is_concrete_constants_state_id/1, | |
52 | multiple_concrete_constants_exist/0, | |
53 | get_constants_state_for_id/2, get_constants_state_id_for_id/2, | |
54 | try_get_unique_constants_state/1, | |
55 | get_constants_id_for_state_id/2, | |
56 | get_variables_state_for_id/2, | |
57 | out_degree/2, | |
58 | operation_not_yet_covered/1, operation_name_not_yet_covered/1, | |
59 | get_operation_name_coverage_infos/4, | |
60 | mark_operation_as_covered/1, | |
61 | initialise_operation_not_yet_covered/0, | |
62 | ||
63 | transition_info/2, store_transition_infos/2, | |
64 | keep_transition_info/1, | |
65 | compute_transitions_if_necessary/1, | |
66 | ||
67 | state_space_initialise/0, state_space_initialise_with_stats/0, | |
68 | state_space_reset/0, | |
69 | state_space_add/2, state_space_packed_add/2, | |
70 | delete_node/1, | |
71 | ||
72 | current_state_corresponds_to_initialised_b_machine/0, | |
73 | current_state_corresponds_to_fully_setup_b_machine/0, | |
74 | current_state_corresponds_to_setup_constants_b_machine/0, | |
75 | visited_state_corresponds_to_initialised_b_machine/1, | |
76 | visited_state_corresponds_to_setup_constants_b_machine/1, | |
77 | ||
78 | specialized_inv/2, %reuse_operation/4, | |
79 | assert_max_reached_for_node/1, assert_time_out_for_node/3, | |
80 | assert_time_out_for_invariant/1, assert_time_out_for_assertions/1, | |
81 | ||
82 | set_max_nr_of_new_impl_trans_nodes/1, | |
83 | get_max_nr_of_new_impl_trans_nodes/1, | |
84 | impl_trans_term/3, impl_trans_term_all/2, | |
85 | impl_trans_id/4, | |
86 | compute_transitions_if_necessary_saved/1, | |
87 | max_nr_of_new_nodes_limit_not_reached/0, | |
88 | ||
89 | find_trace_to_initial_state/2, find_initialised_states/1, | |
90 | ||
91 | tcltk_save_state_space/1, tcltk_load_state/1, | |
92 | compute_full_state_space_hash/1, | |
93 | ||
94 | execute_id_trace_from_current/3, | |
95 | set_trace_by_transition_ids/1, try_set_trace_by_transition_ids/1, | |
96 | extend_trace_by_transition_ids/1, | |
97 | extract_term_trace_from_transition_ids/2, | |
98 | ||
99 | add_counterexample_node/1, add_counterexample_op/1, | |
100 | reset_counterexample/0, set_counterexample_by_transition_ids/1, | |
101 | counterexample_node/1, counterexample_op/1 % specific predicates to register counter examples | |
102 | ]). | |
103 | ||
104 | :- use_module(library(lists)). | |
105 | ||
106 | :- use_module(self_check). | |
107 | :- use_module(error_manager). | |
108 | :- use_module(gensym). | |
109 | :- use_module(preferences). | |
110 | :- use_module(tools). | |
111 | %:- use_module(state_space_exploration_modes,[compute_hash/3]). | |
112 | ||
113 | :- use_module(extension('counter/counter'), | |
114 | [counter_init/0, new_counter/1, get_counter/2, inc_counter/1, inc_counter/2, inc_counter_by/2, reset_counter/1, set_counter/2]). | |
115 | ||
116 | :- use_module(module_information). | |
117 | :- module_info(group,state_space). | |
118 | :- module_info(description,'This module keeps track of the visited states by the animator/model checker.'). | |
119 | ||
120 | % ---------------------------------- | |
121 | ||
122 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
123 | :- if((environ(prob_myheap,false) ; \+ predicate_property(load_foreign_resource(_), _))). | |
124 | :- use_module(state_space_open_nodes). %% comment in to use only Prolog datastructures | |
125 | :- else. | |
126 | :- use_module(state_space_open_nodes_c). %% comment in to use C++ multimap queue; can make use of HEURISTIC_FUNCTION | |
127 | :- endif. | |
128 | ||
129 | % ---------------------------------- | |
130 | ||
131 | get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes) :- | |
132 | get_counter(states,N), NrNodes is N+1, | |
133 | get_counter(transitions,NrTransitions), | |
134 | get_counter(processed_nodes,ProcessedNodes). | |
135 | ||
136 | get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes,IgnoredNodes) :- | |
137 | get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes), | |
138 | get_counter(not_interesting_nodes,IgnoredNodes). | |
139 | ||
140 | gen_new_state_id(Nr) :- | |
141 | inc_counter(states,N1), Nr is N1-1. % only one C call | |
142 | %get_counter(states,Nr), inc_counter(states). | |
143 | reset_state_counter :- reset_counter(states). | |
144 | reset_state_counter(Nr) :- set_counter(states,Nr). | |
145 | ||
146 | get_state_id_trace(StateIds) :- | |
147 | history(History), | |
148 | current_state_id(CurID), | |
149 | reverse([CurID|History],StateIds). | |
150 | ||
151 | get_current_predecessor_state_id(PriorID) :- | |
152 | history([PriorID|_]). | |
153 | ||
154 | :- dynamic history/1. | |
155 | history([]). | |
156 | ||
157 | ||
158 | :- dynamic forward_history/1. | |
159 | ||
160 | :- dynamic current_state_id/1. | |
161 | current_state_id(root). | |
162 | /* INITIAL STATE, third arg: clp(fd) constraints as generated | |
163 | by fd_copy_term */ | |
164 | ||
165 | current_expression(ID,State) :- current_state_id(ID), | |
166 | visited_expression(ID,State). | |
167 | current_packed_expression(ID,State) :- current_state_id(ID), | |
168 | packed_visited_expression(ID,State). | |
169 | ||
170 | :- use_module(specfile,[state_corresponds_to_initialised_b_machine/1, | |
171 | state_corresponds_to_fully_setup_b_machine/1, | |
172 | state_corresponds_to_set_up_constants/1]). | |
173 | current_state_corresponds_to_initialised_b_machine :- | |
174 | current_packed_expression(_,PS), unpack_state_top_level(PS,TLState), | |
175 | state_corresponds_to_initialised_b_machine(TLState). | |
176 | visited_state_corresponds_to_initialised_b_machine(ID) :- | |
177 | packed_visited_expression(ID,PS), unpack_state_top_level(PS,TLState), | |
178 | state_corresponds_to_initialised_b_machine(TLState). | |
179 | ||
180 | current_state_corresponds_to_fully_setup_b_machine :- | |
181 | current_packed_expression(_,PS), unpack_state_top_level(PS,TLState), | |
182 | state_corresponds_to_fully_setup_b_machine(TLState). | |
183 | ||
184 | current_state_corresponds_to_setup_constants_b_machine :- | |
185 | current_packed_expression(_,PS), unpack_state_top_level(PS,TLState), | |
186 | state_corresponds_to_set_up_constants(TLState). | |
187 | ||
188 | visited_state_corresponds_to_setup_constants_b_machine(ID) :- | |
189 | packed_visited_expression(ID,PS), unpack_state_top_level(PS,TLState), | |
190 | state_corresponds_to_set_up_constants(TLState). | |
191 | ||
192 | :- dynamic current_options/1. | |
193 | current_options([]). | |
194 | ||
195 | set_current_options(Options) :- | |
196 | retractall( current_options(_) ), | |
197 | assertz( current_options(Options) ). | |
198 | ||
199 | :- dynamic packed_visited_expression/2. | |
200 | %packed_visited_expression(v_0,true). | |
201 | ||
202 | :- use_module(state_packing). | |
203 | ||
204 | retract_visited_expression(ID,State) :- retract(packed_visited_expression(ID,PState)), | |
205 | unpack_state(PState,State). | |
206 | ||
207 | retractall_visited_expression(ID) :- retractall(packed_visited_expression(ID,_)). | |
208 | ||
209 | state_space_packed_add(Id,PackedTerm) :- assertz(packed_visited_expression(Id,PackedTerm)). | |
210 | ||
211 | state_space_add(Id,Term) :- | |
212 | (pack_state(Term,PackedTerm) -> assertz(packed_visited_expression(Id,PackedTerm)) | |
213 | ; add_internal_error('State packing failed: ',pack_state(Term,_)), | |
214 | assertz(packed_visited_expression(Id,Term))). | |
215 | ||
216 | % deprecated: | |
217 | visited_expression(ID,State,true) :- visited_expression(ID,State). | |
218 | % not call(CurBody); for the moment we always have true as last argument | |
219 | ||
220 | visited_expression(A,B) :- packed_visited_expression(A,PB), | |
221 | (unpack_state(PB,R) -> B=R ; add_internal_error('Unpacking state failed: ',unpack_state(PB,R)),R=A). | |
222 | ||
223 | %visited_expression_id(A) :- packed_visited_expression(A,_). % avoid unpacking state | |
224 | % even better: not to look up fact at all to avoid constructing state term, this is done below: | |
225 | :- use_module(library(between),[between/3]). | |
226 | visited_expression_id(ID) :- number(ID),!, ID>=0, get_counter(states,N), ID<N. | |
227 | visited_expression_id(ID) :- ID==root,!. | |
228 | visited_expression_id(root). | |
229 | visited_expression_id(Nr) :- Nr \== root, get_counter(states,N), N1 is N-1, between(0,N1,Nr). | |
230 | ||
231 | % given a hash and a packed state: find ID (fail if does not exist) | |
232 | find_hashed_packed_visited_expression(Hash,PackedState,ID) :- | |
233 | hash_to_id(Hash,ID), | |
234 | (packed_visited_expression(ID,PackedState) | |
235 | -> true /* warning: may instantiate State if not ground */ | |
236 | ; print(hash_collision(Hash,ID)),nl,fail | |
237 | ). | |
238 | ||
239 | ||
240 | :- dynamic not_invariant_checked/1. | |
241 | set_invariant_checked(ID) :- %print(inv_checked(ID)),nl, | |
242 | retract(not_invariant_checked(ID)). | |
243 | ||
244 | invariant_not_yet_checked(ID) :- | |
245 | not_all_transitions_added(ID) ; /* assumption: if not all transitions added then we haven't checked invariant yet */ | |
246 | not_invariant_checked(ID) ; | |
247 | not_interesting(ID). % assumption: if a node is marked as not interesting it will not be examined | |
248 | ||
249 | % difference with invariant_not_yet_checked: not interesting nodes not reported and cannot be backtracked | |
250 | invariant_still_to_be_checked(ID) :- | |
251 | (not_all_transitions_added(ID) -> true ; not_invariant_checked(ID) -> true). | |
252 | ||
253 | :- dynamic not_interesting/1. | |
254 | %not_interesting(v_0). | |
255 | ||
256 | :- dynamic max_reached_for_node/1. | |
257 | /* true if not all outgoing transistions were computed due to the limit | |
258 | on the number of operations/initialisations computed */ | |
259 | :- dynamic time_out_for_node/3, use_no_timeout/1, time_out_for_invariant/1, time_out_for_assertions/1. | |
260 | ||
261 | time_out_for_node(ID) :- (var(ID) -> visited_expression_id(ID) ; true), | |
262 | (time_out_for_node(ID,_,_) -> true ; fail). | |
263 | ||
264 | :- dynamic transition/4. | |
265 | %transition(v_0,a,1,v_1). | |
266 | ||
267 | store_transition(Org,Action,Dest,Id) :- | |
268 | %get_counter(transitions,Id), inc_counter(transitions), | |
269 | inc_counter(transitions,Id1), Id is Id1-1, % only one C call | |
270 | assertz(transition(Org,Action,Id,Dest)). | |
271 | ||
272 | deadlocked_state(Origin) :- \+ any_transition(Origin,_,_). | |
273 | ||
274 | is_concrete_constants_state_id(ID) :- | |
275 | transition(root,_,ID), | |
276 | packed_visited_expression(ID,concrete_constants(_)). | |
277 | ||
278 | % check if we have multiple constant setups | |
279 | multiple_concrete_constants_exist :- | |
280 | is_concrete_constants_state_id(ID), | |
281 | is_concrete_constants_state_id(ID2), ID2 \= ID,!. | |
282 | ||
283 | ||
284 | is_initial_state_id(InitialStateID) :- | |
285 | transition(root,_,State), | |
286 | packed_visited_expression(State,P), | |
287 | (P = concrete_constants(_) % also covers '$partial_setup_constants' | |
288 | -> state_space:transition(State,_,InitialStateID) | |
289 | ; InitialStateID=State). | |
290 | ||
291 | % get the constants for a state (if there are constants) | |
292 | get_constants_state_for_id(ID,ConstantsState) :- | |
293 | visited_expression(ID,State), % TO DO: use packed_visited_expression for performance | |
294 | get_constants_state_aux(State,ConstantsState). | |
295 | get_constants_state_aux(concrete_constants(ConstantsState),ConstantsState). | |
296 | get_constants_state_aux(const_and_vars(ID,_),State) :- get_constants_state_for_id(ID,State). | |
297 | ||
298 | % get the staet id for associated constants state for a state (if there are constants) | |
299 | get_constants_state_id_for_id(ID,CstID) :- | |
300 | visited_expression(ID,State), % TO DO: use packed_visited_expression for performance | |
301 | get_constants_id_for_id_aux(State,ID,CstID). | |
302 | get_constants_id_for_id_aux(concrete_constants(_),ID,ID). | |
303 | get_constants_id_for_id_aux(const_and_vars(ID,_),_,ID). | |
304 | ||
305 | get_variables_state_for_id(ID,VarState) :- | |
306 | visited_expression(ID,State), | |
307 | get_vars_aux(State,VarState). | |
308 | %get_vars_aux(concrete_constants(ConstantsState),[]). | |
309 | get_vars_aux(const_and_vars(_,Vars),State) :- !, State=Vars. | |
310 | get_vars_aux([],[]). | |
311 | get_vars_aux([H|T],[H|T]). | |
312 | ||
313 | % check if there is a unique constants state: | |
314 | try_get_unique_constants_state(ConstantsState) :- | |
315 | transition(root,_,_TransID,DestID), | |
316 | \+ (transition(root,_,_,DestID2), DestID2 \= DestID), % no other transition exists | |
317 | \+ max_reached_or_timeout_for_node(root), | |
318 | DestID \= root, % DestID=root should never happen | |
319 | get_constants_state_for_id(DestID,ConstantsState). | |
320 | ||
321 | % returns id of constants state for a state (if it exists) | |
322 | get_constants_id_for_state_id(ID,ConstID) :- | |
323 | packed_visited_expression(ID,'$cst_vars'(ConstID,_)). | |
324 | ||
325 | any_transition(Origin,TransID,Destination) :- transition(Origin,_,TransID,Destination). | |
326 | ||
327 | transition(Origin,Action,Destination) :- transition(Origin,Action,_TransID,Destination). | |
328 | ||
329 | :- dynamic transition_info/2. | |
330 | store_transition_infos([],_TransId). | |
331 | store_transition_infos([Info|Irest],TransId) :- | |
332 | store_transition_info(Info,TransId), | |
333 | store_transition_infos(Irest,TransId). | |
334 | store_transition_info(Info,TransId) :- %print(info(Info,TransId)),nl, | |
335 | (keep_transition_info(Info) | |
336 | -> assertz(transition_info(TransId,Info)) | |
337 | ; true). | |
338 | ||
339 | % Do not store path info by default | |
340 | keep_transition_info(path(_)) :- !,fail. | |
341 | keep_transition_info(eventtrace(_)) :- !,preference(eventtrace,true). | |
342 | keep_transition_info(event(_)) :- !,preference(store_event_transinfo,true). | |
343 | keep_transition_info(_). % store everything else | |
344 | ||
345 | reset_transition_store :- | |
346 | retractall(transition(_,_,_,_)), | |
347 | retractall(transition_info(_,_)), | |
348 | reset_counter(transitions), | |
349 | reset_counterexample. | |
350 | ||
351 | /* | |
352 | Version with packing of transitions: | |
353 | store_transition(Org,Action,Dest,Id) :- | |
354 | retract(transition_counter(Id)), | |
355 | NewId is Id+1, | |
356 | assertz(transition_counter(NewId)), | |
357 | Action =.. [ActionName|Parameters], | |
358 | pack_values(Parameters,PackedParameters), | |
359 | assertz(packed_transition(Org,ActionName,PackedParameters,Id,Dest)). | |
360 | ||
361 | transition(Origin,Action,TransID,Destination) :- nonvar(Action),!, | |
362 | Action =.. [ActionName|Parameters], | |
363 | packed_transition(Origin,ActionName,PackedParameters,TransID,Destination), | |
364 | unpack_values(PackedParameters,Parameters). | |
365 | transition(Origin,Action,TransID,Destination) :- | |
366 | packed_transition(Origin,ActionName,PackedParameters,TransID,Destination), | |
367 | unpack_values(PackedParameters,Parameters), | |
368 | Action =.. [ActionName|Parameters]. | |
369 | any_transition(Origin,TransID,Destination) :- packed_transition(Origin,_,_,TransID,Destination). | |
370 | */ | |
371 | ||
372 | % compute out-degree of a node | |
373 | out_degree(ID,OutDegree) :- findall(0, transition(ID,_,_,_), L), length(L,OutDegree). | |
374 | ||
375 | operation_name_not_yet_covered(OpName) :- operation_not_yet_covered(OpName). | |
376 | ||
377 | ||
378 | get_operation_name_coverage_infos(PossibleNr,FeasibleNr,UncovNr,UncoveredList) :- | |
379 | findall(ON, specfile:get_possible_event(ON), Possible), length(Possible,PossibleNr), | |
380 | findall(OF, specfile:get_feasible_event(OF), Feasible), length(Feasible,FeasibleNr), | |
381 | findall(OpName, state_space: operation_name_not_yet_covered(OpName), UncoveredList), | |
382 | length(UncoveredList,UncovNr). | |
383 | ||
384 | ||
385 | :- dynamic operation_not_yet_covered/1. | |
386 | %operation_not_yet_covered(b). | |
387 | ||
388 | :- use_module(probsrc(debug),[formatsilent/2]). | |
389 | mark_operation_as_covered(OpName) :- | |
390 | (retract(operation_not_yet_covered(OpName)) | |
391 | -> (preferences:get_preference(provide_trace_information,true) | |
392 | -> print(cover(OpName)),nl ; true), | |
393 | (operation_not_yet_covered(_) -> true ; formatsilent('~nALL OPERATIONS COVERED~n',[])) | |
394 | ; true | |
395 | ). | |
396 | ||
397 | ||
398 | :- use_module(bmachine,[b_top_level_operation/1]). | |
399 | :- use_module(debug,[debug_println/1]). | |
400 | :- use_module(probcspsrc(haskell_csp),[channel/2]). | |
401 | initialise_operation_not_yet_covered :- retractall(operation_not_yet_covered(_)), | |
402 | b_or_z_mode, | |
403 | ? | b_top_level_operation(Name), |
404 | % b_get_machine_operation(Name,_,Par,_), length(Par,Arity), functor(Op,Name,Arity), | |
405 | % Note: no '-->' added | |
406 | assertz(operation_not_yet_covered(Name)), | |
407 | debug_println(operation_not_yet_covered(Name)), | |
408 | fail. | |
409 | /* Missing: treat operations with return values */ | |
410 | initialise_operation_not_yet_covered :- csp_mode, \+ csp_with_bz_mode, | |
411 | channel(Name,_), | |
412 | assertz(operation_not_yet_covered(Name)), | |
413 | debug_println(operation_not_yet_covered(Name)), | |
414 | fail. | |
415 | initialise_operation_not_yet_covered. | |
416 | ||
417 | state_error_exists :- state_error(_,_,_),!. | |
418 | :- dynamic state_error/3. | |
419 | ||
420 | %state_error([],invariant_violated). | |
421 | ||
422 | reset_next_state_error_id_counter :- reset_counter(next_state_error_id). | |
423 | :- use_module(tools_printing, [print_error/1, format_error_with_nl/2]). | |
424 | :- use_module(error_manager,[print_error_span/1]). | |
425 | store_state_error(State,Error,Id) :- state_error(State,Id,Error),!. % do not store identical error twice | |
426 | store_state_error(State,Error,Id) :- | |
427 | %retract( next_state_error_id(Id) ), | |
428 | inc_counter(next_state_error_id,Id), | |
429 | % tools_printing:print_term_summary(Error),nl, tools_printing:nested_print_term(Error),nl, | |
430 | assertz( state_error(State,Id,Error) ). | |
431 | store_error_for_context_state(Error,Id) :- | |
432 | ( context_state(State,Errs) -> | |
433 | (Errs<25 | |
434 | -> store_state_error(State,Error,Id), E1 is Errs+1, | |
435 | %assertz(context_state(State,E1)) | |
436 | set_context_number_of_errors(E1) | |
437 | ; store_state_error(State,max_state_errors_reached(25),Id) | |
438 | ) | |
439 | ; | |
440 | add_internal_error('No known context when calling store_error_for_context_state: ',store_error_for_context_state(Error,Id)), | |
441 | fail). | |
442 | ||
443 | % copy current errors from error_manager to state errors | |
444 | copy_current_errors_to_state(StateID,Context) :- | |
445 | % error_manager:logged_error(Source,ErrMsg,_Context,Span), % will not retract | |
446 | error_manager:get_error_with_span(Source,ErrMsg,Span), % will retract | |
447 | store_state_error(StateID,abort_error(Source,ErrMsg,'',span_context(Span,Context)),SID), | |
448 | % TO DO: use other error class | |
449 | debug_println(stored(Source,SID,_Context,ErrMsg)), | |
450 | fail. | |
451 | copy_current_errors_to_state(_,_). | |
452 | ||
453 | store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span) :- | |
454 | %print(store(Msg,Term,Span)),nl, | |
455 | ( get_current_context_state(State) -> | |
456 | error_manager:get_error_context(Context), | |
457 | (abort_error_for_same_location_exists(State,Id1,ErrType,Msg,Span), | |
458 | abort_error_for_same_location_exists(State,Id2,ErrType,Msg,Span), | |
459 | Id2>Id1 | |
460 | -> /* two errors of same type, for same state and same source location exists */ | |
461 | /* TO DO: maybe merge state errors */ | |
462 | simplify_span(Span,Span1), | |
463 | compress_span(Span1,Span2), | |
464 | store_state_error(State,abort_error(ErrType,'Further identical errors occurred (not stored !)',Term,span_context(Span2,Context)),_) | |
465 | ; | |
466 | format_error_with_nl('! An error occurred in state ~w: ~w !',[State,ErrType]), | |
467 | % usual errors: precondition_error, while_invariant_violation, while_variant_error, | |
468 | % assert_error, well_definedness_error | |
469 | print_error(Msg), | |
470 | print_error_term(Term,Span), | |
471 | % print_error(context_state_id(State)), % printed by print_error_context | |
472 | print_error_context, | |
473 | (debug_mode(on),visited_expression(State,S) -> translate:translate_bstate(S,O),print_error(O) ; true), | |
474 | compress_span(Span,Span2), | |
475 | print_error_span(Span2), | |
476 | store_state_error(State,abort_error(ErrType,Msg,Term,span_context(Span2,Context)),_) | |
477 | ), | |
478 | (add_new_event_in_error_scope(abort_error(ErrType)) -> true ; true), % should we use well_definedness_error? | |
479 | assert_real_error_occurred(abort_error) % Note that in this case the error manager list of errors maybe empty even though real_error_occured is true. (see ProB2 kernel test de.prob.cli.integration.rules.RulesMachineTest > testReuseStateSpace) | |
480 | ; % no current context_state exists: | |
481 | compress_span(Span,Span2), | |
482 | add_error(ErrType,Msg,Term,Span2) | |
483 | ). | |
484 | ||
485 | :- use_module(bsyntaxtree, [find_identifier_uses/3]). | |
486 | compress_span(span_context(Span,C),span_context(CS,C)) :- !, | |
487 | compress_span(Span,CS). | |
488 | compress_span(pos_context(Span1,C,Span2),pos_context(CS1,C,CS2)) :- !, | |
489 | compress_span(Span1,CS1), | |
490 | compress_span(Span2,CS2). | |
491 | compress_span(span_predicate(Pred,LS,S),Res) :- find_identifier_uses(Pred,[],Ids), | |
492 | sort(Ids,SIds), | |
493 | filter_state(LS,SIds,FLS), | |
494 | filter_state(S,SIds,FS), % TODO: do we need to store the global state? we can reconstruct it ? | |
495 | % format('Compressed span_predicate (~w)~n',[Ids]), | |
496 | !, | |
497 | Res = span_predicate(Pred,FLS,FS). | |
498 | compress_span(S,S). | |
499 | % avoid storing large useless values | |
500 | % TO DO: probably we should stop storing spans when a certain threshold of number of errors is reached | |
501 | ||
502 | ||
503 | :- use_module(library(ordsets),[ord_member/2]). | |
504 | filter_state([],_,[]). | |
505 | filter_state([bind(ID,L)|T],Vars,Res) :- | |
506 | (ord_member(ID,Vars) -> Res = [bind(ID,L)|RT] ; Res=RT), | |
507 | filter_state(T,Vars,RT). | |
508 | ||
509 | ||
510 | :- use_module(translate, [translate_error_term/3]). | |
511 | print_error_term(T,S) :- (var(T);var(S)),!, | |
512 | print_error('### VARIABLE error term or span:'), print_error(print_error_term(T,S)). | |
513 | print_error_term(Term,Span) :- translate_error_term(Term,Span,S), | |
514 | (S='' -> true ; print_error(S)). | |
515 | ||
516 | abort_error_for_same_location_exists(State,Id,ErrType,Msg,Span) :- | |
517 | state_error(State,Id,abort_error(ErrType,Msg,_Term2,span_context(Span2,_Ctxt2))), | |
518 | same_span_location(Span2,Span). | |
519 | % should be moved to error_manager ? | |
520 | same_span_location(span_context(Span1,C),span_context(Span2,C)) :- !, same_span_location(Span1,Span2). | |
521 | same_span_location(pos_context(Span1,C,_),pos_context(Span2,C,_)) :- !, | |
522 | same_span_location(Span1,Span2). % should we check second span? | |
523 | same_span_location(span_predicate(Pred1,_,_),span_predicate(Pred2,_,_)) :- !,Pred1=Pred2. | |
524 | same_span_location(X,X). | |
525 | ||
526 | :- dynamic saved_nested_context_state/2. | |
527 | save_nested_context_state(_S) :- | |
528 | bb_get(state_space_context_state,ID), | |
529 | bb_get(state_space_context_errors,Errs),!, | |
530 | %print(saving_context_state(_S,ID,Errs)),nl, | |
531 | asserta(saved_nested_context_state(ID,Errs)). | |
532 | save_nested_context_state(_). | |
533 | ||
534 | % actually pops context state | |
535 | clear_context_state :- | |
536 | retract(saved_nested_context_state(ID,Errs)),!, %print(restoring_nested(ID,Errs)),nl, | |
537 | bb_put(state_space_context_state,ID), | |
538 | bb_put(state_space_context_errors,Errs). | |
539 | clear_context_state :- | |
540 | (bb_delete(state_space_context_state,_) -> true ; true). | |
541 | %(retract(context_state(_,_)) -> true ; true). % retractall seems to be slowing down with use | |
542 | ||
543 | % Note: Each Prolog module maintains its own blackboard for bb_get/bb_put | |
544 | context_state(ID,Errs) :- | |
545 | bb_get(state_space_context_state,ID), bb_get(state_space_context_errors,Errs). | |
546 | ||
547 | % sets a new context state; pushing the previous one if necessary | |
548 | set_context_state(State) :- %print(set_id(State)),nl, | |
549 | save_nested_context_state(State), | |
550 | bb_put(state_space_context_state,State), | |
551 | bb_put(state_space_context_errors,0). | |
552 | ||
553 | set_context_state(State,_Context) :- % Context can be used for debugging later | |
554 | set_context_state(State). | |
555 | ||
556 | % update current context state, without storing nested states | |
557 | update_context_state(State) :- | |
558 | bb_put(state_space_context_state,State), | |
559 | bb_put(state_space_context_errors,0). | |
560 | ||
561 | get_current_context_state(ID) :- bb_get(state_space_context_state,ID). | |
562 | %get_current_context_state(ID) :- context_state(ID,_). | |
563 | ||
564 | set_context_number_of_errors(Errs) :- bb_put(state_space_context_errors,Errs). | |
565 | ||
566 | retractall_invariant_violated(State) :- | |
567 | retractall(state_error(State,_,invariant_violated)). | |
568 | invariant_violated(State) :- | |
569 | state_error(State,_,invariant_violated). | |
570 | set_invariant_violated(State) :- | |
571 | ( invariant_violated(State) -> true | |
572 | ; time_out_for_invariant(ID) -> print('Timeout for node: '), print(ID),nl, | |
573 | print('Not setting invariant violation status'),nl | |
574 | ; store_state_error(State,invariant_violated,_) | |
575 | ). | |
576 | ||
577 | %:- set_invariant_violated([]). % why is this ?? | |
578 | ||
579 | ||
580 | :- dynamic hash_to_id/2. | |
581 | :- dynamic id_to_marker/2. | |
582 | ||
583 | :- dynamic hash_to_nauty_id/2. % used in nauty mode to map nauty id's to hash values | |
584 | ||
585 | :- dynamic specialized_inv/2. /* stores whether for a node a specialized invariant | |
586 | version could be computed */ | |
587 | ||
588 | % :- dynamic reuse_operation/4. /* when for a state and given operation name we can reuse the operation computed for another state */ | |
589 | % used to be used for OPERATION_REUSE TRUE | |
590 | ||
591 | :- use_module(hashing). | |
592 | state_space_startup :- % call once at startup to ensure all counters exist | |
593 | counter_init, | |
594 | new_counter(states), new_counter(processed_nodes), new_counter(transitions), | |
595 | new_counter(next_state_error_id), | |
596 | new_counter(not_interesting_nodes), | |
597 | reset_open_ids. % also calls myheap init | |
598 | state_space_initialise :- counter_init, reset_gennum, reset_gensym, | |
599 | new_counter(states), new_counter(processed_nodes), new_counter(transitions), | |
600 | new_counter(next_state_error_id), new_counter(not_interesting_nodes), | |
601 | reset_state_counter, reset_processed_nodes_counter, reset_next_state_error_id_counter, | |
602 | retractall_visited_expression(_), | |
603 | reset_open_ids, | |
604 | reset_stored_values, % state_packing | |
605 | retractall(not_invariant_checked(_)), | |
606 | reset_not_interesting, | |
607 | retractall(max_reached_for_node(_)), | |
608 | retractall(time_out_for_node(_,_,_)), | |
609 | retractall(time_out_for_invariant(_)), | |
610 | retractall(time_out_for_assertions(_)), | |
611 | retractall(use_no_timeout(_)), | |
612 | retractall(state_error(_,_,_)), | |
613 | clear_context_state, | |
614 | reset_transition_store, | |
615 | retractall(operation_not_yet_covered(_)), | |
616 | retractall(hash_to_id(_,_)), | |
617 | retractall(hash_to_nauty_id(_,_)), | |
618 | retractall(id_to_marker(_,_)), | |
619 | retractall(specialized_inv(_,_)), | |
620 | %retractall(reuse_operation(_,_,_,_)), | |
621 | state_space_add(root,root), | |
622 | add_id_at_front(root), | |
623 | my_term_hash(root,RootHash), | |
624 | assertz(hash_to_id(RootHash,root)), | |
625 | %assertz(not_invariant_checked(root)), | |
626 | state_space_reset. | |
627 | ||
628 | :- use_module(eventhandling,[register_event_listener/3]). | |
629 | :- register_event_listener(startup_prob,state_space_startup, | |
630 | 'Initialise Statespace Counters.'). | |
631 | :- register_event_listener(reset_specification,state_space_initialise, | |
632 | 'Reset Statespace.'). | |
633 | :- register_event_listener(change_of_animation_mode,state_space_initialise, | |
634 | 'Reset Statespace.'). | |
635 | :- register_event_listener(specification_initialised,initialise_operation_not_yet_covered, | |
636 | 'Init coverage info.'). | |
637 | :- register_event_listener(reset_prob,state_space_initialise, | |
638 | 'Reset Statespace.'). | |
639 | ||
640 | /* A version of reset which checks how much memory is used by each fact */ | |
641 | /* state_space:init_with_stats */ | |
642 | state_space_initialise_with_stats :- | |
643 | reset_gennum, reset_gensym, reset_state_counter, reset_processed_nodes_counter, | |
644 | reset_next_state_error_id_counter, | |
645 | retract_open_ids_with_statistics, | |
646 | retract_with_statistics(state_space,[packed_visited_expression(_,_), | |
647 | not_invariant_checked(_), | |
648 | not_interesting(_), | |
649 | max_reached_for_node(_), | |
650 | time_out_for_node(_,_,_), | |
651 | time_out_for_invariant(_), | |
652 | time_out_for_assertions(_), | |
653 | use_no_timeout(_), | |
654 | state_error(_,_,_), | |
655 | transition(_,_,_,_), | |
656 | transition_info(_,_), | |
657 | operation_not_yet_covered(_), | |
658 | hash_to_id(_,_), | |
659 | hash_to_nauty_id(_,_), | |
660 | id_to_marker(_,_), | |
661 | specialized_inv(_,_), | |
662 | %reuse_operation(_,_,_,_), | |
663 | history(_), forward_history(_), op_trace_ids(_)]), | |
664 | reset_not_interesting, | |
665 | retract_stored_values_with_statistics, | |
666 | clear_context_state, | |
667 | reset_transition_store, | |
668 | state_space_add(root,root), | |
669 | add_id_at_front(root), | |
670 | %assertz(not_invariant_checked(root)), | |
671 | state_space_reset, | |
672 | initialise_operation_not_yet_covered. | |
673 | ||
674 | ||
675 | ||
676 | :- dynamic op_trace_ids/1. | |
677 | reset_trace :- retractall(op_trace_ids(_)), assertz(op_trace_ids([])). | |
678 | get_action_trace(T) :- trace(T). | |
679 | get_action_term_trace(PT) :- get_action_trace_with_limit(0,T), project_on_action_term(T,PT). | |
680 | trace(Trace) :- get_action_trace_with_limit(500,Trace). | |
681 | get_action_trace_with_limit(Limit,Trace) :- | |
682 | op_trace_ids(IDT), reverse(IDT,RIDT), | |
683 | extract_trace_from_transition_ids(RIDT,root,Limit,[],Trace). | |
684 | ||
685 | reset_op_trace_ids :- retractall(op_trace_ids(_)), assertz(op_trace_ids([])). | |
686 | add_to_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), assertz(op_trace_ids([OpID|OpIDS])). | |
687 | remove_from_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), | |
688 | (OpIDS = [R|Rest] -> assertz(op_trace_ids(Rest)), OpID = R | |
689 | ; assertz(op_trace_ids(OpIDS)),fail). | |
690 | ||
691 | % translate a list of transition ids (from root) into a list of operation terms | |
692 | extract_term_trace_from_transition_ids(TransIDListFromRoot,Trace) :- | |
693 | extract_trace_from_transition_ids(TransIDListFromRoot,root,0,[],ActionTrace), | |
694 | reverse_and_project_on_action_term(ActionTrace,[],Trace). | |
695 | ||
696 | reverse_and_project_on_action_term([],A,A). | |
697 | reverse_and_project_on_action_term([action(_,Term)|T],Acc,Res) :- !, | |
698 | reverse_and_project_on_action_term(T,[Term|Acc],Res). | |
699 | reverse_and_project_on_action_term([H|T],Acc,Res) :- | |
700 | add_error(reverse_and_project_on_action_term,'Illegal action: ',H), | |
701 | reverse_and_project_on_action_term(T,[H|Acc],Res). | |
702 | ||
703 | project_on_action_term([],[]). | |
704 | project_on_action_term([action(_,Term)|T],Res) :- !, Res=[Term|TR], | |
705 | project_on_action_term(T,TR). | |
706 | project_on_action_term([H|T],Res) :- | |
707 | add_error(project_on_action_term,'Illegal action: ',H), | |
708 | project_on_action_term(T,Res). | |
709 | ||
710 | extract_trace_from_transition_ids([],_CurrentState,_,Trace,Trace). | |
711 | extract_trace_from_transition_ids([TransId|Rest],CurrentState,Limit,AccTrace,Trace) :- | |
712 | compute_op_string(TransId,CurrentState,Limit,OpTerm,OpString,DestState),!, | |
713 | extract_trace_from_transition_ids(Rest,DestState,Limit, | |
714 | [action(OpString,OpTerm)|AccTrace],Trace). | |
715 | extract_trace_from_transition_ids([TransId|_],CurrentState,_,_,_Trace) :- | |
716 | add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail. | |
717 | ||
718 | :- use_module(translate,[translate_event_with_src_and_target_id/5]). | |
719 | compute_op_string(jump(TO),_CurID,_,Term,String,DestID) :- !, Term=jump,String=jump,DestID=TO. | |
720 | compute_op_string(TransId,CurID,Limit,Term,String,DestID) :- transition(CurID,Term,TransId,DestID), | |
721 | translate_event_with_src_and_target_id(Term,CurID,DestID,Limit,String). | |
722 | ||
723 | % reset history and forward history, but not state-space itself | |
724 | state_space_reset :- | |
725 | reset_trace, | |
726 | retractall(history(_)), | |
727 | retractall(forward_history(_)), | |
728 | retractall(current_state_id(_)), | |
729 | retractall(current_options(_)), | |
730 | assertz(history([])), | |
731 | assertz(current_state_id(root)). | |
732 | ||
733 | reset_not_interesting :- retractall(not_interesting(_)), reset_counter(not_interesting_nodes). | |
734 | ||
735 | mark_as_not_interesting(ID) :- assertz(not_interesting(ID)), inc_counter(not_interesting_nodes). | |
736 | ||
737 | set_current_state_id(ID) :- (retract(current_state_id(_)) -> true ; true), | |
738 | assertz(current_state_id(ID)). | |
739 | ||
740 | state_space_clean_all :- | |
741 | retractall(state_space_version_in_file(_)), | |
742 | retractall_visited_expression(_), | |
743 | reset_open_ids, | |
744 | retractall(not_invariant_checked(_)), | |
745 | reset_not_interesting, | |
746 | retractall(max_reached_for_node(_)), | |
747 | retractall(time_out_for_node(_,_,_)), | |
748 | retractall(time_out_for_invariant(_)), | |
749 | retractall(time_out_for_assertions(_)), | |
750 | retractall(use_no_timeout(_)), | |
751 | retractall(state_error(_,_,_)), | |
752 | clear_context_state, | |
753 | reset_transition_store, | |
754 | retractall(operation_not_yet_covered(_)), | |
755 | retractall(hash_to_id(_,_)), | |
756 | retractall(hash_to_nauty_id(_,_)), | |
757 | retractall(id_to_marker(_,_)), | |
758 | retractall(specialized_inv(_,_)), | |
759 | %retractall(reuse_operation(_,_,_,_)), | |
760 | retractall(history(_)), | |
761 | retractall(forward_history(_)), | |
762 | retractall(op_trace_ids(_)), | |
763 | retractall(current_state_id(_)), | |
764 | retractall(current_options(_)). | |
765 | ||
766 | % this is only used from within the Tcl/Tk animator at the moment: | |
767 | delete_node(ID) :- print(deleting(ID)),nl, | |
768 | retractall_visited_expression(ID), | |
769 | retractall_invariant_violated(ID), | |
770 | retract_open_node_and_update_processed_nodes(ID), | |
771 | retractall(not_invariant_checked(ID)), | |
772 | (retract(not_interesting(ID)) -> inc_counter_by(not_interesting_nodes,-1) ; true), | |
773 | retractall(max_reached_for_node(ID)), | |
774 | retractall(time_out_for_node(ID,_,_)), | |
775 | retractall(time_out_for_invariant(ID)), | |
776 | retractall(time_out_for_assertions(ID)), | |
777 | retractall(use_no_timeout(ID)), | |
778 | retractall(state_error(ID,_,_)), | |
779 | retractall(transition(ID,_,_,_)), | |
780 | % to do: check if operation_not_yet_covered(_) changes | |
781 | retract_hash(ID), | |
782 | retractall(id_to_marker(ID,_)). | |
783 | ||
784 | retract_hash(ID) :- retract(hash_to_id(Hash,ID)), retractall(hash_to_nauty_id(_TermHash,Hash)),fail. | |
785 | retract_hash(_). | |
786 | ||
787 | assert_max_reached_for_node(Id) :- %print_message(max_reached_for_node(Id)), | |
788 | (max_reached_for_node(Id) -> true ; assertz(max_reached_for_node(Id))). | |
789 | ||
790 | :- use_module(probsrc(debug),[debug_mode/1]). | |
791 | assert_time_out_for_node(Id,OpName,TypeOfTimeOut) :- | |
792 | (debug_mode(off),functor(TypeOfTimeOut,virtual_time_out,_) -> true % can easily happen when parameters are unbounded | |
793 | ; print_message(time_out_for_node(Id,OpName,TypeOfTimeOut))), | |
794 | (time_out_for_node(Id,OpName,_) -> true ; assertz(time_out_for_node(Id,OpName,TypeOfTimeOut))). | |
795 | assert_time_out_for_invariant(Id) :- print_message(time_out_for_invariant(Id)), | |
796 | (time_out_for_invariant(Id) -> true ; assertz(time_out_for_invariant(Id))). | |
797 | assert_time_out_for_assertions(Id) :- print_message(time_out_for_assertions(Id)), | |
798 | (time_out_for_assertions(Id) -> true ; assertz(time_out_for_assertions(Id))). | |
799 | ||
800 | max_reached_or_timeout_for_node(Id) :- | |
801 | (max_reached_for_node(Id) ; time_out_for_node(Id,_,_)). | |
802 | /* ---------------------- */ | |
803 | /* state space saving */ | |
804 | /* ---------------------- */ | |
805 | ||
806 | :- dynamic state_space_version_in_file/1. % | |
807 | state_space_version(1). | |
808 | ||
809 | check_state_space_version :- state_space_version(V), | |
810 | (state_space_version_in_file(F) -> true ; F=0), | |
811 | (V>F -> add_message(state_space,'Warning: saved state_space may be incompatible with current version: ',F:V) ; true). | |
812 | ||
813 | % save all infos of state space (transitions, evaluated invariants, ...) | |
814 | tcltk_save_state_space(File) :- | |
815 | print('% saving full state space to: '), print(File),nl, | |
816 | open(File,write,Stream,[encoding(utf8)]), | |
817 | print_state_space(Stream), | |
818 | close(Stream), | |
819 | print_message(done). | |
820 | ||
821 | ||
822 | :- use_module(tools_printing, [print_dynamic_fact/2,print_dynamic_pred/4]). | |
823 | print_state_space(Stream) :- | |
824 | state_space_version(V), | |
825 | print_dynamic_fact(Stream,state_space_version_in_file(V)), | |
826 | % TO DO: maybe also save some important preferences, and warn user and/or propose to adapt preferences ? | |
827 | print_dynamic_pred(Stream,state_space,history,1), | |
828 | print_dynamic_pred(Stream,state_space,forward_history,1), | |
829 | print_dynamic_pred(Stream,state_space,op_trace_ids,1), | |
830 | print_dynamic_pred(Stream,state_space,current_state_id,1), | |
831 | print_dynamic_pred(Stream,state_space,current_options,1), | |
832 | print_dynamic_pred(Stream,state_space,packed_visited_expression,2), | |
833 | print_dynamic_pred(Stream,state_space,not_invariant_checked,1), | |
834 | print_dynamic_pred(Stream,state_space,not_interesting,1), | |
835 | print_dynamic_pred(Stream,state_space,max_reached_for_node,1), | |
836 | print_dynamic_pred(Stream,state_space,time_out_for_node,3), | |
837 | print_dynamic_pred(Stream,state_space,use_no_timeout,1), | |
838 | print_dynamic_pred(Stream,state_space,transition,4), | |
839 | print_dynamic_pred(Stream,state_space,transition_info,2), | |
840 | print_dynamic_pred(Stream,state_space,operation_not_yet_covered,1), | |
841 | print_dynamic_pred(Stream,state_space,state_error,3), | |
842 | print_state_space_open_nodes(Stream), | |
843 | print_stored_values(Stream), | |
844 | get_counter(states,X), | |
845 | write_term(Stream,saved_gennum_count(X),[quoted(true)]),write(Stream,'.'),nl(Stream). | |
846 | ||
847 | saved_gennum_count(99999). | |
848 | ||
849 | /* ---------------------- */ | |
850 | /* state space loading */ | |
851 | /* ---------------------- */ | |
852 | ||
853 | tcltk_load_state(File) :- state_space_clean_all, | |
854 | print('Loading: '), print(File),nl, | |
855 | user_consult_without_redefine_warning(File), % this will read in bind_skeleton/2, ..., next_value_id/1 | |
856 | check_state_space_version, | |
857 | print('Generating open node info'),nl, | |
858 | transfer_open_node_info, | |
859 | print('Transfer state packing info'),nl, | |
860 | transfer_state_packing_info, | |
861 | print('Recomputing hash index'),nl, | |
862 | recompute_all_hash, | |
863 | (saved_gennum_count(X) -> reset_state_counter(X) ; true), | |
864 | reset_processed_nodes_counter, % TO DO: restore or save it | |
865 | reset_next_state_error_id_counter, % DITTO | |
866 | print('Done'),nl,!. | |
867 | tcltk_load_state(File) :- | |
868 | add_error(tcltk_load_state,'Could not load state from file: ',File), | |
869 | state_space_initialise. | |
870 | ||
871 | :- dynamic not_all_z_saved/1, not_all_transitions_added_saved/1. | |
872 | :- dynamic bind_skeleton/2, stored_value/2, stored_value_hash_to_id/2, next_value_id/1. | |
873 | ||
874 | % transfer facts read into state_space into other modules: | |
875 | transfer_open_node_info :- retract(not_all_z_saved(X)), %print(not_all_z(X)),nl, | |
876 | assert_not_all_z(X),fail. | |
877 | transfer_open_node_info :- retract(not_all_transitions_added_saved(X)), | |
878 | assert_not_all_transitions_added(X),fail. | |
879 | transfer_open_node_info. | |
880 | % now for transferring to state_packing module info generated by print_stored_values | |
881 | transfer_state_packing_info :- retract(bind_skeleton(X,Y)), %print(skel(X)),nl, | |
882 | assertz(state_packing:bind_skeleton(X,Y)),fail. | |
883 | transfer_state_packing_info :- retract(stored_value(X,Y)), | |
884 | assertz(state_packing:stored_value(X,Y)),fail. | |
885 | transfer_state_packing_info :- retract(stored_value_hash_to_id(X,Y)), | |
886 | assertz(state_packing:stored_value_hash_to_id(X,Y)),fail. | |
887 | transfer_state_packing_info :- retract(next_value_id(X)), | |
888 | state_packing:set_next_value_id(X),fail. | |
889 | transfer_state_packing_info. | |
890 | ||
891 | recompute_all_hash :- | |
892 | retractall(hash_to_id(_,_)),retractall(id_to_marker(_,_)), | |
893 | retractall(hash_to_nauty_id(_,_)), | |
894 | visited_expression(ID,StateTemplate), | |
895 | state_space_exploration_modes:compute_hash(StateTemplate,Hash,Marker), | |
896 | assertz(hash_to_id(Hash,ID)), | |
897 | assertz(id_to_marker(ID,Marker)), | |
898 | fail. | |
899 | recompute_all_hash. | |
900 | ||
901 | :- use_module(hashing,[my_term_hash/2]). | |
902 | % generates a hash for the entire state space not depending on the order in which states where added | |
903 | compute_full_state_space_hash(Hash) :- | |
904 | %listing(hash_to_id/2), listing(packed_visited_expression/2), | |
905 | findall(Hash,hash_to_id(Hash,_),ListOfHashCodes), | |
906 | sort(ListOfHashCodes,SortedList), | |
907 | my_term_hash(SortedList,Hash). | |
908 | % TO DO: also provide transition hashes | |
909 | ||
910 | :- use_module(tools_meta,[safe_on_exception/3]). | |
911 | user_consult_without_redefine_warning(File) :- | |
912 | get_set_optional_prolog_flag(redefine_warnings, Old, off), | |
913 | get_set_optional_prolog_flag(single_var_warnings, Old2, off), | |
914 | (safe_on_exception(Exc, | |
915 | %consult(File), % | |
916 | load_files([File], [load_type(source),compilation_mode(consult),encoding(utf8)]), | |
917 | (nl,print('Exception occurred:'),print(Exc),nl,fail)) | |
918 | -> OK=true ; OK=false), | |
919 | get_set_optional_prolog_flag(redefine_warnings, _, Old), | |
920 | get_set_optional_prolog_flag(single_var_warnings, _, Old2), | |
921 | OK=true. | |
922 | ||
923 | ||
924 | ||
925 | execute_id_trace_from_current(ID,OpIDL,StateIDList) :- | |
926 | current_state_id(CurID), | |
927 | reverse([CurID|StateIDList],Rev), | |
928 | Rev = [Dest|TRev], (Dest==ID -> true ; print(not_eq(Dest,ID)),nl), | |
929 | retract(history(H)), retractall(forward_history(_)), | |
930 | append(TRev,H,NewH), | |
931 | assertz(history(NewH)), | |
932 | retract(op_trace_ids(OldTrace)), | |
933 | reverse(OpIDL,NewTrace), | |
934 | append(NewTrace,OldTrace,Trace), | |
935 | assertz(op_trace_ids(Trace)), | |
936 | retractall(current_state_id(_)), | |
937 | assertz(current_state_id(ID)). | |
938 | %execute_trace_to_node(OpL,StateIDList). /* <----- BOTTLENECK FOR LONG SEQUENCES */ | |
939 | %generate_trace([],Acc,Acc). | |
940 | %generate_trace([OpTerm|T],Acc,Res) :- | |
941 | % translate:translate_event(OpTerm,OpString), | |
942 | % generate_trace(T,[action(OpString,OpTerm)|Acc],Res). | |
943 | ||
944 | try_set_trace_by_transition_ids(TransIds) :- | |
945 | (set_trace_by_transition_ids(TransIds) -> true | |
946 | ; add_internal_error('Call failed:',set_trace_by_transition_ids(TransIds))). | |
947 | ||
948 | set_trace_by_transition_ids(TransitionIds) :- | |
949 | extract_history_from_transition_ids(TransitionIds,root,[],[],Last,History,OpTrace), | |
950 | %visited_expression(Last,LastState,LastCond), | |
951 | retractall(history(_)), retractall(forward_history(_)), | |
952 | retractall(current_state_id(_)), | |
953 | retractall(op_trace_ids(_)), | |
954 | assertz(history(History)), assertz(op_trace_ids(OpTrace)), | |
955 | assertz(current_state_id(Last)). | |
956 | ||
957 | extract_history_from_transition_ids([],CurrentState,History,Trace,CurrentState,History,Trace). | |
958 | extract_history_from_transition_ids([TransId|Rest],CurrentState,AccHist,AccTrace,Last,History,Trace) :- | |
959 | transition(CurrentState,_,TransId,DestState),!, | |
960 | extract_history_from_transition_ids(Rest,DestState,[CurrentState|AccHist], | |
961 | [TransId|AccTrace],Last,History,Trace). | |
962 | extract_history_from_transition_ids([TransId|_],CurrentState,_,_,_,_,_Trace) :- | |
963 | add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail. | |
964 | ||
965 | % extend trace from current state | |
966 | extend_trace_by_transition_ids(TransitionIds) :- | |
967 | current_state_id(CurID), | |
968 | history(OldH), op_trace_ids(OldOT), | |
969 | extract_history_from_transition_ids(TransitionIds,CurID,OldH,OldOT,Last,History,OpTrace), | |
970 | retractall(history(_)), retractall(forward_history(_)), | |
971 | retractall(current_state_id(_)), | |
972 | retractall(op_trace_ids(_)), | |
973 | assertz(history(History)), | |
974 | assertz(op_trace_ids(OpTrace)), | |
975 | assertz(current_state_id(Last)). | |
976 | ||
977 | /* --------------------------------- */ | |
978 | :- dynamic max_nr_of_new_nodes/1. | |
979 | ||
980 | % negative number or non-number signifies no limit | |
981 | set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :- | |
982 | retractall(max_nr_of_new_nodes(_)), | |
983 | (number(MaxNrOfNewNodes), MaxNrOfNewNodes>=0 | |
984 | -> assertz(max_nr_of_new_nodes(MaxNrOfNewNodes)) | |
985 | ; true). % no need to store limit; we will explore as much as needed | |
986 | ||
987 | get_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :- | |
988 | (max_nr_of_new_nodes(Max) -> MaxNrOfNewNodes=Max; MaxNrOfNewNodes = 0). | |
989 | ||
990 | % used e.g., in refinement or ltl checker | |
991 | impl_trans_term(From,ActionAsTerm,To) :- | |
992 | compute_transitions_if_necessary_saved(From), | |
993 | transition(From,ActionAsTerm,_TID,To). | |
994 | ||
995 | % a variation also giving the transition id: | |
996 | impl_trans_id(From,ActionAsTerm,TransitionID,To) :- | |
997 | compute_transitions_if_necessary_saved(From), | |
998 | transition(From,ActionAsTerm,TransitionID,To). | |
999 | ||
1000 | impl_trans_term_all(From,Ops) :- | |
1001 | compute_transitions_if_necessary_saved(From), | |
1002 | findall(op(Id,ActionAsTerm,To), | |
1003 | transition(From,ActionAsTerm,Id,To), | |
1004 | Ops). | |
1005 | ||
1006 | compute_transitions_if_necessary_saved(From) :- | |
1007 | catch( | |
1008 | compute_transitions_if_necessary(From), | |
1009 | error(forced_interrupt_error('User has interrupted the current execution'),_), | |
1010 | user_interrupts:process_interrupted_error_message). | |
1011 | ||
1012 | :- use_module(tcltk_interface,[compute_all_transitions_if_necessary/2]). | |
1013 | compute_transitions_if_necessary(From) :- | |
1014 | not_all_transitions_added(From),!, | |
1015 | decrease_max_nr_of_new_nodes(From), | |
1016 | compute_all_transitions_if_necessary(From,false). | |
1017 | compute_transitions_if_necessary(_From). | |
1018 | ||
1019 | decrease_max_nr_of_new_nodes(ID) :- | |
1020 | retract(max_nr_of_new_nodes(Max)),!, | |
1021 | ( Max>0 -> | |
1022 | NewMax is Max-1, | |
1023 | assertz(max_nr_of_new_nodes(NewMax)) | |
1024 | ; Max=0 -> NM is -1, | |
1025 | assertz(max_nr_of_new_nodes(NM)), | |
1026 | add_warning(state_space,'Maximum number of new nodes reached for CTL/LTL/refinement check, node id = ',ID), | |
1027 | fail | |
1028 | ; % negative number: re-assert and fail | |
1029 | assertz(max_nr_of_new_nodes(Max)), | |
1030 | fail). | |
1031 | decrease_max_nr_of_new_nodes(_). % no limit stored; just proceed | |
1032 | ||
1033 | % will be called from TCL/TK side | |
1034 | max_nr_of_new_nodes_limit_not_reached :- | |
1035 | max_nr_of_new_nodes(N),N>0. | |
1036 | ||
1037 | :- use_module(specfile,[b_or_z_mode/0, csp_mode/0, csp_with_bz_mode/0]). | |
1038 | retract_open_node(NodeID) :- retract_open_node_and_update_processed_nodes(NodeID), | |
1039 | (b_or_z_mode -> assertz(not_invariant_checked(NodeID)) ; true). | |
1040 | ||
1041 | reset_processed_nodes_counter :- reset_counter(processed_nodes). | |
1042 | %reset_processed_nodes_counter(Nr) :- set_counter(processed_nodes,Nr). | |
1043 | ||
1044 | retract_open_node_and_update_processed_nodes(NodeID) :- | |
1045 | retract_open_node_direct(NodeID), | |
1046 | inc_processed. | |
1047 | ||
1048 | inc_processed :- | |
1049 | inc_counter(processed_nodes). | |
1050 | ||
1051 | pop_id_from_front(ID) :- pop_id_from_front_direct(ID), inc_processed. | |
1052 | pop_id_from_end(ID) :- pop_id_from_end_direct(ID), inc_processed. | |
1053 | pop_id_oldest(ID) :- pop_id_oldest_direct(ID), inc_processed. | |
1054 | ||
1055 | ||
1056 | ||
1057 | /* --------------------------------- */ | |
1058 | ||
1059 | % find initialised states; very similar to is_initial_state_id/1 | |
1060 | % but is used by ltl/ctl/sap | |
1061 | % TO DO: merge these two variations of the same concept | |
1062 | ||
1063 | :- use_module(specfile,[animation_mode/1]). | |
1064 | ||
1065 | find_initialised_states(Init) :- | |
1066 | animation_mode(Mode), | |
1067 | ( init_states_mode_cst_init(Mode) -> | |
1068 | findall(I,find_init1(root,I,_),Init) | |
1069 | ; init_states_mode_one_step(Mode) -> | |
1070 | next_states_from_root(Init) | |
1071 | ; | |
1072 | fail). | |
1073 | ||
1074 | % find trace to some initialised state | |
1075 | find_trace_to_initial_state(Target,Trace) :- animation_mode(Mode), | |
1076 | find_aux(Mode,Target,Trace). | |
1077 | find_aux(Mode,Target,[root,Target]) :- | |
1078 | init_states_mode_one_step(Mode). | |
1079 | find_aux(Mode,Target,[root|Trace]) :- | |
1080 | init_states_mode_cst_init(Mode), | |
1081 | find_init1(root,Target,Trace). | |
1082 | ||
1083 | ||
1084 | init_states_mode_cst_init(b). | |
1085 | init_states_mode_cst_init(z). | |
1086 | init_states_mode_cst_init(csp_and_b). | |
1087 | ||
1088 | init_states_mode_one_step(csp). | |
1089 | init_states_mode_one_step(cspm). | |
1090 | init_states_mode_one_step(xtl). | |
1091 | %init_states_mode_one_step(promela). | |
1092 | ||
1093 | next_states_from_root(States) :- | |
1094 | impl_trans_term_all(root,Ops), | |
1095 | findall(S, member(op(_Id,_,S),Ops), States). | |
1096 | ||
1097 | find_init1(Start,Init,Trace) :- Start==Init,!,Trace=[]. % usually called with Start=Init=root | |
1098 | find_init1(Start,Init,[State|Rest]) :- | |
1099 | impl_trans_term(Start,O,State), | |
1100 | find_init2(O,State,Init,Rest). | |
1101 | find_init2(O,Init,Init,[]) :- | |
1102 | has_functor_and_maybe_tau(O,'$initialise_machine'). | |
1103 | find_init2(O,State,Init,Path) :- | |
1104 | has_functor_and_maybe_tau(O,'$setup_constants'), | |
1105 | find_init1(State,Init,Path). | |
1106 | find_init2(start_cspm_MAIN,State,Init,Path) :- | |
1107 | find_init1(State,Init,Path). | |
1108 | find_init2(start_cspm(_Proc),State,Init,Path) :- | |
1109 | find_init1(State,Init,Path). | |
1110 | ||
1111 | % has_functor_and_maybe_tau(Term,Functor) | |
1112 | % checks if Term has the form "Functor(...)" or "tau(Functor(...))" | |
1113 | % this is used for CSP||B specification where the initialisation is wrapped with | |
1114 | % in a tau operator | |
1115 | has_functor_and_maybe_tau(tau(Term),Functor) :- | |
1116 | has_functor_and_maybe_tau(Term,Functor),!. | |
1117 | has_functor_and_maybe_tau(Term,Functor) :- | |
1118 | functor(Term,Functor,_). | |
1119 | ||
1120 | ||
1121 | /* --------------------------------- */ | |
1122 | ||
1123 | % | |
1124 | % Code to compute equivalence classes | |
1125 | % using the standard DFA minimization algorithm | |
1126 | ||
1127 | :- dynamic equivalent/2. | |
1128 | % state_space:compute_equivalence_classes | |
1129 | :- public compute_equivalence_classes/0. | |
1130 | ||
1131 | compute_equivalence_classes :- init_equi, | |
1132 | split_equivalence_classes,nl, | |
1133 | print_equi. | |
1134 | ||
1135 | print_equi :- state_space:equivalent(A,B), visited_expression(A,State), | |
1136 | visited_expression(B,StateB), | |
1137 | nl, | |
1138 | print(A), print(' : '), print(State),nl, | |
1139 | print(B), print(' : '), print(StateB),nl,fail. | |
1140 | print_equi. | |
1141 | ||
1142 | init_equi :- retractall(equivalent(_,_)), | |
1143 | packed_visited_expression(ID,_State), | |
1144 | \+ not_all_transitions_added(ID), | |
1145 | findall(Action,transition(ID,Action,_,_),List), | |
1146 | packed_visited_expression(ID2,_S2), ID2 @> ID, | |
1147 | \+ not_all_transitions_added(ID2), | |
1148 | findall(Action,transition(ID2,Action,_,_),List), | |
1149 | assertz(equivalent(ID,ID2)), % they have the same signature | |
1150 | %print(equivalent(ID,ID2)),nl, | |
1151 | fail. | |
1152 | init_equi :- print(finished_initialising),nl. | |
1153 | ||
1154 | split_equivalence_classes :- retractall(echange), | |
1155 | equivalent(ID1,ID2), | |
1156 | transition(ID1,A,_,Dest1), | |
1157 | transition(ID2,A,_,Dest2), | |
1158 | \+ check_equi(Dest1,Dest2), | |
1159 | retract(equivalent(ID1,ID2)), % splitting class | |
1160 | % print(diff(ID1,ID2, A, Dest1, Dest2)),nl, | |
1161 | assert_echange, | |
1162 | fail. | |
1163 | split_equivalence_classes :- echange -> split_equivalence_classes ; true. | |
1164 | ||
1165 | :- dynamic echange/0. | |
1166 | assert_echange :- echange -> true ; assertz(echange),print('.'),flush_output. | |
1167 | ||
1168 | check_equi(A,B) :- A=B -> true ; A @<B -> equivalent(A,B) ; equivalent(B,A). | |
1169 | ||
1170 | /* | |
1171 | % benchmark how much time it takes to copy the state space state_space:bench_state_space. | |
1172 | bench_state_space :- | |
1173 | statistics(walltime,_), | |
1174 | (state_space:packed_visited_expression(ID,S), assertz(pve(ID,S)),fail ; true), | |
1175 | statistics(walltime,[_,Delta]), format('Time to copy packed_visited_expression: ~w ms~n',[Delta]), | |
1176 | (state_space:transition(A,B,C,D), assertz(tr(A,B,C,D)),fail ; true), | |
1177 | statistics(walltime,[_,Delta2]), format('Time to copy transition: ~w ms~n',[Delta2]), | |
1178 | (state_packing:stored_value(A,B), assertz(sv(A,B)),fail ; true), | |
1179 | (state_packing:stored_value_hash_to_id(A,B), assertz(svhi(A,B)),fail ; true), | |
1180 | statistics(walltime,[_,Delta3]), format('Time to copy stored_value: ~w ms~n',[Delta3]). | |
1181 | */ | |
1182 | ||
1183 | :- public portray_state_space/0. | |
1184 | portray_state_space :- packed_visited_expression(ID,S), functor(S,F,N), | |
1185 | format('State ~w : ~w/~w~n',[ID,F,N]), fail. | |
1186 | portray_state_space :- transition(ID,Action,TransID,DestID), | |
1187 | format(' ~w: ~w -- ~w --> ~w~n',[TransID,ID,Action,DestID]),fail. | |
1188 | portray_state_space. | |
1189 | ||
1190 | bench_state_space :- statistics(walltime,[W1,_]), | |
1191 | (packed_visited_expression(_,_), fail ; true), | |
1192 | statistics(walltime,[W2,_]), T1 is W2-W1, | |
1193 | format('Time to inspect all states: ~w ms walltime~n',[T1]), | |
1194 | (visited_expression(_,_), fail ; true), | |
1195 | statistics(walltime,[W3,_]), T2 is W3-W2, | |
1196 | format('Time to inspect and unpack all states: ~w ms walltime~n',[T2]), | |
1197 | (transition(_,_,_,_), fail ; true), | |
1198 | statistics(walltime,[W4,_]), T3 is W4-W3, | |
1199 | format('Time to inspect all transitions: ~w ms walltime~n',[T3]), | |
1200 | (visited_expression(_,E), my_term_hash(E,_), fail ; true), | |
1201 | statistics(walltime,[W5,_]), T4 is W5-W4, | |
1202 | format('Time to inspect, unpack and hash all states: ~w ms walltime~n',[T4]). | |
1203 | ||
1204 | % ---------------------------- | |
1205 | % COUNTER EXAMPLE MANAGEMENT | |
1206 | ||
1207 | % store counter example nodes and transition ids; used by LTL model checking for example | |
1208 | ||
1209 | ||
1210 | :- dynamic counterexample_node/1. | |
1211 | :- dynamic counterexample_op/1. | |
1212 | ||
1213 | add_counterexample_node(NodeID) :- assertz(counterexample_node(NodeID)). | |
1214 | add_counterexample_op(TransID) :- | |
1215 | (counterexample_op(TransID) -> true ; assertz(counterexample_op(TransID))). | |
1216 | ||
1217 | ||
1218 | reset_counterexample :- | |
1219 | retractall(counterexample_node(_)), | |
1220 | retractall(counterexample_op(_)). | |
1221 | ||
1222 | :- register_event_listener(play_counterexample,reset_counterexample, | |
1223 | 'Reset marked nodes from previous counterexamples.'). | |
1224 | ||
1225 | set_counterexample_by_transition_ids(TransIds) :- | |
1226 | set_trace_by_transition_ids(TransIds), | |
1227 | maplist(add_counterexample_op,TransIds), | |
1228 | extract_history_from_transition_ids(TransIds,root,[],[],_Last,History,_OpTrace), | |
1229 | maplist(add_counterexample_node,History). |