1		% (c) 2009-2019 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,pretty_print_min_max_coverage_to_file/1,
8		compute_the_coverage/5,pretty_print_coverage_information_to_file/1,
9		operation_hit/2,query_node_hit/2, uncovered_operation/1]).
10
11		:- use_module(state_space).
12		:- use_module(tools).
13
14		:- use_module(module_information).
15		:- module_info(group,animator).
16		:- module_info(description,'This module is responsible for computing state space coverage info.').
17
18		/* --------------------------------------------------- */
19		:- dynamic var_min_max/3.
20
21		tcltk_compute_min_max(_) :-
22		retractall(var_min_max(_,_,_)),
23		visited_expression(_ID,State), %print(treat(_ID)),nl,
24		treat_state(State),fail.
25		tcltk_compute_min_max(list(Res)) :-
26		findall(Info, get_info(Info,constant,true), CRes1),
27		findall(Info, get_info(Info,constant,false), CRes2),
28		findall(Info, get_info(Info,variable,true), VRes1),
29		findall(Info, get_info(Info,variable,false), VRes2),
30		combine_results(CRes1,CRes2,CRes),
31		combine_results(VRes1,VRes2,VRes),
32		(CRes=[] -> Res = ['VARIABLES'|VRes] ;
33		append(['CONSTANTS'|CRes],['VARIABLES'|VRes],Res)).
34
35		combine_results([],[],R) :- !, R=[].
36		combine_results(Eq,[],R) :- R = ['/* all only one value: */'|Eq].
37		combine_results([],NotEq,R) :- R = ['/* all more than one value: */'|NotEq].
38		combine_results(Eq,NotEq,R) :-
39		append(['/* with one value: */'|Eq],['/* with more than one value: */'|NotEq],R).
40
41		:- use_module(tools_files,[write_lines_to_file/2]).
42		pretty_print_min_max_coverage_to_file(Filename) :-
43		tcltk_compute_min_max(list(Res)),
44		write_lines_to_file(Filename,Res).
45
46		:- use_module(b_machine_hierarchy,[abstract_constant/2,concrete_constant/2]).
47
48		get_info(Info,Type,Equal) :- var_min_max(Var,Min,Max),
49		(Min==Max -> Equal=true ; Equal=false),
50		((abstract_constant(Var,_) ; concrete_constant(Var,_))
51		-> Type = constant ; Type = variable),
52		translate_min_max(Var,Min,Max,Info).
53
54		translate_min_max(Var,M,M,Info) :- !, translate:translate_bvalue(M,TMin),
55		ajoin([Var,'=',TMin],Info).
56		translate_min_max(Var,pred_false,pred_true,Info) :- !,
57		ajoin([Var,':BOOL'],Info).
58		translate_min_max(Var,fd(X,T),fd(Y,T),Info) :- !,
59		gen_fd_set(X,Y,T,Set), translate:translate_bvalue(Set,TS),
60		ajoin([Var,':',TS],Info).
61		translate_min_max(Var,Min,Max,Info) :-
62		translate:translate_bvalue(Min,TMin),
63		translate:translate_bvalue(Max,TMax),
64		ajoin([Var,':',TMin,'..',TMax],Info).
65
66		gen_fd_set(X,Y,_T,R) :- X>Y,!, R=[].
67		gen_fd_set(X,Y,T,[fd(X,T)|R]) :- X1 is X+1,
68		gen_fd_set(X1,Y,T,R).
69
70		treat_state(const_and_vars(_,S)) :- !, treat_state(S).
71		treat_state(concrete_constants(S)) :- !, treat_state(S).
72		treat_state(csp_and_b(_,S)) :- !, treat_state(S).
73		treat_state(List) :- member(bind(VAR,VAL),List), treat_var(VAR,VAL),fail.
74
75		treat_var(Variable,Value) :- retract(var_min_max(Variable,Min,Max)),!,
76		(is_smaller(Value,Min) -> NewMin = Value ; NewMin=Min),
77		(is_smaller(Max,Value) -> NewMax = Value ; NewMax=Max),
78		assert(var_min_max(Variable,NewMin,NewMax)).
79		treat_var(Variable,Value) :-
80		assert(var_min_max(Variable,Value,Value)).
81
82		:- use_module(library(avl),[avl_size/2, avl_max/2]).
83		is_smaller(int(X),int(Y)) :- !, X < Y.
84		is_smaller(string(X),string(Y)) :- !, X @< Y.
85		is_smaller(pred_true,_) :- !,fail.
86		is_smaller(pred_false,_) :- !.
87		is_smaller(fd(X,T),fd(Y,T)) :- !, X < Y.
88		is_smaller((X1,X2),(Y1,Y2)) :- !, (is_smaller(X1,Y1) -> true ; X1=Y1, is_smaller(X2,Y2)).
89		is_smaller([],Y) :- !, Y \== [].
90		is_smaller(_,[]) :- !, fail.
91		is_smaller(avl_set(X),avl_set(Y)) :- avl_size(X,SX), avl_size(Y,SY),!,
92		(SX<SY -> true
93		; SX=SY, avl_max(X,MaxX), avl_max(Y,MaxY),
94		(is_smaller(MaxX,MaxY) % used to be X@<Y
95		-> true
96		; MaxX=MaxY -> X @< Y) % if same maximum; look at all values; TO DO: maybe look at avl_min first
97		).
98		is_smaller(X,Y) :- X @< Y.
99
100		/* --------------------------------------------------- */
101
102		pretty_print_coverage_information_to_file(FileName) :-
103		tcltk_compute_coverage(list(Res)),
104		write_lines_to_file(FileName,Res).
105
106		tcltk_compute_coverage(list(Res)) :-
107		compute_the_coverage(Res,_,_,false,false).
108		tcltk_compute_coverage_and_enabling(list(Res)) :-
109		compute_the_coverage(Res,_,_,true,false).
110		tcltk_compute_coverage_and_degree(list(Res)) :-
111		compute_the_coverage(Res,_,_,false,true).
112
113		compute_the_coverage(Res,TotalNodeNr,TotalTransSum,ShowEnabledInfo,ShowDegreeInfo) :-
114		retractall(operation_hit(_,_,_)),
115		reset_node_hit(ShowEnabledInfo,ShowDegreeInfo),
116		compute_coverage(ShowEnabledInfo,ShowDegreeInfo),
117		findall(S2,
118		(operation_hit(OpS,Nr),
119		%translate:translate_bexpression(Op,OpS),
120		string_concatenate(':',Nr,S1),
121		string_concatenate(OpS,S1,S2)),Res1_),
122		sort(Res1_,Res1),
123		findall(S2,
124		(query_node_hit(Prop,Nr),
125		string_concatenate(':',Nr,S1),
126		string_concatenate(Prop,S1,S2)),Res0),
127		findall(OpName, uncovered_operation(OpName),Res2_),
128		sort(Res2_,Res2),
129		total_number_of_transitions(TotalTransSum),
130		(ShowEnabledInfo=false
131		-> ResDE = []
132		;
133		findall(DE, def_enables(DE),EnRes1),
134		findall(DE, pos_enables(DE),EnRes2),
135		append(['DEFINITELY_ENABLED_AFTER'|EnRes1],['POSSIBLY_ENABLES'|EnRes2],ResDE)
136		),
137		(ShowDegreeInfo=false
138		-> Res00 = ResDE
139		;
140		findall(DegR, (max_degree(OpDeg,MaxDeg), tools:ajoin([OpDeg,'->',MaxDeg],DegR)), DegRes),
141		append(['MAXIMUM_DEGREE'|DegRes],ResDE,Res00)
142		),
143		get_op_string('UNCOVERED_',UNCOVEREDSTR),
144		get_op_string('TOTAL_',TOTALSTR), get_op_string('COVERED_',COVEREDSTR),
145		append([UNCOVEREDSTR|Res2],Res00,Res01),
146		append([TOTALSTR,TotalTransSum,COVEREDSTR|Res1],
147		Res01,OpRes),
148		append(['STATES'|Res0],OpRes,Res),
149		query_node_hit(total,TotalNodeNr).
150		%% ,pge_algo: disabled_operations_stats(ResPGE), % in case no disabling stats are given an empty list is returned
151		%% append(Res_,ResPGE,Res).
152
153		:- use_module(specfile,[get_specification_description/2]).
154		get_op_string(PREFIX,Res) :-
155		get_specification_description(operations,OP),
156		string_concatenate(PREFIX,OP,Res).
157
158
159		def_enables(X) :- operation_hit(OpName1,_,_),
160		definitely_enabled_after(OpName1,OpName2),
161		string_concatenate('====>',OpName2,R1),
162		string_concatenate(OpName1,R1,X).
163		pos_enables(X) :- operation_hit(OpName1,_,_),
164		possibly_enables(OpName1,OpName2),
165		% \+ definitely_enabled_after(OpName1,OpName2),
166		string_concatenate('=?+=>',OpName2,R1),
167		string_concatenate(OpName1,R1,X).
168
169		/* note: assumes that same operation name cannot appear with multiple arity */
170
171		total_number_of_transitions(TotalTransSum) :-
172		findall(Nr,operation_hit(_,_,Nr),List),
173		sum_list(List,0,TotalTransSum).
174
175		sum_list([],N,N).
176		sum_list([H|T],SoFar,Res) :- S1 is SoFar+H, sum_list(T,S1,Res).
177
178		operation_hit(OpTerm,Nr) :-
179		operation_hit(OpTerm,_ID,Nr).
180
181		:- dynamic operation_hit/3.
182		operation_hit(operation(_),node__2,55).
183
184		:- use_module(specfile,[get_possible_event/1]).
185
186		uncovered_operation(OpName) :- specfile:get_possible_event(OpName),
187		\+(operation_hit(OpName,_,_)).
188
189		add_hit(OpName,ID) :-
190		((OpName = partition(N,_Op,P)) -> LookupName = partition(N,_,P) ; LookupName = OpName),
191		(retract(operation_hit(LookupName,NID,Nr))
192		-> (N1 is Nr+1, assert(operation_hit(LookupName,NID,N1)))
193		; (assert(operation_hit(OpName,ID,1)))
194		).
195
196		query_node_hit(Prop,Nr) :- node_hit(Prop,Nr).
197		query_node_hit(total,Nr) :- node_hit(open,N1), node_hit(live,N2), node_hit(deadlocked,N3),
198		Nr is N1+N2+N3.
199		:- dynamic node_hit/2.
200		node_hit(property,22).
201		add_node_hit(OpName) :-
202		(retract(node_hit(OpName,Nr))
203		-> N1 is Nr+1, assert(node_hit(OpName,N1))
204		; assert(node_hit(OpName,1))
205		).
206
207		reset_node_hit(ShowEnabledInfo,ShowDegreeInfo) :-
208		retractall(node_hit(_,_)),
209		assert(node_hit(deadlocked,0)),
210		(specfile:b_or_z_mode -> assert(node_hit(invariant_violated,0)),
211		assert(node_hit(invariant_not_checked,0))
212		; true),
213		assert(node_hit(open,0)), assert(node_hit(live,0)),
214		init_enabling_degree_info(ShowEnabledInfo,ShowDegreeInfo).
215
216		:- use_module(specfile,[get_operation_name/2]).
217
218		compute_coverage(_,_) :-
219		visited_expression_id(ID),
220		(not_all_transitions_added(ID)
221		-> add_node_hit(open)
222		; (transition(ID,_,_) -> add_node_hit(live)
223		; user:is_not_interesting(ID) -> add_node_hit(ignored)
224		; max_reached_or_timeout_for_node(ID) -> true % e.g., if MAX_OPERATIONS set to 0
225		; otherwise -> add_node_hit(deadlocked))
226		),
227		(max_reached_or_timeout_for_node(ID)
228		-> add_node_hit(explored_but_not_all_transitions_computed)
229		; true
230		),
231		(invariant_violated(ID) -> add_node_hit(invariant_violated) ; true),
232		(time_out_for_invariant(ID) -> add_node_hit(invariant_time_out) ; true),
233		(time_out_for_assertions(ID) -> add_node_hit(assertions_time_out) ; true),
234		(invariant_not_yet_checked(ID) -> add_node_hit(invariant_not_checked) ; true),
235		(state_error(ID,_,Err),Err\=invariant_violated ->
236		(Err=abort_error(TYPE,_,_,_)
237		-> add_node_hit(TYPE)
238		; add_node_hit(state_error))
239		; true),
240		fail.
241		compute_coverage(ShowEnabledInfo,ShowDegreeInfo) :-
242		transition(ID,Operation,NID),
243		nonvar(Operation),
244		get_operation_name(Operation,OpName),
245		add_hit(OpName,ID),
246		(ShowEnabledInfo=true -> update_enabling_info(ID,OpName,NID) ; true),
247		(ShowDegreeInfo=true -> update_degree_info(ID,OpName) ; true),
248		fail.
249		%compute_coverage :- print_message('Covered Properties: '),
250		% node_hit(OpName,Nr),
251		% print(OpName), print(' nodes:'), print(Nr),nl,
252		% fail.
253		%compute_coverage :- print_message('Covered Operations: '),
254		% operation_hit(OpName,_ID,Nr),
255		% print(OpName), print(' hits:'), print(Nr),nl,
256		% fail.
257		%compute_coverage :- nl, print_message('Uncovered Operations: '),
258		% uncovered_operation(OpName),
259		% print(OpName), print(' '), fail.
260		compute_coverage(_ShowEnabledInfo,ShowDegreeInfo) :-
261		(ShowDegreeInfo=true -> finalise_degree_info ; true),
262		nl.
263
264
265
266
267		:- dynamic definitely_enabled_after/2, possibly_enables/2. /* true if after an operation another is always enabled */
268		:- dynamic degree_in_id/3, max_degree/2.
269
270		:- use_module(specfile,[b_mode/0]).
271		:- use_module(bmachine,[b_is_operation_name/1,b_get_machine_operation/4]).
272		init_enabling_degree_info(ShowEnabledInfo,_ShowDegreeInfo) :-
273		retractall(definitely_enabled_after(_,_)),
274		retractall(possibly_enables(_,_)),
275		retractall(degree_in_id(_,_,_)),
276		retractall(max_degree(_,_)),
277		b_mode,
278		ShowEnabledInfo=true,
279		(b_is_operation_name(OpName1) ; OpName1 = '$initialise_machine'),
280		b_is_operation_name(OpName2),
281		assert(definitely_enabled_after(OpName1,OpName2)),
282		fail.
283		init_enabling_degree_info(_,_).
284
285		finalise_degree_info :- update_last_degree.
286
287		update_enabling_info(_ID,OpName,NewID) :- %print(upd(_ID,OpName)),nl,
288		definitely_enabled_after(OpName,OpName2),
289		(opname_possible(NewID,OpName2)
290		-> true
291		; retract(definitely_enabled_after(OpName,OpName2))
292		%(retract(definitely_enabled_after(OpName,OpName2)) -> print(retract(OpName,OpName2)))
293		),fail.
294		update_enabling_info(ID,OpName,NewID) :- %print(upd(_ID,OpName)),nl,
295		opname_possible(NewID,OpName2), % Note: can succeed multiple times with same OpName2 !
296		\+ possibly_enables(OpName,OpName2),
297		\+ opname_possible(ID,OpName2),
298		assert(possibly_enables(OpName,OpName2)),
299		fail.
300		update_enabling_info(_,_,_).
301
302		% NOTE: we suppose that the transitions are grouped by operation name for each state id; may not be true for CSP ??
303		update_degree_info(ID,OpName) :-
304		get_cur_degree(ID,OpName,Degree), D1 is Degree+1,
305		assert(degree_in_id(ID,OpName,D1)),
306		fail.
307		update_degree_info(_,_).
308
309		update_last_degree :- (retract(degree_in_id(_,OpName,D)) -> update_degree(OpName,D) ; true).
310
311		get_cur_degree(ID,OpName,Degree) :-
312		(retract(degree_in_id(ID,OpName,D)) -> Degree=D
313		; update_last_degree,
314		Degree=0).
315		update_degree(OpName,Degree) :-
316		((max_degree(OpName,Max), Max>=Degree) -> true
317		; retractall(max_degree(OpName,_)), format('Update degree ~w -> ~w~n',[OpName,Degree]),
318		assert(max_degree(OpName,Degree))
319		).
320		opname_possible(ID,OpName) :- transition(ID,Op,_),get_operation_name(Op,OpName).
321
322		% -------------------------------------
323
324