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_nr_of_machine_variables/1, get_nr_of_machine_constants/1, 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