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 %% ,pge_algo: disabled_operations_stats(ResPGE), % in case no disabling stats are given an empty list is returned
309 %% append(Res_,ResPGE,Res).
310
311 :- use_module(probsrc(specfile),[get_specification_description/2]).
312 get_op_string(PREFIX,Res) :-
313 get_specification_description(operations,OP),
314 string_concatenate(PREFIX,OP,Res).
315 get_op_string(PREFIX,Nr,Res) :-
316 get_specification_description(operations,OP),
317 ajoin([PREFIX,OP,' (',Nr,')'],Res).
318
319
320 def_enables(X) :- operation_hit(OpName1,_,_),
321 definitely_enabled_after(OpName1,OpName2),
322 string_concatenate('====>',OpName2,R1),
323 string_concatenate(OpName1,R1,X).
324 pos_enables(X) :- operation_hit(OpName1,_,_),
325 possibly_enables(OpName1,OpName2),
326 % \+ definitely_enabled_after(OpName1,OpName2),
327 string_concatenate('=?+=>',OpName2,R1),
328 string_concatenate(OpName1,R1,X).
329
330 /* note: assumes that same operation name cannot appear with multiple arity */
331
332 total_number_of_transitions(TotalTransSum) :-
333 findall(Nr,operation_hit(_,_,Nr),List),
334 sum_list(List,0,TotalTransSum).
335
336 sum_list([],N,N).
337 sum_list([H|T],SoFar,Res) :- S1 is SoFar+H, sum_list(T,S1,Res).
338
339 operation_hit(OpTerm,Nr) :-
340 ? operation_hit(OpTerm,_ID,Nr).
341
342 :- dynamic operation_hit/3.
343 operation_hit(operation(_),node__2,55).
344
345 :- use_module(probsrc(specfile),[get_possible_event/1]).
346
347 ?uncovered_operation(OpName) :- get_possible_event(OpName),
348 \+(operation_hit(OpName,_,_)).
349
350 add_cov_hit(OpName,ID) :-
351 ((OpName = partition(N,_Op,P)) -> LookupName = partition(N,_,P) ; LookupName = OpName),
352 (retract(operation_hit(LookupName,NID,Nr))
353 -> (N1 is Nr+1, assertz(operation_hit(LookupName,NID,N1)))
354 ; (assertz(operation_hit(OpName,ID,1)))
355 ).
356
357 ?query_node_hit(Prop,Nr) :- node_hit(Prop,Nr).
358 query_node_hit(total,Nr) :- node_hit(open,N1), node_hit(live,N2), node_hit(deadlocked,N3),
359 Nr is N1+N2+N3.
360 :- dynamic node_hit/2.
361 node_hit(property,22).
362 add_node_hit(OpName) :-
363 (retract(node_hit(OpName,Nr))
364 -> N1 is Nr+1, assertz(node_hit(OpName,N1))
365 ; assertz(node_hit(OpName,1))
366 ).
367
368 reset_node_hit(ShowEnabledInfo,ShowDegreeInfo) :-
369 retractall(node_hit(_,_)),
370 assertz(node_hit(deadlocked,0)),
371 (b_or_z_mode -> assertz(node_hit(invariant_violated,0)),
372 assertz(node_hit(invariant_not_checked,0))
373 ; true),
374 assertz(node_hit(open,0)), assertz(node_hit(live,0)),
375 init_enabling_degree_info(ShowEnabledInfo,ShowDegreeInfo).
376
377 :- use_module(probsrc(specfile),[get_operation_name/2]).
378
379 :- use_module(probsrc(state_space_exploration_modes),[is_not_interesting/1]).
380 compute_coverage(_,_) :-
381 ? visited_expression_id(ID),
382 (not_all_transitions_added(ID)
383 -> add_node_hit(open)
384 ? ; (transition(ID,_,_) -> add_node_hit(live)
385 ; is_not_interesting(ID) -> add_node_hit(ignored)
386 ; max_reached_or_timeout_for_node(ID) -> true % e.g., if MAX_OPERATIONS set to 0
387 ; add_node_hit(deadlocked))
388 ),
389 ? (max_reached_or_timeout_for_node(ID)
390 -> add_node_hit(explored_but_not_all_transitions_computed)
391 ; true
392 ),
393 (invariant_violated(ID) -> add_node_hit(invariant_violated) ; true),
394 (time_out_for_invariant(ID) -> add_node_hit(invariant_time_out) ; true),
395 (time_out_for_assertions(ID) -> add_node_hit(assertions_time_out) ; true),
396 ? (invariant_not_yet_checked(ID) -> add_node_hit(invariant_not_checked) ; true),
397 (state_error(ID,_,Err),Err\=invariant_violated ->
398 (Err=abort_error(TYPE,_,_,_)
399 -> add_node_hit(TYPE)
400 ; add_node_hit(state_error))
401 ; true),
402 fail.
403 compute_coverage(ShowEnabledInfo,ShowDegreeInfo) :-
404 ? transition(ID,Operation,NID),
405 nonvar(Operation),
406 get_operation_name(Operation,OpName),
407 add_cov_hit(OpName,ID),
408 (ShowEnabledInfo=true -> update_enabling_info(ID,OpName,NID) ; true),
409 (ShowDegreeInfo=true -> update_degree_info(ID,OpName) ; true),
410 fail.
411 %compute_coverage :- print_message('Covered Properties: '),
412 % node_hit(OpName,Nr),
413 % print(OpName), print(' nodes:'), print(Nr),nl,
414 % fail.
415 %compute_coverage :- print_message('Covered Operations: '),
416 % operation_hit(OpName,_ID,Nr),
417 % print(OpName), print(' hits:'), print(Nr),nl,
418 % fail.
419 %compute_coverage :- nl, print_message('Uncovered Operations: '),
420 % uncovered_operation(OpName),
421 % print(OpName), print(' '), fail.
422 compute_coverage(_ShowEnabledInfo,ShowDegreeInfo) :-
423 (ShowDegreeInfo=true -> finalise_degree_info ; true).
424
425
426
427
428 :- dynamic definitely_enabled_after/2, possibly_enables/2. /* true if after an operation another is always enabled */
429 :- dynamic degree_in_id/3, max_degree/2.
430
431 :- use_module(probsrc(specfile),[b_or_z_mode/0]).
432 :- use_module(probsrc(bmachine),[b_is_operation_name/1]).
433 init_enabling_degree_info(ShowEnabledInfo,_ShowDegreeInfo) :-
434 retractall(definitely_enabled_after(_,_)),
435 retractall(possibly_enables(_,_)),
436 retractall(degree_in_id(_,_,_)),
437 retractall(max_degree(_,_)),
438 b_or_z_mode,
439 ShowEnabledInfo=true,
440 (b_is_operation_name(OpName1) ; OpName1 = '$initialise_machine'),
441 b_is_operation_name(OpName2),
442 assertz(definitely_enabled_after(OpName1,OpName2)),
443 fail.
444 init_enabling_degree_info(_,_).
445
446 finalise_degree_info :- update_last_degree.
447
448 update_enabling_info(_ID,OpName,NewID) :- %print(upd(_ID,OpName)),nl,
449 definitely_enabled_after(OpName,OpName2),
450 (opname_possible(NewID,OpName2)
451 -> true
452 ; retract(definitely_enabled_after(OpName,OpName2))
453 %(retract(definitely_enabled_after(OpName,OpName2)) -> print(retract(OpName,OpName2)))
454 ),fail.
455 update_enabling_info(ID,OpName,NewID) :- %print(upd(_ID,OpName)),nl,
456 opname_possible(NewID,OpName2), % Note: can succeed multiple times with same OpName2 !
457 \+ possibly_enables(OpName,OpName2),
458 \+ opname_possible(ID,OpName2),
459 assertz(possibly_enables(OpName,OpName2)),
460 fail.
461 update_enabling_info(_,_,_).
462
463 % NOTE: we suppose that the transitions are grouped by operation name for each state id; may not be true for CSP ??
464 update_degree_info(ID,OpName) :-
465 get_cur_degree(ID,OpName,Degree), D1 is Degree+1,
466 assertz(degree_in_id(ID,OpName,D1)),
467 fail.
468 update_degree_info(_,_).
469
470 update_last_degree :- (retract(degree_in_id(_,OpName,D)) -> update_degree(OpName,D) ; true).
471
472 get_cur_degree(ID,OpName,Degree) :-
473 (retract(degree_in_id(ID,OpName,D)) -> Degree=D
474 ; update_last_degree,
475 Degree=0).
476 update_degree(OpName,Degree) :-
477 ((max_degree(OpName,Max), Max>=Degree) -> true
478 ; retractall(max_degree(OpName,_)), format('Update degree ~w -> ~w~n',[OpName,Degree]),
479 assertz(max_degree(OpName,Degree))
480 ).
481 opname_possible(ID,OpName) :- transition(ID,Op,_),get_operation_name(Op,OpName).
482
483 % -------------------------------------
484
485