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