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