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