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) -> add_warning(b_operation_cache,'Error scope not fresh:',E) ; true),
185	?	call_cleanup(
186		com_op_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,Done),
187		(get_mutable(still_computing,Done)
188		-> format('Timeout, exception or virtual timeout occured during caching for ~w (cache id ~w)~n',[OpName,NewID]),
189		% also happens during -execute due to cut!, hence we now disable preference in -execute
190		% stop_ms_timer_with_msg(Timer,'Runtime for computing'),
191		register_op_cache_time_out(NewID,OpName)
192		; error_occurred_in_error_scope
193		-> format('Error occurred during caching for ~w (cache id ~w)~n',[OpName,NewID]),
194		invalidate_operation_cache(NewID,OpName)
195		; event_occurred_in_error_scope(Event),
196		format('Enumeration warning occurred during caching for ~w (cache id ~w)~n',[OpName,NewID]),
197		register_op_cache_enum_warning(NewID,OpName,Event),
198		fail
199		% TODO: should we also check if errors occured
200		; true
201		)),
202		get_mutable(DVal,Done), DVal \= finished. % fail if we are Done;
203
204		% we could do this: but we don't know if an exception, timeout or virtual time_out occurred
205		register_op_cache_time_out(ID,OpName) :-
206		inc_counter(op_cached_timeouts),
207		assertz(operation_cached_time_out(ID,OpName)).
208		register_op_cache_enum_warning(ID,OpName,Event) :-
209		inc_counter(op_cached_enum_warnings),
210		assertz(operation_cached_enum_warning(ID,OpName,Event)).
211		% as an alternative this removes the cached results:
212		invalidate_operation_cache(ID,OpName) :-
213		inc_counter(op_cached_errors),
214		retractall(operation_cached_results(ID,_Operation,_,_)),
215		retractall(operation_computed(_,OpName,_,_,ID)). % can be expensive
216
217
218
219		com_op_update_max(_,check_invariant_violated(Nr),Operation,ProjState,NewState,PathInfo,_,Done) :- !,
220		NewState =[], PathInfo=invariant, Operation=Nr, % values not used anyway for invariants
221		%print(check_invariant(Nr)),nl, bmachine:b_nth1_invariant(Nr,Inv,_UsedIds), translate:print_bexpr(Inv),nl,
222		(b_interpreter:check_nth1_invariant(Nr,ProjState )
223		-> update_mutable(finished,Done) % will lead to failure above; we store only violations
224		; % invariant violation found
225		update_mutable(last_sol_found,Done)
226		).
227		com_op_update_max(_,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,_) :-
228		% for CSP||B: clear out any parameters; otherwise we also need to hash the parameters
229		reset_max_reached(OpName),
230	?	succeed_max_call_id(OpName,
231		b_execute_top_level_operation_update(OpName,Operation,ProjInOutState,NewState,PathInfo),
232		MaxForCall).
233		% TO DO: normalise_store out state values, to avoid re-normalising when storing updates
234		com_op_update_max(NewID,OpName,_,_,_,_,_,Done) :-
235		(NewID \= uncached,
236		max_reached(OpName)
237		-> assertz(operation_cached_max_reached(NewID,OpName)) % store that we reached max. nr of transitions for this node
238		; true %format('No Timeout or virtual timeout occurred during caching for ~w leading to ~w~n',[OpName,NewID])
239		),
240		update_mutable(finished,Done).
241
242
243
244		% entry point to cache invariant checking
245		check_invariant_violated_cache(Nr,State) :-
246		%get_store_and_info(State,FullStore,Infos),
247	?	compute_operation_on_expanded_store_cache(check_invariant_violated(Nr),_,State,_,_,-1).
248
249		:- use_module(probsrc(specfile),[expand_const_and_vars_to_full_store/2]).
250		%get_store_and_info(expanded_const_and_vars(_ConstID,_Vars,E,Info),FullStore,Info) :- !, FullStore=E.
251		%get_store_and_info(expanded_vars(E,Info),FullStore,Info) :- !, FullStore=E.
252		%get_store_and_info(Store,FullStore,[]) :- expand_const_and_vars_to_full_store(Store,FullStore).
253
254		% -------------------------------
255
256
257		% check if caching is worthwhile for this operation
258		%worthwhile_to_cache(OpName) :-
259		% get_read_write_info(OpName,ReadVariables,WrittenVariables),
260		% length(ReadVariables,NrRV),
261		% bmachine:b_machine_statistics(variables,NrVars),
262		% bmachine:b_machine_statistics(constants,NrConstants),
263		% Perc is (NrRV*100) // (NrVars+NrConstants),
264		% length(WrittenVariables,NrWV),
265		% 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]),
266		% Perc < 95. % maybe provide as preference
267
268		:- use_module(library(ordsets),[ord_member/2]).
269		%is_read(ReadVariables,bind(Var,_)) :- ord_member(Var,ReadVariables).
270		member_ord(List,X) :- ord_member(X,List). % for maplist, exclude,...
271
272		% -------------------------------
273
274		% a variation of split_list which also returns a list of predicate results
275		% with re_project_state(L,ProjVarsInOrder,A) : we can split another list using the same pattern
276
277		:- assert_must_succeed((b_operation_cache:project_state_onto_vars([bind(x,1),bind(y,2),bind(b,3)],[b,y],
278		ProjVars,ProjState,0,NrDel),
279		ProjVars == [y,b], ProjState == [bind(y,2),bind(b,3)], NrDel==1)).
280
281		project_state_onto_vars([],_,[],[],Acc,Acc).
282		project_state_onto_vars([Elem|Rest],ReadVariables,ProjVars,ProjState,NrDelAcc,NrDel) :-
283		Elem = bind(Var,_),
284		(ord_member(Var,ReadVariables) % TO DO: we could improve performance by sorting Elements
285		-> ProjVars=[Var|PT], ProjState=[Elem|AR], ND1=NrDelAcc
286		; ProjVars=PT, ProjState=AR, ND1 is NrDelAcc+1),
287		project_state_onto_vars(Rest,ReadVariables,PT,AR,ND1,NrDel).
288
289
290		% -------------------------------
291
292		:- assert_must_succeed((b_operation_cache:re_project_state([y,b],[bind(x,1),bind(y,2),bind(b,3)],Res),
293		Res == [bind(y,2),bind(b,3)])).
294
295		% project state(VarsInOrder,State,ProjectedState)
296		% faster than project_state_onto_vars
297		re_project_state([],_,[]).
298		re_project_state([VarToProject|PT],[Elem|Rest],A) :-
299		arg(1,Elem,Var), %Elem = bind(Var,_),
300		(VarToProject==Var
301		-> A=[Elem|AR],re_project_state(PT,Rest,AR)
302		; re_project_state2(VarToProject,PT,Rest,A)).
303
304		re_project_state2(VarToProject,PT,[Elem|Rest],A) :-
305		arg(1,Elem,Var), %Elem = bind(Var,_),
306		(VarToProject==Var
307		-> A=[Elem|AR],re_project_state(PT,Rest,AR)
308		; re_project_state2(VarToProject,PT,Rest,A)).
309
310		% -----------------------------
311
312		% Two utilities to optionally generate lemma facts for fast projection
313		% Does not seem to be worth it
314
315		% abstract away values, can be used to generate pre-compiled facts
316		%abstract_state([],[]).
317		%abstract_state([bind(Var,_)|T],[bind(Var,_)|AT]) :- abstract_state(T,AT).
318
319		% abstract away unused bindings, can be used to generate pre-compiled facts
320		%clear_unused_bindings([],_,_) :- !.
321		%clear_unused_bindings([VarToProject|PT],[bind(Var,V)|T],[bind(Var,V)|RT]) :-
322		% % we could clear out Variable name Var; but this creates a danger of successfully matching an erroneous state
323		% VarToProject==Var,!,
324		% clear_unused_bindings(PT,T,RT).
325		%clear_unused_bindings(Vars,[_|T],[_|RT]) :- % leave slot in result as fresh var
326		% clear_unused_bindings(Vars,T,RT).
327
328		% -------------------------------
329
330		:- use_module(probsrc(hashing)).
331		:- use_module(probsrc(state_packing)).
332
333		:- dynamic operation_computed/5, operation_cached_results/4,
334		operation_cached_max_reached/2, operation_cached_time_out/2, operation_cached_enum_warning/3,
335		op_guard_fails/3.
336
337		% return Hash and check if operation computed
338		% TO DO: do not hash constants if single value exists ?
339		check_if_operation_was_computed(OpName,ConstID,State,Skel,Infos,PackedValList,IsReadingCsts,
340		HashConstID,Hash,Res) :-
341		(Infos = [packed_state/PS|_]
342		-> get_packed_vars(PS,OpName,PackedState),
343		remove_bind_skeleton(PackedState,Skel,PackedValList)
344		% packing already performed in prepare_state_for_specfile_trans
345		; write(no_packed_state_info(OpName,ConstID)),nl, % shouldn't happen hopefully
346		project_in_state(State,OpName,ProjectedInState), % State contains just variables
347		pack_bind_list(ProjectedInState,Skel,PackedValList)
348		),
349		(IsReadingCsts = false -> HashConstID=root ; HashConstID=ConstID),
350		op_hash(OpName,HashConstID,PackedValList,Hash),
351		(operation_computed(Hash,OpName,HashConstID,PackedValList,ID)
352		-> Res = ID
353		; % operation_guard_read_info(OpKey,GuardVars,_), re_project_state(GuardVars,Skel,PackedValList,GuardPackedVals)
354		% op_hash(OpName,HashConstID,GuardPackedVals,GuardHash), op_guard_fails(GuardHash,OpName,GuardPackedVals,ID) -> true
355		Res= false).
356
357		% project a state or packed value list onto the variables relevant for the guard (if it is a subset)
358		project_onto_guard(OpName,OpKey,HashConstID,Skel,PackedValList,GuardPackedVals,GuardHash) :-
359		operation_guard_read_info(OpKey,_,IgnoredVars),
360	?	remove_ignored_vars(IgnoredVars,Skel,PackedValList,GuardPackedVals),
361		op_hash(OpName,HashConstID,GuardPackedVals,GuardHash).
362
363
364		% remove_ignored_vars(VarsToIgnore,SkeletonList,ValueList,Result)
365		remove_ignored_vars([],_,PackedVals,Res) :- Res=PackedVals.
366		remove_ignored_vars([ID|T],[ID|ST],[_|PackedVals],GuardPackedVals) :- !,
367	?	remove_ignored_vars(T,ST,PackedVals,GuardPackedVals).
368		remove_ignored_vars(Ignored,[_|ST],[PV|PackedVals],[PV|GuardPackedVals]) :-
369	?	remove_ignored_vars(Ignored,ST,PackedVals,GuardPackedVals).
370
371		get_packed_vars(const_and_vars(_,Vars),OpName,PackedVars) :- !, project_in_state(Vars,OpName,PackedVars).
372		get_packed_vars(PS,OpName,PackedVars) :- !, project_in_state(PS,OpName,PackedVars).
373		:- use_module(library(terms),[term_hash/3]).
374		:- use_module(probsrc(hashing),[my_term_hash/2]).
375
376		op_hash(OpName,HashConstID,PackedValList,Hash) :- get_preference(use_state_packing,false),!,
377		my_term_hash((OpName,HashConstID,PackedValList),Hash). % will user super_hash
378		op_hash(OpName,HashConstID,PackedValList,Hash) :-
379		% 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
380		term_hash((OpName,HashConstID,PackedValList),
381		[range(smallint),algorithm(sdbm),depth(infinite),if_var(ignore)], % djb2
382		Hash).
383
384
385		% remove bind/2 wrappers and variable name for faster hashing
386		remove_bind_skeleton([],[],R) :- !, R=[].
387		remove_bind_skeleton([bind(Var,Val)|T],[Var|VT],[Val|RT]) :- !,
388		remove_bind_skeleton(T,VT,RT).
389		remove_bind_skeleton(L,V,R) :- add_internal_error('Illegal store: ',remove_bind_skeleton(L,V,R)), R=L.
390
391		% we could also peel a few infos not useful for hashing:
392		%peel_val('$stored_avl_packed'(Nr),Nr).
393		%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
394
395
396		get_new_operation_computed_id(OpName,ConstID,PackedValList,Hash,ID) :-
397		inc_counter(op_cache_id,ID),
398		(OpName=check_invariant_violated(_) -> inc_counter(inv_cache_nr,_) ; true),
399		assertz(operation_computed(Hash,OpName,ConstID,PackedValList,ID)).
400		% To reduce memory consumption we could use the following clause:
401		% can be useful if there are many operations with a large number of projected variables
402		% but does lead to noticable slowdown when looking up operations
403		%get_new_operation_computed_id(OpName,ConstID,_PackedValList,Hash,[_,state_id/ReferenceStateID],ID) :- !,
404		% inc_counter(op_cache_id,ID),
405		% assertz(operation_computed(Hash,OpName,ConstID,ReferenceStateID,ID)). % storing reference ID preserves memory
406		% when looking up operation_was_computed we would need to do something like:
407		% state_space:packed_visited_expression(StoredState,PS),
408		% get_packed_b_state_with_uncompressed_lists(PS,PUS),
409		% get_state_infos(PUS,ConstID,PackedList,_,_),
410		% project_in_state(PackedList,OpName,ProjectedStoredState),
411		% remove_bind_skeleton(ProjectedStoredState,Skel,ProjectedValList),
412		% ProjectedValList = PackedValList
413
414
415		:- use_module(probsrc(runtime_profiler),[profile_failure_driven_loop/1]).
416		% this is used when get_preference(try_operation_reuse,true/full)
417		% it is only called for operations, not for setup_constants or initalise_machine
418
419		% treat expanded_const_and_vars(ConstID,Vars,FullStore,Infos)
420
421		get_state_infos(expanded_const_and_vars(ID,Vars,FullStore,I),ConstID,Vars,FullStore,Infos) :- !,ConstID=ID,Infos=I.
422		get_state_infos(expanded_vars(V,I),ConstID,Vars,FullStore,Infos) :- !, ConstID=root,Vars=V,FullStore=V,Infos=I.
423		get_state_infos(const_and_vars(ConstID,Vars),ConstID,Vars,FullStore,Infos) :- !,
424		add_warning(get_state_infos,'State not prepared for caching: ',const_and_vars(ConstID,Vars)),
425		Infos=[],
426		expand_const_and_vars_to_full_store(const_and_vars(ConstID,Vars),FullStore).
427		get_state_infos(csp_and_b(_,State),ConstID,Vars,FullStore,Infos) :- !,
428		get_state_infos(State,ConstID,Vars,FullStore,Infos).
429		get_state_infos(Vars,unknown,Vars,Vars,[]).
430
431		% InState is either already an expanded list or expanded_const_and_vars, expanded_vars
432		compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :-
433		get_state_infos(InState,ConstID,Vars,FullStore,Infos), % extract infos from the store
434		% TO DO: check if state_id in Infos and if OpName in equivalence class with same proj. vars
435		get_opname_key(OpName,OpNameKey),
436		get_operation_read_projection_infos(OpNameKey,OpName,Vars,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars),
437		!,
438		% tools_printing:print_term_summary(proj(OpName,ConstID,ProjInState,FullStore)),nl,
439		check_if_operation_was_computed(OpName,ConstID,Vars,ProjVarsInOrder,Infos,PackedValList,IsReadingCsts,
440		HashConstID,Hash,ID),
441		(ID \= false
442		-> % we can reuse the stored operation effect
443		%print('+'),
444		%hit_profiler:add_hit(operation_reused,OpName),
445		(inv_op_name(OpName) -> inc_counter(inv_cached_successes)
446		; inc_counter(op_cached_successes)),
447	?	(operation_cached_results(ID,Operation,PackedNewState,PathInfo),
448		unpack_values(PackedNewState,NewState)
449		; operation_cached_max_reached(ID,OpName), % we did not compute all operations
450		assert_max_reached(OpName),
451		fail
452	?	; operation_cached_enum_warning(ID,OpName,Event),
453		format('Regenerating enumeration warning for ~w and cache id ~w~n',[OpName,ID]),
454		add_new_event_in_error_scope(Event),
455		fail
456		; operation_cached_time_out(ID,OpName),
457		format('Rethrowing cached time_out for ~w and cache id ~w~n',[OpName,ID]),
458		throw(time_out)
459		)
460		; % we have not computed solutions for this operation for this projected state
461	?	(project_onto_guard(OpName,OpNameKey,HashConstID,ProjVarsInOrder,PackedValList,GuardPackedVals,GuardHash)
462		-> true
463		; GuardPackedVals = none),
464		(nonvar(GuardHash),
465		op_guard_fails(GuardHash,OpName,GuardPackedVals)
466		-> % we did already compute this operation for this projected state and it failed
467		inc_counter(op_cached_failures),
468		fail % the guard is guaranteed to fail
469		; % we have not yet computed this operation; compute it and store solutions as we go
470		get_new_operation_computed_id(OpName,HashConstID,PackedValList,Hash,NewID),
471		%print('-'),
472		%hit_profiler:add_hit(operation_cache_computation,OpName),
473		(IsReadingCsts=false
474		-> % TO DO: check if this projection is worthwhile
475		project_in_state_for_opname_key(Vars,OpNameKey,ProjInState),
476		% Note: if no packed_state this projection was already performed in check_if_operation_was_computed
477		add_new_vars(AdditionalOutVars,ProjInState,ProjInOutState)
478		; ProjInOutState = FullStore % use full store with constants
479		),
480		profile_failure_driven_loop(OpName),
481	?	if(api_compute_operation_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall),
482		(% Normalise here or in update_max
483		pack_values(NewState,PackedNewState),
484		(PathInfo=invariant -> StoredPathInfo=Hash
485		; filter_transition_path_info(PathInfo,StoredPathInfo)),
486		assertz(operation_cached_results(NewID,Operation,PackedNewState,StoredPathInfo))
487		),
488		(nonvar(GuardHash),
489		%print(op_guard_fails(GuardHash,OpName,GuardPackedVals)),nl,
490		assertz(op_guard_fails(GuardHash,OpName,GuardPackedVals)),
491		fail
492		)
493		)
494		)
495		% TO DO: if we have no successors for ID and if the operation reads less IDs in the guard
496		% we can replace remaining identifier values by a variable
497		).
498		compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :-
499		%hit_profiler:add_hit(operation_not_cached,OpName),
500		% operation is not cached
501		get_state_infos(InState,_,_,FullStore,_),
502	?	api_compute_operation_update_max(uncached,OpName,Operation,FullStore,NewState,PathInfo,MaxForCall).
503
504		% add written vars which are not read virtually to state to avoid error messages in store_intermediate_updates:
505		add_new_vars([],S,S).
506		add_new_vars([WrittenVar|T],State,[bind(WrittenVar,term(undefined))|ST]) :-
507		add_new_vars(T,State,ST).
508
509		:- use_module(probsrc(state_space),[keep_transition_info/1]).
510		filter_transition_path_info([],R) :- !, R=[].
511		filter_transition_path_info([H|T],Res) :- !,
512		(keep_transition_info(H) -> Res = [H|RT]
513		; Res=RT), % by default we filter out possibly large path infos (in particular for Event-B)
514		filter_transition_path_info(T,RT).
515		filter_transition_path_info(H,Res) :-
516		(keep_transition_info(H) -> Res = H ; Res=[]).
517
518
519	?	invariant_op_key(OpKey,InvNr) :- operation_read_projection_cache(OpKey,check_invariant_violated(InvNr),_,_,_).
520
521		:- use_module(probsrc(bmachine),[b_nth1_invariant/3]).
522		print_violated_invariants :-
523		operation_cached_results(ID,Nr,[],Hash),number(Nr),
524		b_nth1_invariant(Nr,Invariant,_UsedIds),
525		format('Invariant ~w violated (op-cache-id ~w)~n ',[Nr,ID]),
526		translate:print_bexpr(Invariant),nl,
527		% now try and recover state where it was violated:
528		operation_computed(Hash,OpName,ConstID,PackedValList,ID),
529		operation_read_projection_cache(_,OpName,Skel,_,_),
530		unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,StateDesc),
531		format(' in state (ConstID ~w) ~w~n',[ConstID,StateDesc]),
532		fail.
533		print_violated_invariants.
534
535		% small utility code to analyze hash collisions:
536		% b_operation_cache:ahc.
537		:- public ahc/0.
538	?	ahc :- operation_computed(Hash,OpName,ConstID,State,ID),
539		operation_computed(Hash,OpName2,ConstID2,State2,ID2),
540		(ConstID @> ConstID2 -> true ; ConstID=ConstID2, ID2 > ID),
541		format('Hash collision: ~w~n ~w:~w:~w:~w~n ~w:~w:~w:~w~n~n',
542		[Hash,OpName,ConstID,State,ID,OpName2,ConstID2,State2,ID2]),
543		fail.
544		ahc.
545
546		:- use_module(probsrc(translate),[translate_bstate_limited/2, translate_event_with_limit/3]).
547		:- use_module(probsrc(debug),[debug_mode/1]).
548		:- use_module(probsrc(preferences),[get_preference/2]).
549		:- use_module(probsrc(specfile),[get_operation_name/2]).
550		get_op_name(Nr,check_invariant_violated(Nr)) :- number(Nr),!.
551		get_op_name(Op,OpName) :- get_operation_name(Op,OpName).
552		get_nr_next_state_calls(OpName,Nr) :- findall(1,operation_computed(_Hash,OpName,_,_,_ID),Ls), length(Ls,Nr).
553		get_nr_cache_results(OpName,RNr) :-
554		findall(1,(operation_cached_results(_ID,Op,_,_),get_op_name(Op,OpName)),Rs), length(Rs,RNr).
555		:- use_module(probsrc(bmachine),[b_get_machine_variables/1]).
556		% b_operation_cache:print_op_cache_profile
557
558		check_if_op_cache_useful :-
559		b_get_machine_variables(Var),length(Var,VLen),
560		api_get_operation_read_write_info(OpName,ReadVariables,_ReadConstants,_WrittenVariables),
561		length(ReadVariables,ReadLen),
562		ReadLen < VLen,
563		(inv_op_name(OpName) -> get_preference(use_po,false) ; true),
564		format('Operation reuse potentially useful: ~w reads ~w/~w variables~n',[OpName,ReadLen,VLen]),
565		fail.
566		check_if_op_cache_useful.
567
568		inv_op_name(check_invariant_violated(_)).
569
570	?	print_op_cache_profile :- \+ operation_computed(_,_,_,_,_),!, % print nothing
571		(get_preference(try_operation_reuse,false) -> format('OPERATION_REUSE preference not set to TRUE~n',[]) ; true),
572		format('No operation cached~n',[]),
573		check_if_op_cache_useful.
574		print_op_cache_profile :-
575		b_get_machine_variables(Var),length(Var,VLen),
576	?	operation_read_projection_cache(OpKey,OpName,ProjVars,_,WV), (ProjVars = [] ; ProjVars = [_|_]),
577		length(ProjVars,Len),
578		operation_read_constants(OpKey,ReadConstants),
579		(operation_guard_read_info(OpKey,_,IrrelevantVars)
580		-> 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])
581		; format('Operation ~w cached onto ~w/~w variables: ~w (only written: ~w, constants read: ~w)~n',[OpName,Len,VLen,ProjVars,WV,ReadConstants])
582		),fail.
583		print_op_cache_profile :- findall(OpName,operation_read_projection_cache(_,OpName,no_caching,_,_),Ls),
584		format('Operations not cached: ~w~n',[Ls]),fail.
585	?	print_op_cache_profile :- operation_read_projection_cache(OpKey,OpName,ProjVars,_,_), ProjVars = [_|_],
586		get_nr_next_state_calls(OpName,Nr),
587		get_nr_cache_results(OpName,RNr),
588		(inv_op_name(OpName) -> Results='violations' ; Results = 'results'),
589		format('Next-state-calls for ~w: ~w (~w ~w)~n',[OpName,Nr,RNr,Results]),
590		operation_guard_read_info(OpKey,RelVars,_),
591		findall(1,op_guard_fails(_,OpName,_),Fails), length(Fails,NrFails),
592		format(' projected-failures (on ~w): ~w~n',[RelVars,NrFails]),
593		fail.
594		print_op_cache_profile :-
595		get_total_number_of_next_state_calls(Nr,InvNr),
596		format('Total Number of Next-state-calls for Operations: ~w~n',[Nr]),
597		get_counter(op_cached_failures,FailCalls),
598		format(' - Reused guard failures: ~w~n',[FailCalls]),
599		get_counter(op_cached_successes,SuccCalls),
600		format(' - Reused successful operation call results: ~w~n',[SuccCalls]),
601		format('Total Number of Invariant-check-calls: ~w~n',[InvNr]),
602		get_counter(inv_cached_successes,SuccInvCalls),
603		format(' - Reused invariant check results: ~w~n',[SuccInvCalls]),
604		get_counter(op_cached_errors,Errs),
605		format('Errors during calls: ~w~n',[Errs]),
606		get_counter(op_cached_timeouts,Timeouts),
607		format('Timeouts during calls: ~w~n',[Timeouts]),
608		get_counter(op_cached_enum_warnings,EnumWarns),
609		format('Enumeration warnings during calls: ~w~n',[EnumWarns]),
610		fail.
611		print_op_cache_profile :- debug_mode(on), nl,
612		operation_read_projection_cache(_,OpName,Skel,_,_),
613		format('~n** Local Operation Cache Info for ~w ** (projected on ~w):~n',[OpName,Skel]),
614		operation_computed(_Hash,OpName,ConstID,PackedValList,ID),
615		(operation_cached_max_reached(ID,OpName) -> MaxR='(max reached, not all transitions computed)'
616		; MaxR=''),
617		format('~nNode ID = ~w, Operation = ~w ~w~n',[ID,OpName,MaxR]),
618		unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,NodeDesc),
619		format(' projected state : (ConstID ~w) ~w~n',[ConstID,NodeDesc]),
620		operation_cached_results(ID,Operation,PackedNewState,_PathInfo),
621		translate_event_with_limit(Operation,100,OpStr),
622		unpack_values(PackedNewState,NewState), translate:translate_bstate_limited(NewState,UpdateStr),
623		format(' ~w -upd-> ~w~n',[OpStr,UpdateStr]),
624		fail.
625		print_op_cache_profile :- print_violated_invariants,fail.
626		print_op_cache_profile :- ahc,print('----------'),nl.
627
628		get_total_number_of_next_state_calls(OpNr,InvNr) :-
629		get_counter(op_cache_id,TotNr),
630		get_counter(inv_cache_nr,InvNr),
631		OpNr is TotNr-InvNr.
632		%findall(0,b_operation_cache:operation_computed(_Hash,_Op,_,_,_ID),Ls), length(Ls,Nr).
633
634		get_op_cache_stats([next_state_calls-NrN, % actual calls to the B interpreter to compute next state
635		operations_cached-NrC, % number of operations whose calls are cached
636		invariants_cached-NrI, % number of invariants whose evaluation is cached
637		next_state_guard_failures-NrFails, % number of next-state_call failures stored (disabled operation)
638		reused_next_state_calls-SuccCalls,
639		reused_next_state_failures-FailCalls,
640		inv_check_calls-InvNr, % actual calls to check individual invariants in a state
641		reused_inv_check_calls-SuccInvCalls
642		]) :-
643		findall(OpKey,(operation_read_projection_cache(OpKey,OpName,_,_,_),atomic(OpName)),OK1),
644		length(OK1,NrC),
645		findall(OpKey,invariant_op_key(OpKey,_),OK2),
646		length(OK2,NrI),
647		findall(OpKey,(op_guard_fails(OpKey,_,_)),OK3),
648		length(OK3,NrFails),
649		get_total_number_of_next_state_calls(NrN,InvNr),
650		get_counter(op_cached_failures,FailCalls),
651		get_counter(op_cached_successes,SuccCalls),
652		get_counter(inv_cached_successes,SuccInvCalls).
653
654		% ----------------------
655
656		:- use_module(probsrc(tools_strings),[ajoin/2]).
657		tcltk_op_cache_stats(list([list(['Operation','#Next-State', '#Results',
658		'# Proj.Vars','Proj.Vars', 'ReadCsts', 'OnlyWritten'])|SEntries])) :-
659		%b_get_machine_variables(Var),length(Var,VLen),
660		findall(list([OP,NrCalls,RNr,NrProjVars,ProjVars,ReadConstants,AdditionalOutVars]),
661		(operation_read_projection_cache(OpKey,OpName,ProjVars,_,AdditionalOutVars),
662		(OpName = check_invariant_violated(Nr) -> ajoin(['Invariant',Nr],OP) ; OP=OpName),
663		length(ProjVars,NrProjVars),
664		operation_read_constants(OpKey,ReadConstants),
665		get_nr_next_state_calls(OpName,NrCalls),
666		get_nr_cache_results(OpName,RNr)
667		), Entries), sort(Entries,SEntries).
668
669		% ----------------------
670		% DOT RENDERING (not yet finished)
671
672		%op_cache_node(ID,OpName,NodeDesc,Shape,Style,Color) :- Shape=box, Style=solid, Color=blue,
673		% operation_computed(_Hash,OpName,_,PackedState,ID),
674		% unpack_values(PackedState,State), translate_bstate_limited(State,NodeDesc).
675		%:- use_module(probsrc(dotsrc(dot_graph_generator)),[gen_dot_graph/3]).
676		% Predicates for creating a dependency graph
677		%tcltk_operation_cache_graph(File) :- gen_dot_graph(File,op_cache_node,cbc_dependence_trans_predicate).
678