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