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