1		% (c) 2016-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(b_operation_cache, [ %project_in_state/6,
6		%operation_computed/4,
7		compute_operation_on_expanded_store_cache/6,
8		check_invariant_violated_cache/2,
9		print_op_cache_profile/0,
10		get_op_cache_stats/1,
11		reset_b_operation_cache_with_statistics/0,
12		tcltk_op_cache_stats/1
13		]).
14
15
16		:- use_module(probsrc(module_information)).
17		:- module_info(group,animator).
18		:- module_info(description,'This module caches B operation results on projected states. Used when preference try_operation_reuse different from false').
19
20		% TO DO:
21		% provide predecessor ID and operation to know which values are unchanged? -> reuse hash; know which ops are definitely disabled? (cf pge)
22		% Note: operation caching works better with COMPRESSION TRUE, as this way the values are pre-hashed. A simpler hash function is then used.
23		% Note: if we change the MAX_OPERATIONS preference, this will have no effect on already cached operations
24		% TODO: we could invalidate operation cache upon such a change; storing the value for each node is probably overkill
25
26		:- use_module(probsrc(self_check)).
27		:- use_module(extension('counter/counter')). % op_cache_id,... counter
28		:- use_module(probsrc(succeed_max),[succeed_max_call_id/3, reset_max_reached/1, max_reached/1, assert_max_reached/1]).
29		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
30		:- use_module(probsrc(error_manager)).
31		:- use_module(probsrc(debug),[debug_println/2]).
32		:- use_module(probsrc(performance_messages),[perfmessage/2]).
33		:- use_module(library(ordsets), [ord_subtract/3]).
34		:- use_module(probsrc(tools),[retract_with_statistics/2]).
35
36		b_operation_cache_startup :- % call once at startup to ensure all counters exist
37		counter_init,
38		new_counter(op_cache_id),
39		new_counter(inv_cache_nr),
40		new_counter(op_cached_failures),
41		new_counter(op_cached_successes),
42		new_counter(inv_cached_successes),
43		new_counter(op_cached_timeouts),
44		new_counter(op_cached_enum_warnings),
45		new_counter(op_cached_errors).
46
47
48		:- register_event_listener(startup_prob,b_operation_cache_startup,
49		'Initialise Statespace Counters.').
50		:- register_event_listener(reset_specification,reset_b_operation_cache,
51		'Reset Operation Cache.').
52		:- register_event_listener(clear_specification,reset_b_operation_cache, % necessary? as reset occurs before?
53		'Reset Operation Cache.').
54		:- register_event_listener(change_of_animation_mode,reset_b_operation_cache,
55		'Reset Operation Cache.').
56		% TO DO: also reset if maxNrOfEnablingsPerOperation changed ?
57
58
59		:- dynamic operation_read_projection_cache/5, operation_read_constants/2, operation_guard_read_info/3.
60		reset_b_operation_cache :-
61		retractall(operation_read_projection_cache(_,_,_,_,_)),
62		retractall(operation_read_constants(_,_)),
63		retractall(operation_guard_read_info(_,_,_)),
64		retractall(operation_computed(_,_,_,_,_)),
65		retractall(operation_cached_results(_,_,_,_)),
66		retractall(operation_cached_max_reached(_,_)),
67		retractall(operation_cached_time_out(_,_)),
68		retractall(operation_cached_enum_warning(_,_,_)),
69		retractall(op_guard_fails(_,_,_)),
70		reset_counter(op_cache_id),
71		reset_counter(inv_cache_nr),
72		reset_counter(op_cached_failures),
73		reset_counter(op_cached_successes),
74		reset_counter(inv_cached_successes).
75
76
77		reset_b_operation_cache_with_statistics :-
78		retract_with_statistics(b_operation_cache,
79		[operation_read_projection_cache(_,_,_,_,_),
80		operation_read_constants(_,_),operation_guard_read_info(_,_,_),
81		operation_computed(_,_,_,_,_), operation_cached_results(_,_,_,_),
82		operation_cached_max_reached(_,_),
83		operation_cached_time_out(_,_),
84		operation_cached_enum_warning(_,_,_),
85		op_guard_fails(_,_,_)
86		]
87		),
88		reset_b_operation_cache.
89
90
91		% -------------------------------------------------
92
93
94		% project the in-state for an operation onto the relevant variables
95		project_in_state(VarsInState,OpName,ProjectedInState) :-
96		get_opname_key(OpName,OpNameKey),
97		project_in_state_for_opname_key(VarsInState,OpNameKey,ProjectedInState).
98
99		:- use_module(probsrc(bmachine),[b_is_constant/1]).
100		:- use_module(library(lists),[exclude/3, include/3]).
101		project_in_state_for_opname_key(InState,OpNameKey,ProjectedInState) :-
102		get_operation_read_projection_infos(OpNameKey,_,InState,ProjVars,_,_),
103		(re_project_state(ProjVars,InState,Res) -> ProjectedInState=Res
104		; add_internal_error('Re-Projection failed: ',re_project_state(ProjVars,InState,_)),
105		ProjectedInState = InState).
106
107		:- use_module(probsrc(specfile),[csp_with_bz_mode/0]).
108		:- use_module(probsrc(b_read_write_info),[b_get_operation_read_guard_vars/4]).
109		:- use_module(probsrc(bmachine),[b_definition_prefixed/5]).
110
111
112		% get infos about cached operations (and compute the first time info requested for an operation)
113		get_operation_read_projection_infos(OpNameKey,OpName,_,ProjVars,IsReadingCsts,AdditionalOutVars) :-
114		operation_read_projection_cache(OpNameKey,OpName,ProjVars,IsReadingCsts,AdditionalOutVars),!,
115		ProjVars \= no_caching.
116		get_operation_read_projection_infos(OpNameKey,OpName,_,_,_,_) :- atom(OpName),
117		b_definition_prefixed(_, 'OPERATION_REUSE_OFF_', OpName, _DefName,_),
118		!,
119		format('Ignoring operation ~w for reuse~n',[OpName]),
120		assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])),
121		fail.
122		get_operation_read_projection_infos(OpNameKey,OpName,InState,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars) :-
123		api_get_operation_read_write_info(OpName,ReadVariables,ReadConstants,WrittenVariables),
124		(ReadConstants=[] -> IsReadingCsts=false ; IsReadingCsts=true),
125		debug_println(19,operation_reads_vars_consts(OpName,ReadVariables,ReadConstants)),
126		(project_state_onto_vars(InState,ReadVariables,ProjVarsInOrder,_RelevantState,0,NrDeleted)
127		-> % TO DO: if we have constants in the state which are deterministic anyway, then they should not count
128		% TO DO: statically pre-compute which operations are worthwhile for this treatment
129		((NrDeleted>0 % we project away at least one variable and thus hope to cache operation results
130		; csp_with_bz_mode) % in CSP||B mode, the same operation may be called with different CSP controllers
131		-> ord_subtract(WrittenVariables,ReadVariables,AdditionalOutVars), % vars written but not read
132		assertz(operation_read_projection_cache(OpNameKey,OpName,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars)),
133		assertz(operation_read_constants(OpNameKey,ReadConstants)),
134		% ,print(proj(OpName,ProjVarsInOrder,AdditionalOutVars)),nl,
135		(get_preference(try_operation_reuse,full),
136		b_get_operation_read_guard_vars(OpName,true,ReadVarsInGuard,precise),
137		exclude(member_ord(ReadVarsInGuard),ProjVarsInOrder,IrrelevantVars),
138		% TO DO: analyse if projection really useful
139		IrrelevantVars \= []
140		-> include(member_ord(ReadVarsInGuard),ProjVarsInOrder,ReadVarsInGuard),
141		debug_println(19,guard_reads_subset_of_vars(OpName,OpNameKey,ReadVarsInGuard,IrrelevantVars)),
142		assertz(operation_guard_read_info(OpNameKey,ReadVarsInGuard,IrrelevantVars))
143		; true)
144		; assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])),
145		perfmessage('Not caching operation for reuse: ',OpName),
146		fail
147		)
148		; add_internal_error('Projection failed for: ', project_state_onto_vars(InState,ReadVariables,_,_,0,_)),
149		assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])),
150		fail
151		).
152		%TODO: also compute precise guard b_get_operation_read_guard_vars(Operation,JustVariables,VarsResult,VarsPrecise) if possible and if read vars in guard << ReadVariables also store this
153		% if operation call fails -> store only precise guard
154
155		% -------------------------------
156
157		% API to abstract operations so that we can use caching also for invariants, maybe later assertions, ...
158
159		% get atomic key to store operation info
160		get_opname_key(Name,Res) :- var(Name),!,
161		add_internal_error('Variable opname: ',get_opname_key(Name,Res)), Res=Name.
162		get_opname_key(check_invariant_violated(Nr),Key) :- !, Key=Nr.
163		get_opname_key(Name,Name).
164
165		api_get_operation_read_write_info(OpName,ReadVariables,ReadConstants,WrittenVariables) :-
166		api_get_op_rw_aux(OpName,ReadIds,WrittenVariables),
167		exclude(b_is_constant,ReadIds,ReadVariables),
168		include(b_is_constant,ReadIds,ReadConstants).
169		:- use_module(probsrc(bmachine),[b_nth1_invariant/3,b_get_operation_normalized_read_write_info/3]).
170		api_get_op_rw_aux(check_invariant_violated(Nr),UsedIds,Written) :- !, Written=[],
171		b_nth1_invariant(Nr,_,UsedIds).
172		api_get_op_rw_aux(OpName,ReadVariables,WrittenVariables) :-
173		b_get_operation_normalized_read_write_info(OpName,ReadVariables,WrittenVariables).
174
175
176		:- use_module(probsrc(b_interpreter),[b_execute_top_level_operation_update/5]).
177
178		% we use a trick using a mutable to detect when a time_out or exception has been thrown
179		% during caching; we could have used assert/retract or bb_put/bb_get instead
180
181		api_compute_operation_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall) :-
182		create_mutable(still_computing,Done),
183		%tools:start_ms_timer(Timer),
184		(event_occurred_in_error_scope(E)
185		-> add_message(b_operation_cache,'Error scope not fresh: ',E),
186		enter_new_error_scope(Level)
187		; Level=none),
188		call_cleanup(
189		com_op_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,Done),
190		(get_mutable(still_computing,Done)
191		-> format('Timeout, exception or virtual timeout occured during caching for ~w (cache id ~w)~n',[OpName,NewID]),
192		% also happens during -execute due to cut!, hence we now disable preference in -execute
193		% stop_ms_timer_with_msg(Timer,'Runtime for computing'),
194		exit_scope(Level),
195		register_op_cache_time_out(NewID,OpName)
196		; error_occurred_in_error_scope
197		-> format('Error occurred during caching for ~w (cache id ~w)~n',[OpName,NewID]),
198		invalidate_operation_cache(NewID,OpName),
199		exit_scope(Level)
200		; event_occurred_in_error_scope(Event),
201		functor(Event,Kind,_),
202		format('Event ~w occurred during caching for ~w (cache id ~w)~n',[Kind,OpName,NewID]),
203		register_op_cache_enum_warning(NewID,OpName,Event),
204		exit_scope(Level),
205		fail
206		% TODO: should we also check if errors occured
207		; exit_scope(Level)
208		)),
209		get_mutable(DVal,Done), DVal \= finished. % fail if we are Done;
210
211		exit_scope(none) :- !.
212		exit_scope(Level) :- exit_error_scope(Level,_).
213
214		% we could do this: but we don't know if an exception, timeout or virtual time_out occurred
215		register_op_cache_time_out(ID,OpName) :-
216		inc_counter(op_cached_timeouts),
217		assertz(operation_cached_time_out(ID,OpName)).
218		register_op_cache_enum_warning(ID,OpName,Event) :-
219		inc_counter(op_cached_enum_warnings),
220		assertz(operation_cached_enum_warning(ID,OpName,Event)).
221		% as an alternative this removes the cached results:
222		invalidate_operation_cache(ID,OpName) :-
223		inc_counter(op_cached_errors),
224		retractall(operation_cached_results(ID,_Operation,_,_)),
225		retractall(operation_computed(_,OpName,_,_,ID)). % can be expensive
226
227
228
229		com_op_update_max(_,check_invariant_violated(Nr),Operation,ProjState,NewState,PathInfo,_,Done) :- !,
230		NewState =[], PathInfo=invariant, Operation=Nr, % values not used anyway for invariants
231		%print(check_invariant(Nr)),nl, bmachine:b_nth1_invariant(Nr,Inv,_UsedIds), translate:print_bexpr(Inv),nl,
232		(b_interpreter:check_nth1_invariant(Nr,ProjState )
233		-> update_mutable(finished,Done) % will lead to failure above; we store only violations
234		; % invariant violation found
235		update_mutable(last_sol_found,Done)
236		).
237		com_op_update_max(_,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,_) :-
238		% for CSP||B: clear out any parameters; otherwise we also need to hash the parameters
239		reset_max_reached(OpName),
240		succeed_max_call_id(OpName,
241		b_execute_top_level_operation_update(OpName,Operation,ProjInOutState,NewState,PathInfo),
242		MaxForCall).
243		% TO DO: normalise_store out state values, to avoid re-normalising when storing updates
244		com_op_update_max(NewID,OpName,_,_,_,_,_,Done) :-
245		(NewID \= uncached,
246		max_reached(OpName)
247		-> assertz(operation_cached_max_reached(NewID,OpName)) % store that we reached max. nr of transitions for this node
248		; true %format('No Timeout or virtual timeout occurred during caching for ~w leading to ~w~n',[OpName,NewID])
249		),
250		update_mutable(finished,Done).
251
252
253
254		% entry point to cache invariant checking
255		check_invariant_violated_cache(Nr,State) :-
256		%get_store_and_info(State,FullStore,Infos),
257		compute_operation_on_expanded_store_cache(check_invariant_violated(Nr),_,State,_,_,-1).
258
259		:- use_module(probsrc(specfile),[expand_const_and_vars_to_full_store/2]).
260		%get_store_and_info(expanded_const_and_vars(_ConstID,_Vars,E,Info),FullStore,Info) :- !, FullStore=E.
261		%get_store_and_info(expanded_vars(E,Info),FullStore,Info) :- !, FullStore=E.
262		%get_store_and_info(Store,FullStore,[]) :- expand_const_and_vars_to_full_store(Store,FullStore).
263
264		% -------------------------------
265
266
267		% check if caching is worthwhile for this operation
268		%worthwhile_to_cache(OpName) :-
269		% get_read_write_info(OpName,ReadVariables,WrittenVariables),
270		% length(ReadVariables,NrRV),
271		% bmachine:b_machine_statistics(variables,NrVars),
272		% bmachine:b_machine_statistics(constants,NrConstants),
273		% Perc is (NrRV*100) // (NrVars+NrConstants),
274		% length(WrittenVariables,NrWV),
275		% format('Analyzing ~w, ~w %, read: ~w, written: ~w, tot vars: ~w, tot cst: ~w~n (read: ~w)~n',[OpName,Perc,NrRV,NrWV,NrVars,NrConstants,ReadVariables]),
276		% Perc < 95. % maybe provide as preference
277
278		:- use_module(library(ordsets),[ord_member/2]).
279		%is_read(ReadVariables,bind(Var,_)) :- ord_member(Var,ReadVariables).
280		member_ord(List,X) :- ord_member(X,List). % for maplist, exclude,...
281
282		% -------------------------------
283
284		% a variation of split_list which also returns a list of predicate results
285		% with re_project_state(L,ProjVarsInOrder,A) : we can split another list using the same pattern
286
287		:- assert_must_succeed((b_operation_cache:project_state_onto_vars([bind(x,1),bind(y,2),bind(b,3)],[b,y],
288		ProjVars,ProjState,0,NrDel),
289		ProjVars == [y,b], ProjState == [bind(y,2),bind(b,3)], NrDel==1)).
290
291		project_state_onto_vars([],_,[],[],Acc,Acc).
292		project_state_onto_vars([Elem|Rest],ReadVariables,ProjVars,ProjState,NrDelAcc,NrDel) :-
293		Elem = bind(Var,_),
294		(ord_member(Var,ReadVariables) % TO DO: we could improve performance by sorting Elements
295		-> ProjVars=[Var|PT], ProjState=[Elem|AR], ND1=NrDelAcc
296		; ProjVars=PT, ProjState=AR, ND1 is NrDelAcc+1),
297		project_state_onto_vars(Rest,ReadVariables,PT,AR,ND1,NrDel).
298
299
300		% -------------------------------
301
302		:- assert_must_succeed((b_operation_cache:re_project_state([y,b],[bind(x,1),bind(y,2),bind(b,3)],Res),
303		Res == [bind(y,2),bind(b,3)])).
304
305		% project state(VarsInOrder,State,ProjectedState)
306		% faster than project_state_onto_vars
307		re_project_state([],_,[]).
308		re_project_state([VarToProject|PT],[Elem|Rest],A) :-
309		arg(1,Elem,Var), %Elem = bind(Var,_),
310		(VarToProject==Var
311		-> A=[Elem|AR],re_project_state(PT,Rest,AR)
312		; re_project_state2(VarToProject,PT,Rest,A)).
313
314		re_project_state2(VarToProject,PT,[Elem|Rest],A) :-
315		arg(1,Elem,Var), %Elem = bind(Var,_),
316		(VarToProject==Var
317		-> A=[Elem|AR],re_project_state(PT,Rest,AR)
318		; re_project_state2(VarToProject,PT,Rest,A)).
319
320		% -----------------------------
321
322		% Two utilities to optionally generate lemma facts for fast projection
323		% Does not seem to be worth it
324
325		% abstract away values, can be used to generate pre-compiled facts
326		%abstract_state([],[]).
327		%abstract_state([bind(Var,_)|T],[bind(Var,_)|AT]) :- abstract_state(T,AT).
328
329		% abstract away unused bindings, can be used to generate pre-compiled facts
330		%clear_unused_bindings([],_,_) :- !.
331		%clear_unused_bindings([VarToProject|PT],[bind(Var,V)|T],[bind(Var,V)|RT]) :-
332		% % we could clear out Variable name Var; but this creates a danger of successfully matching an erroneous state
333		% VarToProject==Var,!,
334		% clear_unused_bindings(PT,T,RT).
335		%clear_unused_bindings(Vars,[_|T],[_|RT]) :- % leave slot in result as fresh var
336		% clear_unused_bindings(Vars,T,RT).
337
338		% -------------------------------
339
340		:- use_module(probsrc(hashing)).
341		:- use_module(probsrc(state_packing)).
342
343		:- dynamic operation_computed/5, operation_cached_results/4,
344		operation_cached_max_reached/2, operation_cached_time_out/2, operation_cached_enum_warning/3,
345		op_guard_fails/3.
346
347		% return Hash and check if operation computed
348		% TO DO: do not hash constants if single value exists ?
349		check_if_operation_was_computed(OpName,ConstID,State,Skel,Infos,PackedValList,IsReadingCsts,
350		HashConstID,Hash,Res) :-
351		(Infos = [packed_state/PS|_]
352		-> get_packed_vars(PS,OpName,PackedState),
353		remove_bind_skeleton(PackedState,Skel,PackedValList)
354		% packing already performed in prepare_state_for_specfile_trans
355		; write(no_packed_state_info(OpName,ConstID)),nl, % shouldn't happen hopefully
356		project_in_state(State,OpName,ProjectedInState), % State contains just variables
357		pack_bind_list(ProjectedInState,Skel,PackedValList)
358		),
359		(IsReadingCsts = false -> HashConstID=root ; HashConstID=ConstID),
360		op_hash(OpName,HashConstID,PackedValList,Hash),
361		(operation_computed(Hash,OpName,HashConstID,PackedValList,ID)
362		-> Res = ID
363		; % operation_guard_read_info(OpKey,GuardVars,_), re_project_state(GuardVars,Skel,PackedValList,GuardPackedVals)
364		% op_hash(OpName,HashConstID,GuardPackedVals,GuardHash), op_guard_fails(GuardHash,OpName,GuardPackedVals,ID) -> true
365		Res= false).
366
367		% project a state or packed value list onto the variables relevant for the guard (if it is a subset)
368		project_onto_guard(OpName,OpKey,HashConstID,Skel,PackedValList,GuardPackedVals,GuardHash) :-
369		operation_guard_read_info(OpKey,_,IgnoredVars),
370		remove_ignored_vars(IgnoredVars,Skel,PackedValList,GuardPackedVals),
371		op_hash(OpName,HashConstID,GuardPackedVals,GuardHash).
372
373
374		% remove_ignored_vars(VarsToIgnore,SkeletonList,ValueList,Result)
375		remove_ignored_vars([],_,PackedVals,Res) :- Res=PackedVals.
376		remove_ignored_vars([ID|T],[ID|ST],[_|PackedVals],GuardPackedVals) :- !,
377		remove_ignored_vars(T,ST,PackedVals,GuardPackedVals).
378		remove_ignored_vars(Ignored,[_|ST],[PV|PackedVals],[PV|GuardPackedVals]) :-
379		remove_ignored_vars(Ignored,ST,PackedVals,GuardPackedVals).
380
381		get_packed_vars(const_and_vars(_,Vars),OpName,PackedVars) :- !, project_in_state(Vars,OpName,PackedVars).
382		get_packed_vars(PS,OpName,PackedVars) :- !, project_in_state(PS,OpName,PackedVars).
383		:- use_module(library(terms),[term_hash/3]).
384		:- use_module(probsrc(hashing),[my_term_hash/2]).
385
386		op_hash(OpName,HashConstID,PackedValList,Hash) :- get_preference(use_state_packing,false),!,
387		my_term_hash((OpName,HashConstID,PackedValList),Hash). % will user super_hash
388		op_hash(OpName,HashConstID,PackedValList,Hash) :-
389		% we use state packing and thus replace AVL sets by identifiers, ...: a simpler hash suffices, but we get collisions for Train1_Lukas_POR (which do not seem to matter); we get an improvement for ifm18/Ref5_Switch_mch.eventb
390		term_hash((OpName,HashConstID,PackedValList),
391		[range(smallint),algorithm(sdbm),depth(infinite),if_var(ignore)], % djb2
392		Hash).
393
394
395		% remove bind/2 wrappers and variable name for faster hashing
396		remove_bind_skeleton([],[],R) :- !, R=[].
397		remove_bind_skeleton([bind(Var,Val)|T],[Var|VT],[Val|RT]) :- !,
398		remove_bind_skeleton(T,VT,RT).
399		remove_bind_skeleton(L,V,R) :- add_internal_error('Illegal store: ',remove_bind_skeleton(L,V,R)), R=L.
400
401		% we could also peel a few infos not useful for hashing:
402		%peel_val('$stored_avl_packed'(Nr),Nr).
403		%peel_val('$avl_bv'(Nr,_),Nr). % correct because if we use a bit_vector we will never also use stored_avl_packed for the same type
404
405
406		get_new_operation_computed_id(OpName,ConstID,PackedValList,Hash,ID) :-
407		inc_counter(op_cache_id,ID),
408		(OpName=check_invariant_violated(_) -> inc_counter(inv_cache_nr,_) ; true),
409		assertz(operation_computed(Hash,OpName,ConstID,PackedValList,ID)).
410		% To reduce memory consumption we could use the following clause:
411		% can be useful if there are many operations with a large number of projected variables
412		% but does lead to noticable slowdown when looking up operations
413		%get_new_operation_computed_id(OpName,ConstID,_PackedValList,Hash,[_,state_id/ReferenceStateID],ID) :- !,
414		% inc_counter(op_cache_id,ID),
415		% assertz(operation_computed(Hash,OpName,ConstID,ReferenceStateID,ID)). % storing reference ID preserves memory
416		% when looking up operation_was_computed we would need to do something like:
417		% state_space:packed_visited_expression(StoredState,PS),
418		% get_packed_b_state_with_uncompressed_lists(PS,PUS),
419		% get_state_infos(PUS,ConstID,PackedList,_,_),
420		% project_in_state(PackedList,OpName,ProjectedStoredState),
421		% remove_bind_skeleton(ProjectedStoredState,Skel,ProjectedValList),
422		% ProjectedValList = PackedValList
423
424
425		:- use_module(probsrc(runtime_profiler),[profile_failure_driven_loop/1]).
426		% this is used when get_preference(try_operation_reuse,true/full)
427		% it is only called for operations, not for setup_constants or initalise_machine
428
429		% treat expanded_const_and_vars(ConstID,Vars,FullStore,Infos)
430
431		get_state_infos(expanded_const_and_vars(ID,Vars,FullStore,I),ConstID,Vars,FullStore,Infos) :- !,ConstID=ID,Infos=I.
432		get_state_infos(expanded_vars(V,I),ConstID,Vars,FullStore,Infos) :- !, ConstID=root,Vars=V,FullStore=V,Infos=I.
433		get_state_infos(const_and_vars(ConstID,Vars),ConstID,Vars,FullStore,Infos) :- !,
434		add_warning(get_state_infos,'State not prepared for caching: ',const_and_vars(ConstID,Vars)),
435		Infos=[],
436		expand_const_and_vars_to_full_store(const_and_vars(ConstID,Vars),FullStore).
437		get_state_infos(csp_and_b(_,State),ConstID,Vars,FullStore,Infos) :- !,
438		get_state_infos(State,ConstID,Vars,FullStore,Infos).
439		get_state_infos(Vars,unknown,Vars,Vars,[]).
440
441		% InState is either already an expanded list or expanded_const_and_vars, expanded_vars
442		compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :-
443		get_state_infos(InState,ConstID,Vars,FullStore,Infos), % extract infos from the store
444		% TO DO: check if state_id in Infos and if OpName in equivalence class with same proj. vars
445		get_opname_key(OpName,OpNameKey),
446		get_operation_read_projection_infos(OpNameKey,OpName,Vars,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars),
447		!,
448		% tools_printing:print_term_summary(proj(OpName,ConstID,ProjInState,FullStore)),nl,
449		check_if_operation_was_computed(OpName,ConstID,Vars,ProjVarsInOrder,Infos,PackedValList,IsReadingCsts,
450		HashConstID,Hash,ID),
451		(ID \= false
452		-> % we can reuse the stored operation effect
453		%print('+'),
454		%hit_profiler:add_hit(operation_reused,OpName),
455		(inv_op_name(OpName) -> inc_counter(inv_cached_successes)
456		; inc_counter(op_cached_successes)),
457		(operation_cached_results(ID,Operation,PackedNewState,PathInfo),
458		unpack_values(PackedNewState,NewState)
459		; operation_cached_max_reached(ID,OpName), % we did not compute all operations
460		assert_max_reached(OpName),
461		fail
462		; operation_cached_enum_warning(ID,OpName,Event),
463		functor(Event,Kind,_),
464		format('Regenerating ~w for ~w and cache id ~w~n',[Kind,OpName,ID]),
465		add_new_event_in_error_scope(Event),
466		fail
467		; operation_cached_time_out(ID,OpName),
468		format('Rethrowing cached time_out for ~w and cache id ~w~n',[OpName,ID]),
469		throw(time_out)
470		)
471		; % we have not computed solutions for this operation for this projected state
472		(project_onto_guard(OpName,OpNameKey,HashConstID,ProjVarsInOrder,PackedValList,GuardPackedVals,GuardHash)
473		-> true
474		; GuardPackedVals = none),
475		(nonvar(GuardHash),
476		op_guard_fails(GuardHash,OpName,GuardPackedVals)
477		-> % we did already compute this operation for this projected state and it failed
478		inc_counter(op_cached_failures),
479		fail % the guard is guaranteed to fail
480		; % we have not yet computed this operation; compute it and store solutions as we go
481		get_new_operation_computed_id(OpName,HashConstID,PackedValList,Hash,NewID),
482		%print('-'),
483		%hit_profiler:add_hit(operation_cache_computation,OpName),
484		(IsReadingCsts=false
485		-> % TO DO: check if this projection is worthwhile
486		project_in_state_for_opname_key(Vars,OpNameKey,ProjInState),
487		% Note: if no packed_state this projection was already performed in check_if_operation_was_computed
488		add_new_vars(AdditionalOutVars,ProjInState,ProjInOutState)
489		; ProjInOutState = FullStore % use full store with constants
490		),
491		profile_failure_driven_loop(OpName),
492		if(api_compute_operation_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall),
493		(% Normalise here or in update_max
494		pack_values(NewState,PackedNewState),
495		(PathInfo=invariant -> StoredPathInfo=Hash
496		; filter_transition_path_info(PathInfo,StoredPathInfo)),
497		assertz(operation_cached_results(NewID,Operation,PackedNewState,StoredPathInfo))
498		),
499		(nonvar(GuardHash),
500		%print(op_guard_fails(GuardHash,OpName,GuardPackedVals)),nl,
501		assertz(op_guard_fails(GuardHash,OpName,GuardPackedVals)),
502		fail
503		)
504		)
505		)
506		% TO DO: if we have no successors for ID and if the operation reads less IDs in the guard
507		% we can replace remaining identifier values by a variable
508		).
509		compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :-
510		%hit_profiler:add_hit(operation_not_cached,OpName),
511		% operation is not cached
512		get_state_infos(InState,_,_,FullStore,_),
513		api_compute_operation_update_max(uncached,OpName,Operation,FullStore,NewState,PathInfo,MaxForCall).
514
515		% add written vars which are not read virtually to state to avoid error messages in store_intermediate_updates:
516		add_new_vars([],S,S).
517		add_new_vars([WrittenVar|T],State,[bind(WrittenVar,term(undefined))|ST]) :-
518		add_new_vars(T,State,ST).
519
520		:- use_module(probsrc(state_space),[keep_transition_info/1]).
521		filter_transition_path_info([],R) :- !, R=[].
522		filter_transition_path_info([H|T],Res) :- !,
523		(keep_transition_info(H) -> Res = [H|RT]
524		; Res=RT), % by default we filter out possibly large path infos (in particular for Event-B)
525		filter_transition_path_info(T,RT).
526		filter_transition_path_info(H,Res) :-
527		(keep_transition_info(H) -> Res = H ; Res=[]).
528
529
530		invariant_op_key(OpKey,InvNr) :- operation_read_projection_cache(OpKey,check_invariant_violated(InvNr),_,_,_).
531
532		:- use_module(probsrc(bmachine),[b_nth1_invariant/3]).
533		print_violated_invariants :-
534		operation_cached_results(ID,Nr,[],Hash),number(Nr),
535		b_nth1_invariant(Nr,Invariant,_UsedIds),
536		format('Invariant ~w violated (op-cache-id ~w)~n ',[Nr,ID]),
537		translate:print_bexpr(Invariant),nl,
538		% now try and recover state where it was violated:
539		operation_computed(Hash,OpName,ConstID,PackedValList,ID),
540		operation_read_projection_cache(_,OpName,Skel,_,_),
541		unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,StateDesc),
542		format(' in state (ConstID ~w) ~w~n',[ConstID,StateDesc]),
543		fail.
544		print_violated_invariants.
545
546		% small utility code to analyze hash collisions:
547		% b_operation_cache:ahc.
548		:- public ahc/0.
549		ahc :- operation_computed(Hash,OpName,ConstID,State,ID),
550		operation_computed(Hash,OpName2,ConstID2,State2,ID2),
551		(ConstID @> ConstID2 -> true ; ConstID=ConstID2, ID2 > ID),
552		format('Hash collision: ~w~n ~w:~w:~w:~w~n ~w:~w:~w:~w~n~n',
553		[Hash,OpName,ConstID,State,ID,OpName2,ConstID2,State2,ID2]),
554		fail.
555		ahc.
556
557		:- use_module(probsrc(translate),[translate_bstate_limited/2, translate_event_with_limit/3]).
558		:- use_module(probsrc(debug),[debug_mode/1]).
559		:- use_module(probsrc(preferences),[get_preference/2]).
560		:- use_module(probsrc(specfile),[get_operation_name/2]).
561		get_op_name(Nr,check_invariant_violated(Nr)) :- number(Nr),!.
562		get_op_name(Op,OpName) :- get_operation_name(Op,OpName).
563		get_nr_next_state_calls(OpName,Nr) :- findall(1,operation_computed(_Hash,OpName,_,_,_ID),Ls), length(Ls,Nr).
564		get_nr_cache_results(OpName,RNr) :-
565		findall(1,(operation_cached_results(_ID,Op,_,_),get_op_name(Op,OpName)),Rs), length(Rs,RNr).
566		:- use_module(probsrc(bmachine),[b_get_machine_variables/1]).
567		% b_operation_cache:print_op_cache_profile
568
569		check_if_op_cache_useful :-
570		b_get_machine_variables(Var),length(Var,VLen),
571		api_get_operation_read_write_info(OpName,ReadVariables,_ReadConstants,_WrittenVariables),
572		length(ReadVariables,ReadLen),
573		ReadLen < VLen,
574		(inv_op_name(OpName) -> get_preference(use_po,false) ; true),
575		format('Operation reuse potentially useful: ~w reads ~w/~w variables~n',[OpName,ReadLen,VLen]),
576		fail.
577		check_if_op_cache_useful.
578
579		inv_op_name(check_invariant_violated(_)).
580
581		print_op_cache_profile :- \+ operation_computed(_,_,_,_,_),!, % print nothing
582		(get_preference(try_operation_reuse,false) -> format('OPERATION_REUSE preference not set to TRUE~n',[]) ; true),
583		format('No operation cached~n',[]),
584		check_if_op_cache_useful.
585		print_op_cache_profile :-
586		b_get_machine_variables(Var),length(Var,VLen),
587		operation_read_projection_cache(OpKey,OpName,ProjVars,_,WV), (ProjVars = [] ; ProjVars = [_|_]),
588		length(ProjVars,Len),
589		operation_read_constants(OpKey,ReadConstants),
590		(operation_guard_read_info(OpKey,_,IrrelevantVars)
591		-> format('Operation ~w cached onto ~w/~w variables: ~w (not relevant for guard: ~w, only written: ~w, constants read: ~w)~n',[OpName,Len,VLen,ProjVars,IrrelevantVars,WV,ReadConstants])
592		; format('Operation ~w cached onto ~w/~w variables: ~w (only written: ~w, constants read: ~w)~n',[OpName,Len,VLen,ProjVars,WV,ReadConstants])
593		),fail.
594		print_op_cache_profile :- findall(OpName,operation_read_projection_cache(_,OpName,no_caching,_,_),Ls),
595		format('Operations not cached: ~w~n',[Ls]),fail.
596		print_op_cache_profile :- operation_read_projection_cache(OpKey,OpName,ProjVars,_,_), ProjVars = [_|_],
597		get_nr_next_state_calls(OpName,Nr),
598		get_nr_cache_results(OpName,RNr),
599		(inv_op_name(OpName) -> Results='violations' ; Results = 'results'),
600		format('Next-state-calls for ~w: ~w (~w ~w)~n',[OpName,Nr,RNr,Results]),
601		operation_guard_read_info(OpKey,RelVars,_),
602		findall(1,op_guard_fails(_,OpName,_),Fails), length(Fails,NrFails),
603		format(' projected-failures (on ~w): ~w~n',[RelVars,NrFails]),
604		fail.
605		print_op_cache_profile :-
606		get_total_number_of_next_state_calls(Nr,InvNr),
607		format('Total Number of Next-state-calls for Operations: ~w~n',[Nr]),
608		get_counter(op_cached_failures,FailCalls),
609		format(' - Reused guard failures: ~w~n',[FailCalls]),
610		get_counter(op_cached_successes,SuccCalls),
611		format(' - Reused successful operation call results: ~w~n',[SuccCalls]),
612		format('Total Number of Invariant-check-calls: ~w~n',[InvNr]),
613		get_counter(inv_cached_successes,SuccInvCalls),
614		format(' - Reused invariant check results: ~w~n',[SuccInvCalls]),
615		get_counter(op_cached_errors,Errs),
616		format('Errors during calls: ~w~n',[Errs]),
617		get_counter(op_cached_timeouts,Timeouts),
618		format('Timeouts during calls: ~w~n',[Timeouts]),
619		get_counter(op_cached_enum_warnings,EnumWarns),
620		format('Enumeration warnings during calls: ~w~n',[EnumWarns]),
621		fail.
622		print_op_cache_profile :- debug_mode(on), nl,
623		operation_read_projection_cache(_,OpName,Skel,_,_),
624		format('~n** Local Operation Cache Info for ~w ** (projected on ~w):~n',[OpName,Skel]),
625		operation_computed(_Hash,OpName,ConstID,PackedValList,ID),
626		(operation_cached_max_reached(ID,OpName) -> MaxR='(max reached, not all transitions computed)'
627		; MaxR=''),
628		format('~nNode ID = ~w, Operation = ~w ~w~n',[ID,OpName,MaxR]),
629		unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,NodeDesc),
630		format(' projected state : (ConstID ~w) ~w~n',[ConstID,NodeDesc]),
631		operation_cached_results(ID,Operation,PackedNewState,_PathInfo),
632		translate_event_with_limit(Operation,100,OpStr),
633		unpack_values(PackedNewState,NewState), translate:translate_bstate_limited(NewState,UpdateStr),
634		format(' ~w -upd-> ~w~n',[OpStr,UpdateStr]),
635		fail.
636		print_op_cache_profile :- print_violated_invariants,fail.
637		print_op_cache_profile :- ahc,print('----------'),nl.
638
639		get_total_number_of_next_state_calls(OpNr,InvNr) :-
640		get_counter(op_cache_id,TotNr),
641		get_counter(inv_cache_nr,InvNr),
642		OpNr is TotNr-InvNr.
643		%findall(0,b_operation_cache:operation_computed(_Hash,_Op,_,_,_ID),Ls), length(Ls,Nr).
644
645		get_op_cache_stats([next_state_calls-NrN, % actual calls to the B interpreter to compute next state
646		operations_cached-NrC, % number of operations whose calls are cached
647		invariants_cached-NrI, % number of invariants whose evaluation is cached
648		next_state_guard_failures-NrFails, % number of next-state_call failures stored (disabled operation)
649		reused_next_state_calls-SuccCalls,
650		reused_next_state_failures-FailCalls,
651		inv_check_calls-InvNr, % actual calls to check individual invariants in a state
652		reused_inv_check_calls-SuccInvCalls
653		]) :-
654		findall(OpKey,(operation_read_projection_cache(OpKey,OpName,_,_,_),atomic(OpName)),OK1),
655		length(OK1,NrC),
656		findall(OpKey,invariant_op_key(OpKey,_),OK2),
657		length(OK2,NrI),
658		findall(OpKey,(op_guard_fails(OpKey,_,_)),OK3),
659		length(OK3,NrFails),
660		get_total_number_of_next_state_calls(NrN,InvNr),
661		get_counter(op_cached_failures,FailCalls),
662		get_counter(op_cached_successes,SuccCalls),
663		get_counter(inv_cached_successes,SuccInvCalls).
664
665		% ----------------------
666
667		:- use_module(probsrc(tools_strings),[ajoin/2]).
668		tcltk_op_cache_stats(list([list(['Operation','#Next-State', '#Results',
669		'# Proj.Vars','Proj.Vars', 'ReadCsts', 'OnlyWritten'])|SEntries])) :-
670		%b_get_machine_variables(Var),length(Var,VLen),
671		findall(list([OP,NrCalls,RNr,NrProjVars,ProjVars,ReadConstants,AdditionalOutVars]),
672		(operation_read_projection_cache(OpKey,OpName,ProjVars,_,AdditionalOutVars),
673		(OpName = check_invariant_violated(Nr) -> ajoin(['Invariant',Nr],OP) ; OP=OpName),
674		length(ProjVars,NrProjVars),
675		operation_read_constants(OpKey,ReadConstants),
676		get_nr_next_state_calls(OpName,NrCalls),
677		get_nr_cache_results(OpName,RNr)
678		), Entries), sort(Entries,SEntries).
679
680		% ----------------------
681		% DOT RENDERING (not yet finished)
682
683		%op_cache_node(ID,OpName,NodeDesc,Shape,Style,Color) :- Shape=box, Style=solid, Color=blue,
684		% operation_computed(_Hash,OpName,_,PackedState,ID),
685		% unpack_values(PackedState,State), translate_bstate_limited(State,NodeDesc).
686		%:- use_module(probsrc(dotsrc(dot_graph_generator)),[gen_dot_graph/3]).
687		% Predicates for creating a dependency graph
688		%tcltk_operation_cache_graph(File) :- gen_dot_graph(File,op_cache_node,cbc_dependence_trans_predicate).
689