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 |