1 | | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(state_space, |
6 | | [get_state_space_stats/3, gen_new_state_id/1, |
7 | | history/1, forward_history/1, |
8 | | get_action_trace/1, % old trace/1 |
9 | | get_action_term_trace/1, |
10 | | op_trace_ids/1, add_to_op_trace_ids/1, remove_from_op_trace_ids/1, reset_op_trace_ids/0, |
11 | | get_state_id_trace/1, |
12 | | current_state_id/1, current_expression/2, |
13 | | current_options/1, set_current_options/1, |
14 | | |
15 | | add_id_at_front/1, add_id_at_end/1, |
16 | | add_id_random/1, /* from state_space_open_nodes_c */ |
17 | | add_id_with_weight/2, add_id_to_process/3, |
18 | | pop_id_from_front/1, pop_id_from_end/1, pop_id_oldest/1, |
19 | | retract_open_node/1, open_ids_empty/0, |
20 | | |
21 | | visited_expression/3, visited_expression/2, visited_expression_id/1, |
22 | | find_hashed_packed_visited_expression/3, |
23 | | retract_visited_expression/2, |
24 | | not_all_transitions_added/1, |
25 | | not_invariant_checked/1, set_invariant_checked/1, |
26 | | invariant_not_yet_checked/1, |
27 | | not_interesting/1,max_reached_for_node/1, |
28 | | max_reached_or_timeout_for_node/1, |
29 | | use_no_timeout/1, time_out_for_node/1, time_out_for_node/3, |
30 | | hash_to_id/2,id_to_marker/2, hash_to_nauty_id/2, |
31 | | invariant_violated/1, time_out_for_invariant/1, time_out_for_assertions/1, |
32 | | set_invariant_violated/1, |
33 | | |
34 | | state_error_exists/0, state_error/3, store_state_error/3, |
35 | | set_context_state/1, clear_context_state/0, get_current_context_state/1, |
36 | | store_error_for_context_state/2, |
37 | | store_abort_error_for_context_state_if_possible/4, |
38 | | |
39 | | transition/3,transition/4, any_transition/3, |
40 | | store_transition/4, |
41 | | deadlocked_state/1, % no outgoing edge |
42 | | is_initial_state_id/1, is_concrete_constants_state_id/1, |
43 | | multiple_concrete_constants_exist/0, |
44 | | out_degree/2, |
45 | | operation_not_yet_covered/1, operation_name_not_yet_covered/1, |
46 | | |
47 | | transition_info/2, store_transition_infos/2, |
48 | | compute_transitions_if_necessary/1, |
49 | | |
50 | | state_space_initialise/0, state_space_initialise_with_stats/0, |
51 | | state_space_reset/0, |
52 | | state_space_add/2, state_space_packed_add/2, |
53 | | delete_node/1, |
54 | | |
55 | | current_state_corresponds_to_initialised_b_machine/0, |
56 | | current_state_corresponds_to_fully_setup_b_machine/0, |
57 | | current_state_corresponds_to_setup_constants_b_machine/0, |
58 | | |
59 | | specialized_inv/2, reuse_operation/4, |
60 | | assert_max_reached_for_node/1, assert_time_out_for_node/3, |
61 | | assert_time_out_for_invariant/1, assert_time_out_for_assertions/1, |
62 | | |
63 | | set_max_nr_of_new_impl_trans_nodes/1, |
64 | | get_max_nr_of_new_impl_trans_nodes/1, |
65 | | impl_trans_term/3, impl_trans_term_all/2, |
66 | | compute_transitions_if_necessary_saved/1, |
67 | | max_nr_of_new_nodes_limit_not_reached/0, |
68 | | |
69 | | tcltk_save_state/1, tcltk_load_state/1, |
70 | | compute_full_state_space_hash/1, |
71 | | |
72 | | execute_id_trace_from_current/3, |
73 | | set_trace_by_transition_ids/1, |
74 | | extract_term_trace_from_transition_ids/2]). |
75 | | |
76 | | :- use_module(library(lists)). |
77 | | |
78 | | :- use_module(self_check). |
79 | | :- use_module(error_manager). |
80 | | :- use_module(gensym). |
81 | | :- use_module(preferences). |
82 | | :- use_module(tools). |
83 | | %:- use_module(state_space_exploration_modes,[compute_hash/3]). |
84 | | |
85 | | :- use_module(extension('counter/counter')). |
86 | | |
87 | | :- use_module(module_information). |
88 | | :- module_info(group,animator). |
89 | | :- module_info(description,'This module keeps track of the visited states by the animator/model checker.'). |
90 | | |
91 | | % ---------------------------------- |
92 | | |
93 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
94 | | :- if(environ(prob_myheap,false)). |
95 | | :- use_module(state_space_open_nodes). %% comment in to use only Prolog datastructures |
96 | | :- else. |
97 | | :- use_module(state_space_open_nodes_c). %% comment in to use C++ multimap queue; can make use of HEURISTIC_FUNCTION |
98 | | :- endif. |
99 | | |
100 | | % ---------------------------------- |
101 | | |
102 | | get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes) :- |
103 | | get_counter(states,N), NrNodes is N+1, |
104 | | get_counter(transitions,NrTransitions), |
105 | | get_counter(processed_nodes,ProcessedNodes). |
106 | | |
107 | | gen_new_state_id(Nr) :- |
108 | | inc_counter(states,N1), Nr is N1-1. % only one C call |
109 | | %get_counter(states,Nr), inc_counter(states). |
110 | | reset_state_counter :- reset_counter(states). |
111 | | reset_state_counter(Nr) :- set_counter(states,Nr). |
112 | | |
113 | | get_state_id_trace(StateIds) :- |
114 | | history(History), |
115 | | current_state_id(CurID), |
116 | | reverse([CurID|History],StateIds). |
117 | | |
118 | | :- dynamic history/1. |
119 | | history([]). |
120 | | |
121 | | |
122 | | :- dynamic forward_history/1. |
123 | | |
124 | | :- dynamic current_state_id/1. |
125 | | current_state_id(root). |
126 | | /* INITIAL STATE, third arg: clp(fd) constraints as generated |
127 | | by fd_copy_term */ |
128 | | |
129 | | current_expression(ID,State) :- current_state_id(ID), |
130 | | visited_expression(ID,State). |
131 | | |
132 | | :- use_module(specfile,[state_corresponds_to_initialised_b_machine/1, |
133 | | state_corresponds_to_fully_setup_b_machine/1, |
134 | | state_corresponds_to_set_up_constants/1]). |
135 | | current_state_corresponds_to_initialised_b_machine:- |
136 | | current_expression(_,State), |
137 | | state_corresponds_to_initialised_b_machine(State). |
138 | | |
139 | | current_state_corresponds_to_fully_setup_b_machine :- |
140 | | current_expression(_,State), |
141 | | state_corresponds_to_fully_setup_b_machine(State). |
142 | | |
143 | | current_state_corresponds_to_setup_constants_b_machine :- |
144 | | current_expression(_,State), |
145 | | state_corresponds_to_set_up_constants(State). |
146 | | |
147 | | |
148 | | :- dynamic current_options/1. |
149 | | current_options([]). |
150 | | |
151 | | set_current_options(Options) :- |
152 | | retractall( current_options(_) ), |
153 | | assert( current_options(Options) ). |
154 | | |
155 | | :- dynamic packed_visited_expression/2. |
156 | | %packed_visited_expression(v_0,true). |
157 | | |
158 | | :- use_module(state_packing). |
159 | | |
160 | | retract_visited_expression(ID,State) :- retract(packed_visited_expression(ID,PState)), |
161 | | unpack_state(PState,State). |
162 | | |
163 | | retractall_visited_expression(ID) :- retractall(packed_visited_expression(ID,_)). |
164 | | |
165 | | state_space_packed_add(Id,PackedTerm) :- assert(packed_visited_expression(Id,PackedTerm)). |
166 | | |
167 | | state_space_add(Id,Term) :- |
168 | | (pack_state(Term,PackedTerm) -> assert(packed_visited_expression(Id,PackedTerm)) |
169 | | ; add_internal_error('State packing failed: ',pack_state(Term,_)), |
170 | | assert(packed_visited_expression(Id,Term))). |
171 | | |
172 | | % deprecated: |
173 | | visited_expression(ID,State,true) :- visited_expression(ID,State). |
174 | | % not call(CurBody); for the moment we always have true as last argument |
175 | | |
176 | ? | visited_expression(A,B) :- packed_visited_expression(A,PB), |
177 | | (unpack_state(PB,R) -> B=R ; add_internal_error('Unpacking state failed: ',unpack_state(PB,R)),R=A). |
178 | | |
179 | | visited_expression_id(A) :- packed_visited_expression(A,_). % avoid unpacking state |
180 | | |
181 | | |
182 | | |
183 | | % given a hash and a packed state: find ID (fail if does not exist) |
184 | | find_hashed_packed_visited_expression(Hash,PackedState,ID) :- |
185 | | hash_to_id(Hash,ID), |
186 | | (packed_visited_expression(ID,PackedState) |
187 | | -> true /* warning: may instantiate State if not ground */ |
188 | | ; print(hash_collision(Hash,ID)),nl,fail |
189 | | ). |
190 | | |
191 | | |
192 | | :- dynamic not_invariant_checked/1. |
193 | | set_invariant_checked(ID) :- %print(inv_checked(ID)),nl, |
194 | | retract(not_invariant_checked(ID)). |
195 | | |
196 | | invariant_not_yet_checked(ID) :- |
197 | | not_all_transitions_added(ID) ; /* assumption: if not all transitions added then we haven't checked invariant yet */ |
198 | | not_invariant_checked(ID). |
199 | | |
200 | | :- dynamic not_interesting/1. |
201 | | %not_interesting(v_0). |
202 | | |
203 | | :- dynamic max_reached_for_node/1. |
204 | | /* true if not all outgoing transistions were computed due to the limit |
205 | | on the number of operations/initialisations computed */ |
206 | | :- dynamic time_out_for_node/3, use_no_timeout/1, time_out_for_invariant/1, time_out_for_assertions/1. |
207 | | |
208 | | time_out_for_node(ID) :- (var(ID) -> packed_visited_expression(ID,_) ; true), |
209 | | (time_out_for_node(ID,_,_) -> true ; fail). |
210 | | |
211 | | :- dynamic transition/4. |
212 | | %transition(v_0,a,1,v_1). |
213 | | |
214 | | store_transition(Org,Action,Dest,Id) :- |
215 | | %get_counter(transitions,Id), inc_counter(transitions), |
216 | | inc_counter(transitions,Id1), Id is Id1-1, % only one C call |
217 | | assert(transition(Org,Action,Id,Dest)). |
218 | | |
219 | | deadlocked_state(Origin) :- \+ any_transition(Origin,_,_). |
220 | | |
221 | | is_concrete_constants_state_id(ID) :- |
222 | | transition(root,_,ID), |
223 | | packed_visited_expression(ID,concrete_constants(_)). |
224 | | |
225 | | % check if we have multiple constant setups |
226 | | multiple_concrete_constants_exist :- |
227 | | is_concrete_constants_state_id(ID), |
228 | | is_concrete_constants_state_id(ID2), ID2 \= ID,!. |
229 | | |
230 | | |
231 | | is_initial_state_id(InitialStateID) :- |
232 | | transition(root,_,State), |
233 | | packed_visited_expression(State,P), |
234 | | (P = concrete_constants(_) |
235 | | -> state_space:transition(State,_,InitialStateID) |
236 | | ; InitialStateID=State). |
237 | | |
238 | | any_transition(Origin,TransID,Destination) :- transition(Origin,_,TransID,Destination). |
239 | | |
240 | | transition(Origin,Action,Destination) :- transition(Origin,Action,_TransID,Destination). |
241 | | |
242 | | :- dynamic transition_info/2. |
243 | | store_transition_infos([],_TransId). |
244 | | store_transition_infos([Info|Irest],TransId) :- |
245 | | store_transition_info(Info,TransId), |
246 | | store_transition_infos(Irest,TransId). |
247 | | store_transition_info(Info,TransId) :- %print(info(Info,TransId)),nl, |
248 | | (keep_transition_info(Info) |
249 | | -> assert(transition_info(TransId,Info)) |
250 | | ; true). |
251 | | |
252 | | % Do not store path info by default |
253 | | keep_transition_info(path(_)) :- !,fail. |
254 | | keep_transition_info(eventtrace(_)) :- !,preference(eventtrace,true). |
255 | | keep_transition_info(event(_)) :- !,preference(store_event_transinfo,true). |
256 | | keep_transition_info(_). % store everything else |
257 | | |
258 | | reset_transition_store :- |
259 | | retractall(transition(_,_,_,_)), |
260 | | retractall(transition_info(_,_)), |
261 | | reset_counter(transitions). |
262 | | |
263 | | /* |
264 | | Version with packing of transitions: |
265 | | store_transition(Org,Action,Dest,Id) :- |
266 | | retract(transition_counter(Id)), |
267 | | NewId is Id+1, |
268 | | assert(transition_counter(NewId)), |
269 | | Action =.. [ActionName|Parameters], |
270 | | pack_values(Parameters,PackedParameters), |
271 | | assert(packed_transition(Org,ActionName,PackedParameters,Id,Dest)). |
272 | | |
273 | | transition(Origin,Action,TransID,Destination) :- nonvar(Action),!, |
274 | | Action =.. [ActionName|Parameters], |
275 | | packed_transition(Origin,ActionName,PackedParameters,TransID,Destination), |
276 | | unpack_values(PackedParameters,Parameters). |
277 | | transition(Origin,Action,TransID,Destination) :- |
278 | | packed_transition(Origin,ActionName,PackedParameters,TransID,Destination), |
279 | | unpack_values(PackedParameters,Parameters), |
280 | | Action =.. [ActionName|Parameters]. |
281 | | any_transition(Origin,TransID,Destination) :- packed_transition(Origin,_,_,TransID,Destination). |
282 | | */ |
283 | | |
284 | | % compute out-degree of a node |
285 | | out_degree(ID,OutDegree) :- findall(0, transition(ID,_,_,_), L), length(L,OutDegree). |
286 | | |
287 | | operation_name_not_yet_covered(OpName) :- operation_not_yet_covered(OpName). |
288 | | |
289 | | :- dynamic operation_not_yet_covered/1. |
290 | | %operation_not_yet_covered(b). |
291 | | |
292 | | state_error_exists :- state_error(_,_,_),!. |
293 | | :- dynamic state_error/3, context_state/2. |
294 | | |
295 | | %state_error([],invariant_violated). |
296 | | |
297 | | reset_next_state_error_id_counter :- reset_counter(next_state_error_id). |
298 | | :- use_module(tools_printing, [print_error/1]). |
299 | | :- use_module(error_manager,[print_error_span/1]). |
300 | | store_state_error(State,Error,Id) :- state_error(State,Id,Error),!. % do not store identical error twice |
301 | | store_state_error(State,Error,Id) :- |
302 | | %retract( next_state_error_id(Id) ), |
303 | | inc_counter(next_state_error_id,Id), |
304 | | assert( state_error(State,Id,Error) ). |
305 | | store_error_for_context_state(Error,Id) :- |
306 | | ( retract(context_state(State,Errs)) -> |
307 | | (Errs<25 -> store_state_error(State,Error,Id), E1 is Errs+1,assert(context_state(State,E1)) |
308 | | ; store_state_error(State,max_state_errors_reached(25),Id),assert(context_state(State,25)) |
309 | | ) |
310 | | ; otherwise -> |
311 | | add_internal_error('No known context when calling store_error_for_context_state: ',store_error_for_context_state(Error,Id)), |
312 | | fail). |
313 | | store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span) :- |
314 | | %print(store(Msg,Term,Span)),nl, |
315 | | ( context_state(State,_Errs) -> |
316 | | error_manager:get_error_context(Context), |
317 | | (abort_error_for_same_location_exists(State,Id1,ErrType,Msg,Span), |
318 | | abort_error_for_same_location_exists(State,Id2,ErrType,Msg,Span), |
319 | | Id2>Id1 |
320 | | -> /* two errors of same type, for same state and same source location exists */ |
321 | | /* TO DO: maybe merge state errors */ |
322 | | simplify_span(Span,Span2), |
323 | | store_state_error(State,abort_error(ErrType,'Further identical errors occurred (not stored !)',Term,span_context(Span2,Context)),_) |
324 | | ; |
325 | | print_error('An abort error occurred !'), print_error(ErrType), |
326 | | print_error(Msg), |
327 | | print_error_term(Term), |
328 | | print_error(context_state_id(State)), |
329 | | print_error_span(Span), |
330 | | store_state_error(State,abort_error(ErrType,Msg,Term,span_context(Span,Context)),_) |
331 | | ), |
332 | | (add_new_event_in_error_scope(abort_error(ErrType)) -> true ; true), |
333 | | assert_real_error_occurred |
334 | | ; otherwise -> |
335 | | add_error(ErrType,Msg,Term,Span)). |
336 | | |
337 | | :- use_module(translate, [translate_error_term/2]). |
338 | | print_error_term(Term) :- translate_error_term(Term,S), print_error(S). |
339 | | |
340 | | abort_error_for_same_location_exists(State,Id,ErrType,Msg,Span) :- |
341 | | state_error(State,Id,abort_error(ErrType,Msg,_Term2,span_context(Span2,_Ctxt2))), |
342 | | same_span_location(Span2,Span). |
343 | | % should be moved to error_manager ? |
344 | | same_span_location(span_predicate(Pred,_,_),span_predicate(Pred,_,_)) :- !. |
345 | | same_span_location(X,X). |
346 | | |
347 | | % remove state information; quite often the same WD error occurs with slightly different stores |
348 | | simplify_span(span_predicate(Pred,_,_),R) :- !, R=Pred. |
349 | | simplify_span(X,X). |
350 | | |
351 | | clear_context_state :- |
352 | | retractall(context_state(_,_)). |
353 | | set_context_state(State) :- |
354 | | %print(setting_ctxt_state(State,Event)),nl, |
355 | | retractall(context_state(_,_)), assert(context_state(State,0)). |
356 | | get_current_context_state(ID) :- context_state(ID,_). |
357 | | |
358 | | retractall_invariant_violated(State) :- |
359 | | retractall(state_error(State,_,invariant_violated)). |
360 | | invariant_violated(State) :- |
361 | ? | state_error(State,_,invariant_violated). |
362 | | set_invariant_violated(State) :- |
363 | | ( invariant_violated(State) -> true |
364 | | ; time_out_for_invariant(ID) -> print('Timeout for node: '), print(ID),nl, |
365 | | print('Not setting invariant violation status'),nl |
366 | | ; store_state_error(State,invariant_violated,_) |
367 | | ). |
368 | | |
369 | | %:- set_invariant_violated([]). % why is this ?? |
370 | | |
371 | | |
372 | | :- dynamic hash_to_id/2. |
373 | | :- dynamic id_to_marker/2. |
374 | | |
375 | | :- dynamic hash_to_nauty_id/2. % used in nauty mode to map nauty id's to hash values |
376 | | |
377 | | :- dynamic specialized_inv/2. /* stores whether for a node a specialized invariant |
378 | | version could be computed */ |
379 | | |
380 | | :- dynamic reuse_operation/4. /* when for a state and given operation name we can reuse the operation computed for another state */ |
381 | | |
382 | | :- use_module(hashing). |
383 | | state_space_startup :- % call once at startup to ensure all counters exist |
384 | | counter_init, |
385 | | new_counter(states), new_counter(processed_nodes), new_counter(transitions), |
386 | | new_counter(next_state_error_id), |
387 | | reset_open_ids. % also calls myheap init |
388 | | state_space_initialise :- counter_init, reset_gennum, reset_gensym, |
389 | | new_counter(states), new_counter(processed_nodes), new_counter(transitions), |
390 | | new_counter(next_state_error_id), |
391 | | reset_state_counter, reset_processed_nodes_counter, reset_next_state_error_id_counter, |
392 | | retractall_visited_expression(_), |
393 | | reset_open_ids, reset_stored_values, |
394 | | retractall(not_invariant_checked(_)), |
395 | | retractall(not_interesting(_)), |
396 | | retractall(max_reached_for_node(_)), |
397 | | retractall(time_out_for_node(_,_,_)), |
398 | | retractall(time_out_for_invariant(_)), |
399 | | retractall(time_out_for_assertions(_)), |
400 | | retractall(use_no_timeout(_)), |
401 | | retractall(state_error(_,_,_)), |
402 | | clear_context_state, |
403 | | reset_transition_store, |
404 | | retractall(operation_not_yet_covered(_)), |
405 | | retractall(hash_to_id(_,_)), |
406 | | retractall(hash_to_nauty_id(_,_)), |
407 | | retractall(id_to_marker(_,_)), |
408 | | retractall(specialized_inv(_,_)), |
409 | | retractall(reuse_operation(_,_,_,_)), |
410 | | state_space_add(root,root), |
411 | | add_id_at_front(root), |
412 | | hashing:my_term_hash(root,RootHash), |
413 | | assert(hash_to_id(RootHash,root)), |
414 | | %assert(not_invariant_checked(root)), |
415 | | state_space_reset. |
416 | | |
417 | | :- use_module(eventhandling,[register_event_listener/3]). |
418 | | :- register_event_listener(startup_prob,state_space_startup, |
419 | | 'Initialise Statespace Counters.'). |
420 | | :- register_event_listener(reset_specification,state_space_initialise, |
421 | | 'Reset Statespace.'). |
422 | | :- register_event_listener(change_of_animation_mode,state_space_initialise, |
423 | | 'Reset Statespace.'). |
424 | | |
425 | | /* A version of reset which checks how much memory is used by each fact */ |
426 | | /* state_space:init_with_stats */ |
427 | | state_space_initialise_with_stats :- |
428 | | reset_gennum, reset_gensym, reset_state_counter, reset_processed_nodes_counter, |
429 | | reset_next_state_error_id_counter, |
430 | | retract_open_ids_with_statistics, |
431 | | retract_with_statistics(state_space,[packed_visited_expression(_,_), |
432 | | not_invariant_checked(_), |
433 | | not_interesting(_), |
434 | | max_reached_for_node(_), |
435 | | time_out_for_node(_,_,_), |
436 | | time_out_for_invariant(_), |
437 | | time_out_for_assertions(_), |
438 | | use_no_timeout(_), |
439 | | state_error(_,_,_), |
440 | | transition(_,_,_,_), |
441 | | transition_info(_,_), |
442 | | operation_not_yet_covered(_), |
443 | | hash_to_id(_,_), |
444 | | hash_to_nauty_id(_,_), |
445 | | id_to_marker(_,_), |
446 | | specialized_inv(_,_), |
447 | | reuse_operation(_,_,_,_), |
448 | | history(_), forward_history(_), op_trace_ids(_)]), |
449 | | retract_stored_values_with_statistics, |
450 | | clear_context_state, |
451 | | reset_transition_store, |
452 | | state_space_add(root,root), |
453 | | add_id_at_front(root), |
454 | | %assert(not_invariant_checked(root)), |
455 | | state_space_reset. |
456 | | |
457 | | |
458 | | |
459 | | :- dynamic op_trace_ids/1. |
460 | | reset_trace :- retractall(op_trace_ids(_)), assert(op_trace_ids([])). |
461 | | get_action_trace(T) :- trace(T). |
462 | | get_action_term_trace(PT) :- trace_with_limit(0,T), project_on_action_term(T,PT). |
463 | | trace(Trace) :- trace_with_limit(500,Trace). |
464 | | trace_with_limit(Limit,Trace) :- |
465 | | op_trace_ids(IDT), reverse(IDT,RIDT), |
466 | | extract_trace_from_transition_ids(RIDT,root,Limit,[],Trace). |
467 | | |
468 | | reset_op_trace_ids :- retractall(op_trace_ids(_)), assert(op_trace_ids([])). |
469 | | add_to_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), assert(op_trace_ids([OpID|OpIDS])). |
470 | | remove_from_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), |
471 | | (OpIDS = [R|Rest] -> assert(op_trace_ids(Rest)), OpID = R |
472 | | ; assert(op_trace_ids(OpIDS)),fail). |
473 | | |
474 | | % translate a list of transition ids (from root) into a list of operation terms |
475 | | extract_term_trace_from_transition_ids(TransIDListFromRoot,Trace) :- |
476 | | extract_trace_from_transition_ids(TransIDListFromRoot,root,0,[],ActionTrace), |
477 | | reverse_and_project_on_action_term(ActionTrace,[],Trace). |
478 | | |
479 | | reverse_and_project_on_action_term([],A,A). |
480 | | reverse_and_project_on_action_term([action(_,Term)|T],Acc,Res) :- !, |
481 | | reverse_and_project_on_action_term(T,[Term|Acc],Res). |
482 | | reverse_and_project_on_action_term([H|T],Acc,Res) :- |
483 | | add_error(reverse_and_project_on_action_term,'Illegal action: ',H), |
484 | | reverse_and_project_on_action_term(T,[H|Acc],Res). |
485 | | |
486 | | project_on_action_term([],[]). |
487 | | project_on_action_term([action(_,Term)|T],Res) :- !, Res=[Term|TR], |
488 | | project_on_action_term(T,TR). |
489 | | project_on_action_term([H|T],Res) :- |
490 | | add_error(project_on_action_term,'Illegal action: ',H), |
491 | | project_on_action_term(T,Res). |
492 | | |
493 | | extract_trace_from_transition_ids([],_CurrentState,_,Trace,Trace). |
494 | | extract_trace_from_transition_ids([TransId|Rest],CurrentState,Limit,AccTrace,Trace) :- |
495 | | compute_op_string(TransId,CurrentState,Limit,OpTerm,OpString,DestState),!, |
496 | | extract_trace_from_transition_ids(Rest,DestState,Limit, |
497 | | [action(OpString,OpTerm)|AccTrace],Trace). |
498 | | extract_trace_from_transition_ids([TransId|_],CurrentState,_,_,_Trace) :- |
499 | | add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail. |
500 | | |
501 | | :- use_module(translate,[translate_event_with_src_and_target_id/5]). |
502 | | compute_op_string(jump(TO),_CurID,_,Term,String,DestID) :- !, Term=jump,String=jump,DestID=TO. |
503 | | compute_op_string(TransId,CurID,Limit,Term,String,DestID) :- transition(CurID,Term,TransId,DestID), |
504 | | translate_event_with_src_and_target_id(Term,CurID,DestID,Limit,String). |
505 | | |
506 | | state_space_reset :- |
507 | | reset_trace, |
508 | | retractall(history(_)), |
509 | | retractall(forward_history(_)), |
510 | | retractall(current_state_id(_)), |
511 | | retractall(current_options(_)), |
512 | | assert(history([])), |
513 | | assert(current_state_id(root)). |
514 | | |
515 | | |
516 | | state_space_clean_all :- |
517 | | retractall(state_space_version_in_file(_)), |
518 | | retractall_visited_expression(_), |
519 | | reset_open_ids, |
520 | | retractall(not_invariant_checked(_)), |
521 | | retractall(not_interesting(_)), |
522 | | retractall(max_reached_for_node(_)), |
523 | | retractall(time_out_for_node(_,_,_)), |
524 | | retractall(time_out_for_invariant(_)), |
525 | | retractall(time_out_for_assertions(_)), |
526 | | retractall(use_no_timeout(_)), |
527 | | retractall(state_error(_,_,_)), |
528 | | clear_context_state, |
529 | | reset_transition_store, |
530 | | retractall(operation_not_yet_covered(_)), |
531 | | retractall(hash_to_id(_,_)), |
532 | | retractall(hash_to_nauty_id(_,_)), |
533 | | retractall(id_to_marker(_,_)), |
534 | | retractall(specialized_inv(_,_)), |
535 | | retractall(reuse_operation(_,_,_,_)), |
536 | | retractall(history(_)), |
537 | | retractall(forward_history(_)), |
538 | | retractall(op_trace_ids(_)), |
539 | | retractall(current_state_id(_)), |
540 | | retractall(current_options(_)). |
541 | | |
542 | | % this is only used from within the Tcl/Tk animator at the moment: |
543 | | delete_node(ID) :- print(deleting(ID)),nl, |
544 | | retractall_visited_expression(ID), |
545 | | retractall_invariant_violated(ID), |
546 | | retract_open_node_and_update_processed_nodes(ID), |
547 | | retractall(not_invariant_checked(ID)), |
548 | | retractall(not_interesting(ID)), |
549 | | retractall(max_reached_for_node(ID)), |
550 | | retractall(time_out_for_node(ID,_,_)), |
551 | | retractall(time_out_for_invariant(ID)), |
552 | | retractall(time_out_for_assertions(ID)), |
553 | | retractall(use_no_timeout(ID)), |
554 | | retractall(state_error(ID,_,_)), |
555 | | retractall(transition(ID,_,_,_)), |
556 | | % to do: check if operation_not_yet_covered(_) changes |
557 | | retract_hash(ID), |
558 | | retractall(id_to_marker(ID,_)). |
559 | | |
560 | | retract_hash(ID) :- retract(hash_to_id(Hash,ID)), retractall(hash_to_nauty_id(_TermHash,Hash)),fail. |
561 | | retract_hash(_). |
562 | | |
563 | | assert_max_reached_for_node(Id) :- %print_message(max_reached_for_node(Id)), |
564 | | (max_reached_for_node(Id) -> true ; assert(max_reached_for_node(Id))). |
565 | | |
566 | | assert_time_out_for_node(Id,OpName,TypeOfTimeOut) :- print_message(time_out_for_node(Id,OpName,TypeOfTimeOut)), |
567 | | (time_out_for_node(Id,OpName,_) -> true ; assert(time_out_for_node(Id,OpName,TypeOfTimeOut))). |
568 | | assert_time_out_for_invariant(Id) :- print_message(time_out_for_invariant(Id)), |
569 | | (time_out_for_invariant(Id) -> true ; assert(time_out_for_invariant(Id))). |
570 | | assert_time_out_for_assertions(Id) :- print_message(time_out_for_assertions(Id)), |
571 | | (time_out_for_assertions(Id) -> true ; assert(time_out_for_assertions(Id))). |
572 | | |
573 | | max_reached_or_timeout_for_node(Id) :- |
574 | | (max_reached_for_node(Id) ; time_out_for_node(Id,_,_)). |
575 | | /* ---------------------- */ |
576 | | /* state space saving */ |
577 | | /* ---------------------- */ |
578 | | |
579 | | :- dynamic state_space_version_in_file/1. % |
580 | | state_space_version(1). |
581 | | |
582 | | check_state_space_version :- state_space_version(V), |
583 | | (state_space_version_in_file(F) -> true ; F=0), |
584 | | (V>F -> add_message(state_space,'Warning: saved state_space may be incompatible with current version: ',F:V) ; true). |
585 | | |
586 | | tcltk_save_state(File) :- |
587 | | print('% saving state to: '), print(File),nl, |
588 | | tell(File), |
589 | | print_state_space, |
590 | | told, |
591 | | print_message(done). |
592 | | |
593 | | |
594 | | :- use_module(tools_printing, [print_dynamic_fact/1,print_dynamic_pred/3]). |
595 | | print_state_space :- |
596 | | state_space_version(V), |
597 | | print_dynamic_fact(state_space_version_in_file(V)), |
598 | | % TO DO: maybe also save some important preferences, and warn user and/or propose to adapt preferences ? |
599 | | print_dynamic_pred(state_space,history,1), |
600 | | print_dynamic_pred(state_space,forward_history,1), |
601 | | print_dynamic_pred(state_space,op_trace_ids,1), |
602 | | print_dynamic_pred(state_space,current_state_id,1), |
603 | | print_dynamic_pred(state_space,current_options,1), |
604 | | print_dynamic_pred(state_space,packed_visited_expression,2), |
605 | | print_dynamic_pred(state_space,not_invariant_checked,1), |
606 | | print_dynamic_pred(state_space,not_interesting,1), |
607 | | print_dynamic_pred(state_space,max_reached_for_node,1), |
608 | | print_dynamic_pred(state_space,time_out_for_node,3), |
609 | | print_dynamic_pred(state_space,use_no_timeout,1), |
610 | | print_dynamic_pred(state_space,transition,4), |
611 | | print_dynamic_pred(state_space,transition_info,2), |
612 | | print_dynamic_pred(state_space,operation_not_yet_covered,1), |
613 | | print_dynamic_pred(state_space,state_error,3), |
614 | | print_state_space_open_nodes, |
615 | | print_stored_values, |
616 | | get_counter(states,X), |
617 | | write_term(saved_gennum_count(X),[quoted(true)]),print('.'),nl. |
618 | | |
619 | | saved_gennum_count(99999). |
620 | | |
621 | | /* ---------------------- */ |
622 | | /* state space loading */ |
623 | | /* ---------------------- */ |
624 | | |
625 | | tcltk_load_state(File) :- state_space_clean_all, |
626 | | print('Loading: '), print(File),nl, |
627 | | user_consult_without_redefine_warning(File), % this will read in bind_skeleton/2, ..., next_value_id/1 |
628 | | check_state_space_version, |
629 | | print('Generating open node info'),nl, |
630 | | transfer_open_node_info, |
631 | | print('Transfer state packing info'),nl, |
632 | | transfer_state_packing_info, |
633 | | print('Recomputing hash index'),nl, |
634 | | recompute_all_hash, |
635 | | (saved_gennum_count(X) -> reset_state_counter(X) ; true), |
636 | | reset_processed_nodes_counter, % TO DO: restore or save it |
637 | | reset_next_state_error_id_counter, % DITTO |
638 | | print('Done'),nl,!. |
639 | | tcltk_load_state(File) :- |
640 | | add_error(tcltk_load_state,'Could not load state from file: ',File), |
641 | | state_space_initialise. |
642 | | |
643 | | :- dynamic not_all_z_saved/1, not_all_transitions_added_saved/1. |
644 | | :- dynamic bind_skeleton/2, stored_value/2, stored_value_hash_to_id/2, next_value_id/1. |
645 | | |
646 | | % transfer facts read into state_space into other modules: |
647 | | transfer_open_node_info :- retract(not_all_z_saved(X)), %print(not_all_z(X)),nl, |
648 | | assert_not_all_z(X),fail. |
649 | | transfer_open_node_info :- retract(not_all_transitions_added_saved(X)), |
650 | | assert_not_all_transitions_added(X),fail. |
651 | | transfer_open_node_info. |
652 | | % now for transferring to state_packing module info generated by print_stored_values |
653 | | transfer_state_packing_info :- retract(bind_skeleton(X,Y)), %print(skel(X)),nl, |
654 | | assert(state_packing:bind_skeleton(X,Y)),fail. |
655 | | transfer_state_packing_info :- retract(stored_value(X,Y)), |
656 | | assert(state_packing:stored_value(X,Y)),fail. |
657 | | transfer_state_packing_info :- retract(stored_value_hash_to_id(X,Y)), |
658 | | assert(state_packing:stored_value_hash_to_id(X,Y)),fail. |
659 | | transfer_state_packing_info :- retract(next_value_id(X)), |
660 | | assert(state_packing:next_value_id(X)),fail. |
661 | | transfer_state_packing_info. |
662 | | |
663 | | recompute_all_hash :- |
664 | | retractall(hash_to_id(_,_)),retractall(id_to_marker(_,_)), |
665 | | retractall(hash_to_nauty_id(_,_)), |
666 | | visited_expression(ID,StateTemplate), |
667 | | state_space_exploration_modes:compute_hash(StateTemplate,Hash,Marker), |
668 | | assert(hash_to_id(Hash,ID)), |
669 | | assert(id_to_marker(ID,Marker)), |
670 | | fail. |
671 | | recompute_all_hash. |
672 | | |
673 | | :- use_module(hashing,[my_term_hash/2]). |
674 | | % generates a hash for the entire state space not depending on the order in which states where added |
675 | | compute_full_state_space_hash(Hash) :- |
676 | | findall(Hash,hash_to_id(Hash,_),ListOfHashCodes), |
677 | | sort(ListOfHashCodes,SortedList), |
678 | | my_term_hash(SortedList,Hash). |
679 | | % TO DO: also provide transition hashes |
680 | | |
681 | | :- use_module(tools_meta,[safe_on_exception/3]). |
682 | | user_consult_without_redefine_warning(File) :- |
683 | | prolog_flag(redefine_warnings, Old, off), |
684 | | prolog_flag(single_var_warnings, Old2, off), |
685 | | (safe_on_exception(Exc,consult(File),(nl,print('Exception occurred:'),print(Exc),nl,fail)) |
686 | | -> OK=true ; OK=false), |
687 | | prolog_flag(redefine_warnings, _, Old), |
688 | | prolog_flag(single_var_warnings, _, Old2), |
689 | | OK=true. |
690 | | |
691 | | |
692 | | |
693 | | execute_id_trace_from_current(ID,OpIDL,StateIDList) :- |
694 | | current_state_id(CurID), |
695 | | reverse([CurID|StateIDList],Rev), |
696 | | Rev = [Dest|TRev], (Dest==ID -> true ; (print(not_eq(Dest,ID)),nl)), |
697 | | retract(history(H)), retractall(forward_history(_)), |
698 | | append(TRev,H,NewH), |
699 | | assert(history(NewH)), |
700 | | retract(op_trace_ids(OldTrace)), |
701 | | reverse(OpIDL,NewTrace), |
702 | | append(NewTrace,OldTrace,Trace), |
703 | | assert(op_trace_ids(Trace)), |
704 | | retractall(current_state_id(_)), |
705 | | assert(current_state_id(ID)). |
706 | | %execute_trace_to_node(OpL,StateIDList). /* <----- BOTTLENECK FOR LONG SEQUENCES */ |
707 | | %generate_trace([],Acc,Acc). |
708 | | %generate_trace([OpTerm|T],Acc,Res) :- |
709 | | % translate:translate_event(OpTerm,OpString), |
710 | | % generate_trace(T,[action(OpString,OpTerm)|Acc],Res). |
711 | | |
712 | | set_trace_by_transition_ids(TransitionIds) :- |
713 | | extract_history_from_transition_ids(TransitionIds,root,[],[],Last,History,OpTrace), |
714 | | %visited_expression(Last,LastState,LastCond), |
715 | | retractall(history(_)), retractall(forward_history(_)), |
716 | | retractall(current_state_id(_)), |
717 | | retractall(op_trace_ids(_)), |
718 | | assert(history(History)), assert(op_trace_ids(OpTrace)), |
719 | | assert(current_state_id(Last)). |
720 | | |
721 | | extract_history_from_transition_ids([],CurrentState,History,Trace,CurrentState,History,Trace). |
722 | | extract_history_from_transition_ids([TransId|Rest],CurrentState,AccHist,AccTrace,Last,History,Trace) :- |
723 | | transition(CurrentState,_,TransId,DestState),!, |
724 | | extract_history_from_transition_ids(Rest,DestState,[CurrentState|AccHist], |
725 | | [TransId|AccTrace],Last,History,Trace). |
726 | | extract_history_from_transition_ids([TransId|_],CurrentState,_,_,_,_,_Trace) :- |
727 | | add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail. |
728 | | |
729 | | |
730 | | |
731 | | /* --------------------------------- */ |
732 | | :- dynamic max_nr_of_new_nodes/1. |
733 | | |
734 | | % negative number or non-number signifies no limit |
735 | | set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :- |
736 | | retractall(max_nr_of_new_nodes(_)), |
737 | | (number(MaxNrOfNewNodes), MaxNrOfNewNodes>=0 |
738 | | -> assert(max_nr_of_new_nodes(MaxNrOfNewNodes)) |
739 | | ; true). % no need to store limit |
740 | | |
741 | | get_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :- |
742 | | (max_nr_of_new_nodes(Max) -> MaxNrOfNewNodes=Max; MaxNrOfNewNodes = 0). |
743 | | |
744 | | impl_trans_term(From,ActionAsTerm,To) :- |
745 | | compute_transitions_if_necessary_saved(From), |
746 | | transition(From,ActionAsTerm,_TID,To). |
747 | | |
748 | | impl_trans_term_all(From,Ops) :- |
749 | | compute_transitions_if_necessary_saved(From), |
750 | | findall(op(Id,ActionAsTerm,To), |
751 | | transition(From,ActionAsTerm,Id,To), |
752 | | Ops). |
753 | | |
754 | | compute_transitions_if_necessary_saved(From) :- |
755 | | on_exception(error(forced_interrupt_error('User has interrupted the current execution'),_), |
756 | | compute_transitions_if_necessary(From), |
757 | | user:process_interrupted_error_message). |
758 | | |
759 | | compute_transitions_if_necessary(From) :- |
760 | | not_all_transitions_added(From),!, |
761 | | decrease_max_nr_of_new_nodes(From), |
762 | | %user:do_one_gui_event, |
763 | | user:compute_all_transitions_if_necessary(From,false). |
764 | | compute_transitions_if_necessary(_From). |
765 | | |
766 | | decrease_max_nr_of_new_nodes(ID) :- |
767 | | retract(max_nr_of_new_nodes(Max)),!, |
768 | | ( Max>0 -> |
769 | | NewMax is Max-1, |
770 | | assert(max_nr_of_new_nodes(NewMax)) |
771 | | ; Max=0 -> NM is -1, |
772 | | assert(max_nr_of_new_nodes(NM)), |
773 | | add_warning(state_space,'Maximum number of new nodes reached for CTL/LTL/refinement check, node id = ',ID), |
774 | | %trace, |
775 | | fail |
776 | | ; otherwise -> % negative number: re-assert and fail |
777 | | assert(max_nr_of_new_nodes(Max)), |
778 | | fail). |
779 | | decrease_max_nr_of_new_nodes(_). % no limit stored; just proceed |
780 | | |
781 | | % will be called from TCL/TK side |
782 | | max_nr_of_new_nodes_limit_not_reached :- |
783 | | max_nr_of_new_nodes(N),N>0. |
784 | | |
785 | | :- use_module(specfile,[b_or_z_mode/0]). |
786 | | retract_open_node(NodeID) :- retract_open_node_and_update_processed_nodes(NodeID), |
787 | | (b_or_z_mode -> assert(not_invariant_checked(NodeID)) ; true). |
788 | | |
789 | | reset_processed_nodes_counter :- reset_counter(processed_nodes). |
790 | | %reset_processed_nodes_counter(Nr) :- set_counter(processed_nodes,Nr). |
791 | | |
792 | | retract_open_node_and_update_processed_nodes(NodeID) :- |
793 | | retract_open_node_direct(NodeID), |
794 | | inc_processed. |
795 | | |
796 | | inc_processed :- |
797 | | inc_counter(processed_nodes). |
798 | | |
799 | | pop_id_from_front(ID) :- pop_id_from_front_direct(ID), inc_processed. |
800 | | pop_id_from_end(ID) :- pop_id_from_end_direct(ID), inc_processed. |
801 | | pop_id_oldest(ID) :- pop_id_oldest_direct(ID), inc_processed. |
802 | | |
803 | | /* --------------------------------- */ |
804 | | |
805 | | % |
806 | | % Code to compute equivalence classes |
807 | | % using the standard DFA minimization algorithm |
808 | | |
809 | | :- dynamic equivalent/2. |
810 | | % state_space:compute_equivalence_classes |
811 | | :- public compute_equivalence_classes/0. |
812 | | |
813 | | compute_equivalence_classes :- init_equi, |
814 | | split_equivalence_classes,nl, |
815 | | print_equi. |
816 | | |
817 | | print_equi :- state_space:equivalent(A,B), visited_expression(A,State), |
818 | | visited_expression(B,StateB), |
819 | | nl, |
820 | | print(A), print(' : '), print(State),nl, |
821 | | print(B), print(' : '), print(StateB),nl,fail. |
822 | | print_equi. |
823 | | |
824 | | init_equi :- retractall(equivalent(_,_)), |
825 | | packed_visited_expression(ID,_State), |
826 | | \+ not_all_transitions_added(ID), |
827 | | findall(Action,transition(ID,Action,_,_),List), |
828 | | packed_visited_expression(ID2,_S2), ID2 @> ID, |
829 | | \+ not_all_transitions_added(ID2), |
830 | | findall(Action,transition(ID2,Action,_,_),List), |
831 | | assert(equivalent(ID,ID2)), % they have the same signature |
832 | | %print(equivalent(ID,ID2)),nl, |
833 | | fail. |
834 | | init_equi :- print(finished_initialising),nl. |
835 | | |
836 | | split_equivalence_classes :- retractall(echange), |
837 | | equivalent(ID1,ID2), |
838 | | transition(ID1,A,_,Dest1), |
839 | | transition(ID2,A,_,Dest2), |
840 | | \+ check_equi(Dest1,Dest2), |
841 | | retract(equivalent(ID1,ID2)), % splitting class |
842 | | % print(diff(ID1,ID2, A, Dest1, Dest2)),nl, |
843 | | assert_echange, |
844 | | fail. |
845 | | split_equivalence_classes :- echange -> split_equivalence_classes ; true. |
846 | | |
847 | | :- dynamic echange/0. |
848 | | assert_echange :- echange -> true ; assert(echange),print('.'),flush_output. |
849 | | |
850 | | check_equi(A,B) :- A=B -> true ; A @<B -> equivalent(A,B) ; equivalent(B,A). |
851 | | |
852 | | /* |
853 | | % benchmark how much time it takes to copy the state space state_space:bench_state_space. |
854 | | bench_state_space :- |
855 | | statistics(walltime,_), |
856 | | (state_space:packed_visited_expression(ID,S), assert(pve(ID,S)),fail ; true), |
857 | | statistics(walltime,[_,Delta]), format('Time to copy packed_visited_expression: ~w ms~n',[Delta]), |
858 | | (state_space:transition(A,B,C,D), assert(tr(A,B,C,D)),fail ; true), |
859 | | statistics(walltime,[_,Delta2]), format('Time to copy transition: ~w ms~n',[Delta2]), |
860 | | (state_packing:stored_value(A,B), assert(sv(A,B)),fail ; true), |
861 | | (state_packing:stored_value_hash_to_id(A,B), assert(svhi(A,B)),fail ; true), |
862 | | statistics(walltime,[_,Delta3]), format('Time to copy stored_value: ~w ms~n',[Delta3]). |
863 | | */ |
864 | | |