1		% (c) 2009-2023 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(coverage_statistics,[tcltk_compute_coverage/1, tcltk_compute_coverage_and_enabling/1,
6		tcltk_compute_coverage_and_degree/1,
7		tcltk_compute_min_max/1,
8		pretty_print_min_max_coverage_to_file/1,
9		compute_the_coverage/5,pretty_print_coverage_information_to_file/1,
10		operation_hit/2,query_node_hit/2, uncovered_operation/1,
11		tcltk_analyse_constants/2, tcltk_analyse_constants/1]).
12
13
14		:- use_module(probsrc(module_information)).
15		:- module_info(group,misc).
16		:- module_info(description,'This module is responsible for computing state space coverage info.').
17
18		:- use_module(probsrc(state_space)).
19		:- use_module(probsrc(tools)).
20		:- use_module(probsrc(debug),[debug_println/2, debug_format/3]).
21		:- use_module(probsrc(error_manager),[add_message/4, add_message/3, add_debug_message/4, add_debug_message/3]).
22		:- use_module(probsrc(tools_lists), [length_less/2]).
23		/* --------------------------------------------------- */
24
25		:- use_module(probsrc(state_space),[current_state_id/1,
26		get_constants_state_for_id/2, try_get_unique_constants_state/1]).
27
28		% provide information about the constants
29		% can be run in procli with -csv constants_analysis
30		tcltk_analyse_constants(Table) :-
31		current_state_id(CurID),
32		tcltk_analyse_constants(CurID,Table).
33
34		:- dynamic constant_can_be_expanded/1.
35
36		:- use_module(library(samsort),[samsort/3]).
37		% called constants_analysis in meta_interface and probcli
38		tcltk_analyse_constants(ID,Table) :-
39		(get_constants_state_for_id(ID,Constants) -> true
40		; ID=root, try_get_unique_constants_state(Constants)),
41		!,
42		retractall(constant_can_be_expanded(_)),
43		findall(H,get_value_info(H,'$DUMMY$',int(0),_),Header),
44		reorder_cols(Header,RHeader),
45		findall(list([CstID|RInfos]), (member(bind(CstID,CstVal),Constants),
46		findall(Info,get_value_info(_,CstID,CstVal,Info),Infos),
47		reorder_cols(Infos,RInfos),
48		debug_format(19,' ~w : ~w~n',[CstID,RInfos])
49		), Entries),
50		samsort(samorder,Entries,SEntries),
51		findall(Cst,constant_can_be_expanded(Cst),ExpList),
52		(ExpList=[] -> true
53		; format(user_output,'Constants that are currently symbolic but could be expanded:~n ~w~n',[ExpList])),
54		Table = list([list(['CONSTANT'|RHeader]) | SEntries]).
55		tcltk_analyse_constants(_,Table) :-
56		Table = list([list(['SETUP CONSTANTS first'])]).
57
58		% move message column to end
59		reorder_cols([Class,MessageCol|OtherCols],ResCols) :- append([Class|OtherCols],[MessageCol],ResCols).
60
61		samorder(list([ID,_,_,TS|_]),list([ID2,_,_,TS2|_])) :- !,(TS,ID) @>= (TS2,ID2).
62		samorder(A,B) :- print(unknown_samorder(A,B)),nl.
63
64		:- use_module(library(terms), [term_size/2]).
65		:- use_module(probsrc(translate), [translate_bvalue_with_limit/3]).
66		get_value_info(class,ID,_,Class) :- get_id_class(ID,Class).
67		get_value_info(INFO,ID,_,Kind) :-
68		is_registered_function_name(ID,_),
69		get_registered_function(_MemoID,ID,RegValue),!, % use stored Memo value instead
70	?	get_value_info2(INFO,ID,RegValue,Kind).
71		get_value_info(INFO,ID,Value,Kind) :-
72	?	get_value_info2(INFO,ID,Value,Kind).
73
74		:- use_module(probsrc(debug),[debug_mode/1]).
75		get_value_info2(Info, ID, Value, Res) :-
76		(var(Info) -> true ; Info=message -> true ; Info=kind),
77		get_value_kind(Value,ID,Kind,Msg),
78		(Info=message,Res=Msg ; Info=kind, Res=Kind).
79		get_value_info2(termsize, _, Value, TS) :- term_size(Value,TS).
80		get_value_info2(value, _, Value, TS) :-
81		(debug_mode(on) -> Limit=1000 ; Limit=100),
82		translate_bvalue_with_limit(Value,Limit,TS).
83
84		% TO DO: use is_concrete_constants_state_id to check if other value exists
85		% TO DO: check if abstract_constants can be converted back
86
87		:- use_module(probsrc(bmachine),[b_is_variable/1,b_is_constant/1]).
88		:- use_module(probsrc(b_machine_hierarchy),[abstract_constant/2]).
89		:- use_module(probsrc(memoization),[is_registered_function_name/2, get_registered_function/3]).
90		:- use_module(probsrc(kernel_objects),[cardinality_as_int/2]).
91
92		get_id_class(ID,Res) :- is_registered_function_name(ID,Expanded),!,
93		(Expanded=true -> Res = 'MEMOIZED (expanded)' ; Res='MEMOIZED'). % probably abstract
94		get_id_class(ID,Res) :- abstract_constant(ID,_),!, Res='ABSTRACT'.
95		get_id_class(ID,Res) :- b_is_constant(ID),!, Res='CONCRETE'.
96		get_id_class(ID,Res) :- b_is_variable(ID),!, Res='VARIABLE'.
97		get_id_class(_,'?').
98
99
100		:- use_module(probsrc(custom_explicit_sets),[is_interval_closure/3, explicit_set_cardinality/2,
101		is_infinite_or_very_large_explicit_set/2,
102		try_expand_custom_set_with_catch/3, is_infinite_explicit_set/1]).
103		:- use_module(library(avl),[avl_size/2]).
104		:- use_module(probsrc(tools_timeout), [time_out_with_factor_call/4]).
105
106		get_simple_value_kind([],_,Res) :- !, Res='EMPTY-Set'.
107		get_simple_value_kind([_|_],_,Res) :- !, Res='LIST-Set'.
108		get_simple_value_kind(avl_set(A),_,Res) :- !, avl_size(A,Size), ajoin(['AVL-Set:',Size],Res).
109		get_simple_value_kind(int(_),_,Res) :- !, Res = 'INTEGER'.
110		get_simple_value_kind(string(_),_,Res) :- !, Res = 'STRING'.
111		get_simple_value_kind(pred_true,_,Res) :- !, Res = 'TRUE'.
112		get_simple_value_kind(pred_false,_,Res) :- !, Res = 'FALSE'.
113		get_simple_value_kind(fd(_,T),_,Res) :- !, Res = T.
114		get_simple_value_kind((_,_),_,Res) :- !, Res = 'PAIR'.
115		get_simple_value_kind(rec(_),_,Res) :- !, Res = 'RECORD'.
116		get_simple_value_kind(CL,_,Res) :- is_interval_closure(CL,_,_),!, Res= 'INTERVAL'.
117
118		get_value_kind(SimpleValue,ID,Res,Msg) :- get_simple_value_kind(SimpleValue,ID,R),!,
119		Res=R, Msg=''.
120		get_value_kind(CL,_,Res,Msg) :- is_infinite_explicit_set(CL),!,
121		Res= 'INFINITE-Set',
122		Msg='The constant is definitely infinite'.
123		get_value_kind(closure(P,T,B),ID,Res,Msg) :-
124		add_debug_message(constants_analysis,'Checking if symbolic closure can be expanded: ',ID,B),
125		% TODO: provide flag as this can take long
126		time_out_with_factor_call(
127		try_expand_custom_set_with_catch(closure(P,T,B),Expansion,get_value_kind),
128		min_max_time_out(10,100,15000), % Factor 10, minimum 100 ms, maximum 15 seconds
129		[silent],
130		(add_debug_message(constants_analysis,'TIME-OUT during expansion for: ',ID),fail)),
131		%functor(Expansion,FF,NN),print(expansion(FF,NN)),nl,
132		%translate:translate_bvalue_with_limit(Expansion,100000,S), write(S),nl,
133		Expansion \= closure(_,_,_),
134		%(length(Expansion,Len) -> print(len(Len)),nl ; true),
135		time_out_with_factor_call(
136		compute_cardinality(closure(P,T,B),Expansion,Size),
137		min_max_time_out(10,100,15000), % Factor=10, but min. 100 ms, max 15000 ms
138		[],
139		(add_debug_message(constants_analysis,'TIME-OUT during computation of Size: ',ID),
140		Size='?')),
141		!, % Symbolic set can be expanded; user could mark it as concrete constant
142		(abstract_constant(ID,_)
143		-> CC = 'Abstract constant ',
144		Suggestion = ' (by moving to CONCRETE_CONSTANTS or annotating with /*@desc expand */ pragma): '
145		; CC = 'Concrete constant ',
146		Suggestion = ' (by annotating with /*@desc expand */ pragma) '
147		),
148		ajoin([CC,'is stored symbolically but can be expanded to a finite set of size ',Size,
149		Suggestion ],Msg),
150		get_constant_span(ID,Span),
151		(constant_can_be_expanded(ID) -> true ; assert(constant_can_be_expanded(ID))),
152		add_debug_message(constants_analysis,Msg,ID,Span),
153		ajoin(['FINITE-SYMBOLIC-Set:',Size],Res).
154		get_value_kind(CL,_,Res,Msg) :-
155		is_infinite_or_very_large_explicit_set(CL,20000),!,
156		Res= 'LARGE-SYMBOLIC-Set',
157		Msg = 'The constant has at least 20000 elements'.
158		get_value_kind(closure(_P,_T,_B),_,Res,Msg) :- !,
159		Res = 'SYMBOLIC-Set', Msg=''.
160		get_value_kind(global_set(G),_,Res,Msg) :- !,
161		Res = G, Msg='The constant is a synonym for an enumerated or deferred set'.
162		%TODO: Z freetypes, ...
163		get_value_kind(_,_,'?','').
164
165		compute_cardinality(_,Expansion,Size) :- length_less(Expansion,100),!, cardinality_as_int(Expansion,int(Size)).
166		compute_cardinality(CS,_,Res) :- explicit_set_cardinality(CS,Size),!,Res=Size.
167		compute_cardinality(_,Expansion,Size) :- cardinality_as_int(Expansion,int(Size)). % can be slow for long lists
168
169
170		/* --------------------------------------------------- */
171		:- dynamic var_min_max/3.
172
173		:- use_module(probsrc(bmachine),[get_nr_of_machine_variables/1, get_nr_of_machine_constants/1, get_constant_span/2]).
174
175		tcltk_compute_min_max(Res) :- tcltk_compute_min_max(interesting,Res).
176
177		tcltk_compute_min_max(_,Res) :-
178	?	\+ (visited_expression_id(X), X\=root),!,
179		Res = list([list(['No states visited yet!'])]).
180		tcltk_compute_min_max(Which,_) :-
181		retractall(var_min_max(_,_,_)),
182	?	visited_expression(ID,State), %print(treat(_ID)),nl,
183		(Which = all -> true
184		; \+ not_interesting(ID)), % only those satisfying scope predicate
185		%functor(State,F,N),print(processing(ID,F,N)),nl,
186		treat_state_for_min_max(State),fail.
187		tcltk_compute_min_max(_,list([Header|Res])) :-
188		Header = list(['Identifier',':','Min-Value','..','Max-Value']),
189		findall(Info, get_info(Info,constant,true), CRes1),
190		findall(Info, get_info(Info,constant,false), CRes2),
191		findall(Info, get_info(Info,variable,true), VRes1),
192		findall(Info, get_info(Info,variable,false), VRes2),
193		combine_results(CRes1,CRes2,CRes),
194		combine_results(VRes1,VRes2,VRes),
195		get_nr_of_machine_variables(NrVars), ajoin(['VARIABLES (',NrVars,')'],VS),
196		(CRes=[]
197		-> Res = [list([VS])|VRes]
198		; get_nr_of_machine_constants(NrCsts), ajoin(['CONSTANTS (',NrCsts,')'],CS),
199		append([list([CS])|CRes],
200		[list([VS])|VRes],Res)).
201
202
203		combine_results([],[],R) :- !, R=[].
204		combine_results(Eq,[],R) :- !, R = [list(['/* all only one value: */'])|Eq].
205		combine_results([],NotEq,R) :- !, R = [list(['/* all more than one value: */'])|NotEq].
206		combine_results(Eq,NotEq,R) :-
207		append([list(['/* with one value: */'])|Eq],
208		[list(['/* with more than one value: */'])|NotEq],R).
209
210		:- use_module(probsrc(tools_files),[write_lines_to_file/2]).
211		pretty_print_min_max_coverage_to_file(Filename) :-
212		tcltk_compute_min_max(list(Res)),
213		write_lines_to_file(Filename,Res).
214
215		:- use_module(probsrc(b_machine_hierarchy),[abstract_constant/2,concrete_constant/2]).
216
217	?	get_info(Info,Type,Equal) :- var_min_max(Var,Min,Max),
218		(Min==Max -> Equal=true ; Equal=false),
219		((abstract_constant(Var,_) ; concrete_constant(Var,_))
220		-> Type = constant ; Type = variable),
221		translate_min_max(Var,Min,Max,Info).
222
223		translate_min_max(Var,M,M,Info) :- !, translate:translate_bvalue(M,TMin),
224		Info = list([Var,'=',TMin]).
225		translate_min_max(Var,pred_false,pred_true,Info) :- !,
226		Info = list([Var,':','BOOL','','(full type)']).
227		translate_min_max(Var,fd(X,T),fd(Y,T),Info) :- !,
228		gen_fd_set(X,Y,T,Set), translate:translate_bvalue(Set,TS),
229		Info = list([Var,':',TS,'','(full type)']).
230		translate_min_max(Var,Min,Max,Info) :-
231		translate:translate_bvalue(Min,TMin),
232		translate:translate_bvalue(Max,TMax),
233		Info = list([Var,':',TMin,'..',TMax]).
234
235		gen_fd_set(X,Y,_T,R) :- X>Y,!, R=[].
236		gen_fd_set(X,Y,T,[fd(X,T)|R]) :- X1 is X+1,
237		gen_fd_set(X1,Y,T,R).
238
239		:- use_module(probsrc(specfile),[property/2]).
240		% treat a visited state for min_max
241		treat_state_for_min_max(const_and_vars(_,S)) :- !, treat_state_for_min_max(S).
242		treat_state_for_min_max(concrete_constants(S)) :- !, treat_state_for_min_max(S).
243		treat_state_for_min_max(csp_and_b(_,S)) :- !, treat_state_for_min_max(S).
244		treat_state_for_min_max(root) :- !.
245		treat_state_for_min_max([]) :- !.
246	?	treat_state_for_min_max(List) :- List=[_|_],!,member(bind(VAR,VAL),List), treat_var(VAR,VAL),fail.
247		treat_state_for_min_max(OtherState) :- \+ b_or_z_mode,
248		property(OtherState,'='(Variable,Value)),
249		treat_var(Variable,Value),fail.
250
251		treat_var(Variable,Value) :- retract(var_min_max(Variable,Min,Max)),!,
252		(is_smaller(Value,Min) -> NewMin = Value ; NewMin=Min),
253		(is_smaller(Max,Value) -> NewMax = Value ; NewMax=Max),
254		assertz(var_min_max(Variable,NewMin,NewMax)).
255		treat_var(Variable,Value) :-
256		assertz(var_min_max(Variable,Value,Value)).
257
258		:- use_module(library(avl),[avl_size/2, avl_max/2]).
259		is_smaller(int(X),int(Y)) :- !, X < Y.
260		is_smaller(string(X),string(Y)) :- !, X @< Y.
261		is_smaller(pred_true,_) :- !,fail.
262		is_smaller(pred_false,_) :- !.
263		is_smaller(fd(X,T),fd(Y,T)) :- !, X < Y.
264		is_smaller((X1,X2),(Y1,Y2)) :- !, (is_smaller(X1,Y1) -> true ; X1=Y1, is_smaller(X2,Y2)).
265		is_smaller([],Y) :- !, Y \== [].
266		is_smaller(_,[]) :- !, fail.
267		is_smaller(avl_set(X),avl_set(Y)) :- avl_size(X,SX), avl_size(Y,SY),!,
268		(SX<SY -> true
269		; SX=SY, avl_max(X,MaxX), avl_max(Y,MaxY),
270		(is_smaller(MaxX,MaxY) % used to be X@<Y
271		-> true
272		; MaxX=MaxY -> X @< Y) % if same maximum; look at all values; TO DO: maybe look at avl_min first
273		).
274		is_smaller(X,Y) :- X @< Y.
275
276		/* --------------------------------------------------- */
277
278		pretty_print_coverage_information_to_file(FileName) :-
279		tcltk_compute_coverage(list(Res)),
280		write_lines_to_file(FileName,Res).
281
282		tcltk_compute_coverage(list(Res)) :-
283		compute_the_coverage(Res,_,_,false,false).
284		tcltk_compute_coverage_and_enabling(list(Res)) :-
285		compute_the_coverage(Res,_,_,true,false).
286		tcltk_compute_coverage_and_degree(list(Res)) :-
287		compute_the_coverage(Res,_,_,false,true).
288
289		compute_the_coverage(Res,TotalNodeNr,TotalTransSum,ShowEnabledInfo,ShowDegreeInfo) :-
290		retractall(operation_hit(_,_,_)),
291		reset_node_hit(ShowEnabledInfo,ShowDegreeInfo),
292		compute_coverage(ShowEnabledInfo,ShowDegreeInfo),
293		findall(S2,
294		(operation_hit(OpS,Nr),
295		%translate:translate_bexpression(Op,OpS),
296		string_concatenate(':',Nr,S1),
297		string_concatenate(OpS,S1,S2)),Res1_),
298		sort(Res1_,Res1),
299		length(Res1,NrCovered),
300		findall(S2,
301		(query_node_hit(Prop,Nr),
302		string_concatenate(':',Nr,S1),
303		string_concatenate(Prop,S1,S2)),Res0),
304		findall(OpName, uncovered_operation(OpName),Res2_),
305		sort(Res2_,Res2),
306		length(Res2,NrUncovered),
307		total_number_of_transitions(TotalTransSum),
308		(ShowEnabledInfo=false
309		-> ResDE = []
310		;
311		findall(DE, def_enables(DE),EnRes1),
312		findall(DE, pos_enables(DE),EnRes2),
313		append(['DEFINITELY_ENABLED_AFTER'|EnRes1],['POSSIBLY_ENABLES'|EnRes2],ResDE)
314		),
315		(ShowDegreeInfo=false
316		-> Res00 = ResDE
317		;
318		findall(DegR, (max_degree(OpDeg,MaxDeg), tools:ajoin([OpDeg,'->',MaxDeg],DegR)), DegRes),
319		append(['MAXIMUM_DEGREE'|DegRes],ResDE,Res00)
320		),
321		get_op_string('UNCOVERED_',NrUncovered,UNCOVEREDSTR),
322		TOTALSTR = 'TOTAL_TRANSITIONS', %get_op_string('TOTAL_',TOTALSTR),
323		get_op_string('COVERED_',NrCovered,COVEREDSTR),
324		append([UNCOVEREDSTR|Res2],Res00,Res01),
325		append([TOTALSTR,TotalTransSum,COVEREDSTR|Res1],
326		Res01,OpRes),
327		query_node_hit(total,TotalNodeNr),
328		ajoin(['STATES (',TotalNodeNr,')'],StatesStr),
329		append([StatesStr|Res0],OpRes,Res).
330		%% ,pge_algo: disabled_operations_stats(ResPGE), % in case no disabling stats are given an empty list is returned
331		%% append(Res_,ResPGE,Res).
332
333		:- use_module(probsrc(specfile),[get_specification_description/2]).
334		get_op_string(PREFIX,Res) :-
335		get_specification_description(operations,OP),
336		string_concatenate(PREFIX,OP,Res).
337		get_op_string(PREFIX,Nr,Res) :-
338		get_specification_description(operations,OP),
339		ajoin([PREFIX,OP,' (',Nr,')'],Res).
340
341
342		def_enables(X) :- operation_hit(OpName1,_,_),
343		definitely_enabled_after(OpName1,OpName2),
344		string_concatenate('====>',OpName2,R1),
345		string_concatenate(OpName1,R1,X).
346		pos_enables(X) :- operation_hit(OpName1,_,_),
347		possibly_enables(OpName1,OpName2),
348		% \+ definitely_enabled_after(OpName1,OpName2),
349		string_concatenate('=?+=>',OpName2,R1),
350		string_concatenate(OpName1,R1,X).
351
352		/* note: assumes that same operation name cannot appear with multiple arity */
353
354		total_number_of_transitions(TotalTransSum) :-
355		findall(Nr,operation_hit(_,_,Nr),List),
356		sum_list(List,0,TotalTransSum).
357
358		sum_list([],N,N).
359		sum_list([H|T],SoFar,Res) :- S1 is SoFar+H, sum_list(T,S1,Res).
360
361		operation_hit(OpTerm,Nr) :-
362	?	operation_hit(OpTerm,_ID,Nr).
363
364		:- dynamic operation_hit/3.
365		operation_hit(operation(_),node__2,55).
366
367		:- use_module(probsrc(specfile),[get_possible_event/1]).
368
369	?	uncovered_operation(OpName) :- get_possible_event(OpName),
370		\+(operation_hit(OpName,_,_)).
371
372		add_cov_hit(OpName,ID) :-
373		((OpName = partition(N,_Op,P)) -> LookupName = partition(N,_,P) ; LookupName = OpName),
374		(retract(operation_hit(LookupName,NID,Nr))
375		-> (N1 is Nr+1, assertz(operation_hit(LookupName,NID,N1)))
376		; (assertz(operation_hit(OpName,ID,1)))
377		).
378
379	?	query_node_hit(Prop,Nr) :- node_hit(Prop,Nr).
380		query_node_hit(total,Nr) :- node_hit(open,N1), node_hit(live,N2), node_hit(deadlocked,N3),
381		Nr is N1+N2+N3.
382		:- dynamic node_hit/2.
383		node_hit(property,22).
384		add_node_hit(OpName) :-
385		(retract(node_hit(OpName,Nr))
386		-> N1 is Nr+1, assertz(node_hit(OpName,N1))
387		; assertz(node_hit(OpName,1))
388		).
389
390		reset_node_hit(ShowEnabledInfo,ShowDegreeInfo) :-
391		retractall(node_hit(_,_)),
392		assertz(node_hit(deadlocked,0)),
393		(b_or_z_mode -> assertz(node_hit(invariant_violated,0)),
394		assertz(node_hit(invariant_not_checked,0))
395		; true),
396		assertz(node_hit(open,0)), assertz(node_hit(live,0)),
397		init_enabling_degree_info(ShowEnabledInfo,ShowDegreeInfo).
398
399		:- use_module(probsrc(specfile),[get_operation_name/2]).
400
401		:- use_module(probsrc(state_space_exploration_modes),[is_not_interesting/1]).
402		compute_coverage(_,_) :-
403	?	visited_expression_id(ID),
404		(not_all_transitions_added(ID)
405		-> add_node_hit(open)
406	?	; (transition(ID,_,_) -> add_node_hit(live)
407		; is_not_interesting(ID) -> add_node_hit(ignored)
408		; max_reached_or_timeout_for_node(ID) -> true % e.g., if MAX_OPERATIONS set to 0
409		; add_node_hit(deadlocked))
410		),
411	?	(max_reached_or_timeout_for_node(ID)
412		-> add_node_hit(explored_but_not_all_transitions_computed)
413		; true
414		),
415		(invariant_violated(ID) -> add_node_hit(invariant_violated) ; true),
416		(time_out_for_invariant(ID) -> add_node_hit(invariant_time_out) ; true),
417		(time_out_for_assertions(ID) -> add_node_hit(assertions_time_out) ; true),
418	?	(invariant_not_yet_checked(ID) -> add_node_hit(invariant_not_checked) ; true),
419		(state_error(ID,_,Err),Err\=invariant_violated ->
420		(Err=abort_error(TYPE,_,_,_)
421		-> add_node_hit(TYPE)
422		; add_node_hit(state_error))
423		; true),
424		fail.
425		compute_coverage(ShowEnabledInfo,ShowDegreeInfo) :-
426	?	transition(ID,Operation,NID),
427		nonvar(Operation),
428		get_operation_name(Operation,OpName),
429		add_cov_hit(OpName,ID),
430		(ShowEnabledInfo=true -> update_enabling_info(ID,OpName,NID) ; true),
431		(ShowDegreeInfo=true -> update_degree_info(ID,OpName) ; true),
432		fail.
433		%compute_coverage :- print_message('Covered Properties: '),
434		% node_hit(OpName,Nr),
435		% print(OpName), print(' nodes:'), print(Nr),nl,
436		% fail.
437		%compute_coverage :- print_message('Covered Operations: '),
438		% operation_hit(OpName,_ID,Nr),
439		% print(OpName), print(' hits:'), print(Nr),nl,
440		% fail.
441		%compute_coverage :- nl, print_message('Uncovered Operations: '),
442		% uncovered_operation(OpName),
443		% print(OpName), print(' '), fail.
444		compute_coverage(_ShowEnabledInfo,ShowDegreeInfo) :-
445		(ShowDegreeInfo=true -> finalise_degree_info ; true).
446
447
448
449
450		:- dynamic definitely_enabled_after/2, possibly_enables/2. /* true if after an operation another is always enabled */
451		:- dynamic degree_in_id/3, max_degree/2.
452
453		:- use_module(probsrc(specfile),[b_or_z_mode/0]).
454		:- use_module(probsrc(bmachine),[b_is_operation_name/1]).
455		init_enabling_degree_info(ShowEnabledInfo,_ShowDegreeInfo) :-
456		retractall(definitely_enabled_after(_,_)),
457		retractall(possibly_enables(_,_)),
458		retractall(degree_in_id(_,_,_)),
459		retractall(max_degree(_,_)),
460		b_or_z_mode,
461		ShowEnabledInfo=true,
462		(b_is_operation_name(OpName1) ; OpName1 = '$initialise_machine'),
463		b_is_operation_name(OpName2),
464		assertz(definitely_enabled_after(OpName1,OpName2)),
465		fail.
466		init_enabling_degree_info(_,_).
467
468		finalise_degree_info :- update_last_degree.
469
470		update_enabling_info(_ID,OpName,NewID) :- %print(upd(_ID,OpName)),nl,
471		definitely_enabled_after(OpName,OpName2),
472		(opname_possible(NewID,OpName2)
473		-> true
474		; retract(definitely_enabled_after(OpName,OpName2))
475		%(retract(definitely_enabled_after(OpName,OpName2)) -> print(retract(OpName,OpName2)))
476		),fail.
477		update_enabling_info(ID,OpName,NewID) :- %print(upd(_ID,OpName)),nl,
478		opname_possible(NewID,OpName2), % Note: can succeed multiple times with same OpName2 !
479		\+ possibly_enables(OpName,OpName2),
480		\+ opname_possible(ID,OpName2),
481		assertz(possibly_enables(OpName,OpName2)),
482		fail.
483		update_enabling_info(_,_,_).
484
485		% NOTE: we suppose that the transitions are grouped by operation name for each state id; may not be true for CSP ??
486		update_degree_info(ID,OpName) :-
487		get_cur_degree(ID,OpName,Degree), D1 is Degree+1,
488		assertz(degree_in_id(ID,OpName,D1)),
489		fail.
490		update_degree_info(_,_).
491
492		update_last_degree :- (retract(degree_in_id(_,OpName,D)) -> update_degree(OpName,D) ; true).
493
494		get_cur_degree(ID,OpName,Degree) :-
495		(retract(degree_in_id(ID,OpName,D)) -> Degree=D
496		; update_last_degree,
497		Degree=0).
498		update_degree(OpName,Degree) :-
499		((max_degree(OpName,Max), Max>=Degree) -> true
500		; retractall(max_degree(OpName,_)), format('Update degree ~w -> ~w~n',[OpName,Degree]),
501		assertz(max_degree(OpName,Degree))
502		).
503		opname_possible(ID,OpName) :- transition(ID,Op,_),get_operation_name(Op,OpName).
504
505		% -------------------------------------
506
507