1 | % (c) 2009-2024 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(reduce_graph_state_space, [print_state_merge_for_dot/1,print_dot_for_dfa_from_nfa/1, | |
6 | print_min_dfa_for_dot/1, | |
7 | reduce_graph_reset/0, | |
8 | %assert_desired_user_transitions/1, | |
9 | %state_merge_separate_iviolations/1, | |
10 | print_subgraph_associated_with_invariant_violations/1, | |
11 | %assert_goal_nodes/0, | |
12 | %jump_to_next_goal_node/1, | |
13 | print_subgraph_of_goal_nodes/1, | |
14 | set_signature_merge_show_all_transitions/1, | |
15 | signature_merge_show_all_transitions/1, | |
16 | %time_stamp/1, time_between/3, mc_duration/1, | |
17 | %total_visited_states/1, total_transitions/1, | |
18 | %reset_use_all_ops_args/0, | |
19 | ||
20 | extract_graph_of_state_merge/1, | |
21 | ||
22 | ||
23 | % tcltk gui | |
24 | user_made_op_selection/0, user_made_arg_selection/0, set_use_all_operations/2 | |
25 | ||
26 | /* symmetry reduction */ | |
27 | %% cleanup_symmetry/0 /* remove all stored representatives */, | |
28 | %% representative/3 /* get the representative state for this state */, | |
29 | %%% reset_relation_types/0 /* resetting this module for new machine */ | |
30 | ]). | |
31 | ||
32 | /* reduce_graph_state_space.pl - GRAPH REDUCTION FUNCTIONS */ | |
33 | ||
34 | /* List of functions that work and (often) reduce the current state space | |
35 | - print_dot_for_dfa_from_nfa(File). | |
36 | - print_min_dfa_for_dot(File). | |
37 | - print_state_merge_for_dot(File). | |
38 | ||
39 | NB: print_min_dfa_for_dot will perform the nfa -> dfa conversion first, and then | |
40 | try and reduce it. However, this doesn't seem to further reduce the dfa ==> | |
41 | dfa is minimal already | |
42 | */ | |
43 | :- use_module(probsrc(tools)). | |
44 | ||
45 | :- use_module(probsrc(module_information),[module_info/2]). | |
46 | :- module_info(group,dot). | |
47 | :- module_info(description,'Various minimization/reduction algorithms for the state space.'). | |
48 | ||
49 | ||
50 | :- use_module(library(lists)). | |
51 | %:- use_module(library(system)). | |
52 | :- use_module(probsrc(preferences)). | |
53 | %:- use_module(library(terms)). | |
54 | ||
55 | :- use_module(dotsrc(visualize_graph),[print_graph_header/1, | |
56 | print_graph_footer/0]). | |
57 | :- use_module(probsrc(state_space),[visited_expression/2, visited_expression_id/1, | |
58 | transition/3, | |
59 | invariant_violated/1, not_all_transitions_added/1]). | |
60 | :- use_module(probsrc(specfile),[csp_mode/0]). | |
61 | :- use_module(probsrc(translate),[translate_bvalue/2]). | |
62 | ||
63 | reduce_graph_reset :- assert_desired_user_transitions(alphabet), | |
64 | reset_use_all_ops_args, reset_counter. | |
65 | ||
66 | :- use_module(probsrc(eventhandling),[register_event_listener/3]). | |
67 | :- register_event_listener(clear_specification,reduce_graph_reset, | |
68 | 'Reset reduce_graph_state_space.'). | |
69 | ||
70 | :- set_prolog_flag(double_quotes, codes). | |
71 | ||
72 | /*============================================================================== | |
73 | Utility Functions | |
74 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ | |
75 | ||
76 | ||
77 | % different types of graphs | |
78 | graph_type(signature_merge). | |
79 | graph_type(dfa_abstraction). | |
80 | ||
81 | ||
82 | % flatten list | |
83 | ent03r_flatten([],[]) :- !. | |
84 | ent03r_flatten([X|L],R) :- !, ent03r_flatten(X,XR), ent03r_flatten(L,LR), append(XR,LR,R). | |
85 | ent03r_flatten(X,[X]). | |
86 | ||
87 | ||
88 | ent03r_union([],X,X). | |
89 | ent03r_union([X|R],Y,Z) :- member(X,Y),!,ent03r_union(R,Y,Z). | |
90 | ent03r_union([X|R],Y,[X|Z]) :- ent03r_union(R,Y,Z). | |
91 | ||
92 | :- volatile curr_equivalence_class_id/1. | |
93 | :- dynamic curr_equivalence_class_id/1. | |
94 | ||
95 | % initialise id counter | |
96 | init_equivalence_class_id :- | |
97 | (curr_equivalence_class_id(X) -> | |
98 | retract(curr_equivalence_class_id(X)) | |
99 | ;true), | |
100 | assertz(curr_equivalence_class_id(0)). | |
101 | ||
102 | % get a unique id | |
103 | next_equivalence_class_id(ID) :- | |
104 | (curr_equivalence_class_id(X) -> | |
105 | ID is X+1, | |
106 | retract(curr_equivalence_class_id(X)), | |
107 | assertz(curr_equivalence_class_id(ID)) | |
108 | ; ID=0, assertz(curr_equivalence_class_id(ID))). | |
109 | ||
110 | number_of_equivalence_classes(X) :- curr_equivalence_class_id(X). | |
111 | % a counter; to do: use extension(counter) | |
112 | increment_counter(C) :- | |
113 | (counter(D) -> C is D + 1,retract(counter(_)),assertz(counter(C));C is 0, | |
114 | assertz(counter(C))). | |
115 | reset_counter :- (counter(_) -> retract(counter(_));true),assertz(counter(0)). | |
116 | ||
117 | ||
118 | ||
119 | ||
120 | transition(State,TranEncoded,IndividualSig,Succ) :- | |
121 | transition(State,TranEncoded,Succ), | |
122 | transition_info(TranEncoded,_,_,IndividualSig). | |
123 | ||
124 | transition_info('-->'(FAction,Args), Name, Arity, Signature) :- | |
125 | transition_name_arity('-->'(FAction,Args),Name,Arity), %Arity is -(Arity+1), | |
126 | compute_signature(Name,Arity,Signature),!. | |
127 | transition_info(io(V,Channel,_Span),Name,Arity,Signature) :- | |
128 | csp_mode, | |
129 | atomic(Channel), length(V,Arity), Name = Channel, | |
130 | compute_signature(Name,Arity,Signature),!. | |
131 | transition_info(Action, Name, Arity, Signature) :- nonvar(Action), functor(Action,Name,Arity), | |
132 | compute_signature(Name,Arity,Signature),!. | |
133 | transition_info(_, Name, Arity, Signature) :- Name = 'err:', Arity = ('?'), Signature = 'err'. | |
134 | ||
135 | :- volatile transition_info/3. | |
136 | :- dynamic transition_info/3. | |
137 | ||
138 | retractall_transition_info :- | |
139 | retractall(transition_info(_,_,_)). | |
140 | ||
141 | % leuschel Jan 2013: I don't understand this piece of code below: | |
142 | compute_signature(Name, Arity, Signature) :- | |
143 | (transition_info(Name,Arity,Signature) -> | |
144 | true | |
145 | ; FS_cl = "/", | |
146 | /* Arity for operations that return a value is one less than it | |
147 | actually is: so that later predicates can test for a return | |
148 | value by the arity being a negative number; and being one less | |
149 | enables coping with returning operations with 0 arity. */ | |
150 | (Arity < 0 -> | |
151 | RealArity is (-Arity-1), Arrow_cl = "-->", | |
152 | number_codes(1, Return_Len), | |
153 | LP_cl = "(", RP_cl = ")" | |
154 | ; RealArity is Arity, Arrow_cl = [], | |
155 | Return_Len = [], LP_cl = [], RP_cl = []), | |
156 | atom_codes(Name, Nn), number_codes(RealArity, Aa), | |
157 | NnAa = [Nn, FS_cl, Aa], | |
158 | ent03r_flatten(NnAa, F_cl), | |
159 | RES = [F_cl, Arrow_cl, LP_cl, Return_Len, RP_cl], | |
160 | ent03r_flatten(RES, Flat_RES), atom_codes(Signature, Flat_RES), | |
161 | assertz(transition_info(Name,Arity,Signature))), | |
162 | !. | |
163 | ||
164 | % find the name and arity of a transition | |
165 | transition_name_arity('-->'(FAction,_), Name, Arity) :- nonvar(FAction), | |
166 | functor(FAction,Name,Arity),!. | |
167 | transition_name_arity(Action, Name, Arity) :- nonvar(Action), functor(Action,Name,Arity),!. | |
168 | transition_name_arity(_, Name, Arity) :- Name = 'err:', Arity = 'err'. | |
169 | ||
170 | % get the transition's arguments from it | |
171 | get_transition_arguments('-->'(FAction,_),Args) :- | |
172 | nonvar(FAction),FAction =.. [_|Args],!. | |
173 | get_transition_arguments(Action, Args) :- nonvar(Action), Action =.. [_|Args],!. | |
174 | get_transition_arguments(_, Args) :- Args = 'err'. | |
175 | ||
176 | ||
177 | % convert the transition's arguments to a list of Strings | |
178 | get_args_as_strings([],[]). | |
179 | get_args_as_strings([First|SecondPlus],[String|Tail]) :- | |
180 | translate_bvalue(First,String), | |
181 | get_args_as_strings(SecondPlus,Tail). | |
182 | ||
183 | % convert a list of atoms to a flat list of codes representing them separated | |
184 | % by a Delimitor string. | |
185 | convert_string_to_code_list(ListA, CodeListA, Delimitor) :- | |
186 | atom_codes(Delimitor,DelimitorCodeList), | |
187 | convert_string_to_code_list_helper(ListA, CodeListA,DelimitorCodeList). | |
188 | convert_string_to_code_list_helper([],[],_). | |
189 | convert_string_to_code_list_helper([H|T],[Hhh|Tt],DelimitorCodeList_) :- | |
190 | (T == [] -> | |
191 | DelimitorCodeList = [];DelimitorCodeList = DelimitorCodeList_), | |
192 | atom_codes(H,Hh),append(Hh,DelimitorCodeList,Hhh), | |
193 | convert_string_to_code_list_helper(T,Tt,DelimitorCodeList). | |
194 | ||
195 | % get the alphabet for the state space, for a particular graph type, taking into | |
196 | % account the "don't cares" for transitions. | |
197 | get_alphabet(GT, Alphabet) :- | |
198 | findall(Letter,(transition(_,L,_), %transition_for_user(L,LU), | |
199 | remove_transition_arg_dont_cares(GT,L,Letter)),Alphabet_), | |
200 | remove_dups(Alphabet_,Alphabet). | |
201 | ||
202 | ||
203 | % get the signatures of alphabet for the state space. | |
204 | get_alphabet_signatures(Alphabet) :- | |
205 | findall(Letter,(transition(_,L,_),transition_info(L,_,_,Letter)),Alphabet_),remove_dups(Alphabet_,Alphabet). | |
206 | ||
207 | ||
208 | :- volatile transition_arg_dont_cares/3. | |
209 | :- dynamic transition_arg_dont_cares/3. | |
210 | ||
211 | retractall_transition_arg_dont_cares :- | |
212 | retractall(transition_arg_dont_cares(_,_,_)). | |
213 | ||
214 | ||
215 | % make a list of size, Length containing ascending integers, except at indices | |
216 | % specified by DontCares, where the element is a '_'. Result is List. | |
217 | make_counting_list(Length,DontCares,List) :- | |
218 | make_counting_list(0,Length,DontCares,List). | |
219 | make_counting_list(End,End,_,[]) :- !. | |
220 | make_counting_list(Counter,Length,DontCares,[Head|Tail]) :- | |
221 | (member(Counter,DontCares) -> | |
222 | Head = '_' | |
223 | ; Head is Counter), | |
224 | CounterAddOne is (Counter + 1), | |
225 | make_counting_list(CounterAddOne,Length,DontCares,Tail). | |
226 | ||
227 | % Assert "don't cares" format for a transition: '_' => don't care, and | |
228 | % anything but this implies that we're intested in this element: GT is the | |
229 | % type of graph we're asserting for. | |
230 | assert_transition_dont_cares(GT,TransitionSig, DontCareIndices) :- | |
231 | retractall(transition_arg_dont_cares(GT,TransitionSig,_)), | |
232 | assertz(transition_arg_dont_cares(GT,TransitionSig, DontCareIndices)). | |
233 | ||
234 | % Assert that all arguments of all UNKNOWN transitions are not cared about - | |
235 | % so this can be used to set dont cares for new transitions of the state space, | |
236 | % without changing current dont cares. | |
237 | assert_all_transition_arg_dont_cares :- | |
238 | ? | graph_type(GT), |
239 | transition(_,Trans,_),transition_info(Trans,_,ArgsLength,Sig), | |
240 | (transition_arg_dont_cares(GT,Sig,_) -> fail;true), | |
241 | % check if argslength is < 0, then add one if it is. | |
242 | ((ArgsLength < 0) -> | |
243 | ArgLength is (-ArgsLength-1) | |
244 | ; ArgLength is ArgsLength), | |
245 | make_counting_list(ArgLength,[],DontCares), | |
246 | make_counting_list(ArgLength,DontCares,ArgFormat), | |
247 | assert_transition_dont_cares(GT,Sig,ArgFormat),fail. | |
248 | assert_all_transition_arg_dont_cares. | |
249 | ||
250 | % Assert that ALL arguments of ALL transitions are not cared about - | |
251 | % this writes over whatever dont cares had been set before. | |
252 | assert_all_transition_arg_dont_cares(ignore_previous_dont_cares) :- | |
253 | retractall_transition_arg_dont_cares, | |
254 | graph_type(GT), | |
255 | transition(_,Trans,_),transition_info(Trans,_,ArgsLength,Sig), | |
256 | % check if argslength is < 0, then add one if it is. | |
257 | ((ArgsLength < 0) -> | |
258 | ArgLength is (-ArgsLength-1) | |
259 | ; ArgLength is ArgsLength), | |
260 | make_counting_list(ArgLength,[],DontCares), | |
261 | make_counting_list(ArgLength,DontCares,ArgFormat), | |
262 | assert_transition_dont_cares(GT,Sig,ArgFormat),fail. | |
263 | assert_all_transition_arg_dont_cares(ignore_previous_dont_cares). | |
264 | ||
265 | % predicate to filter out the arguments from a transition we don't care about. | |
266 | remove_transition_arg_dont_cares(_GT, Tran, FilteredTran) :- | |
267 | csp_mode, Tran = io(V,Ch,_),!, | |
268 | length(V,Len), gen_underscores(Len,US), | |
269 | FilteredTran =.. [Ch|US]. | |
270 | remove_transition_arg_dont_cares(GT, Tran, FilteredTran) :- | |
271 | get_transition_arguments(Tran,Args),transition_info(Tran,N,Arity,Sig), | |
272 | atom_codes(N,Name), | |
273 | transition_arg_dont_cares(GT,Sig,DontCares), | |
274 | get_args_as_strings(Args,ArgsS), | |
275 | remove_transition_arg_dont_cares3(DontCares,ArgsS,Filtered), | |
276 | convert_string_to_code_list(Filtered,FilteredStrings,','), | |
277 | (Arity < 0 -> | |
278 | atom_codes('-->(1)',Arrow_cl) | |
279 | ; Arrow_cl = []),atom_codes('(',LP),atom_codes(')',RP), | |
280 | ent03r_flatten([Name,LP,FilteredStrings,RP,Arrow_cl],FilteredTranCodeList), | |
281 | atom_codes(FilteredTranName,FilteredTranCodeList), | |
282 | FilteredTranName = FilteredTran. % put unification afterwards in case FilteredTran is already instantiated and not atomic | |
283 | ||
284 | gen_underscores(0,R) :- !,R=[]. | |
285 | gen_underscores(N,['_'|T]) :- N1 is N-1, gen_underscores(N1,T). | |
286 | % given 3 lists, DontCares, Original, Result, put each element of Original | |
287 | % into the same index in Result, unless the same element in DontCares is '_', in | |
288 | % which case put '_' in Result. | |
289 | remove_transition_arg_dont_cares3([],[],[]) :- !. | |
290 | remove_transition_arg_dont_cares3(['_'|Tail1], [_|Tail2], ['_'|Rest]) :- | |
291 | !, remove_transition_arg_dont_cares3(Tail1,Tail2,Rest). | |
292 | remove_transition_arg_dont_cares3([_|Tail1], [G|Tail2], [G|Rest]) :- | |
293 | !, remove_transition_arg_dont_cares3(Tail1,Tail2,Rest). | |
294 | ||
295 | :- volatile desired_user_transition/2. | |
296 | :- dynamic desired_user_transition/2. | |
297 | ||
298 | % Assert that the user wants to see all of the transitions in the alphabet, and | |
299 | % remove information stored about transition argument dont cares. (use on loading machine). | |
300 | assert_desired_user_transitions(alphabet) :- | |
301 | retractall(desired_user_transition(_,_)), | |
302 | retractall_transition_info,retractall_transition_arg_dont_cares, | |
303 | assert_all_transition_arg_dont_cares,get_alphabet_signatures(Ab),/* print(Ab),nl, */ | |
304 | ? | graph_type(GT),member(X,Ab), |
305 | assertz(desired_user_transition(GT,X)),fail. | |
306 | assert_desired_user_transitions(alphabet). | |
307 | ||
308 | % Assert that the user wants to see all of the transitions in the alphabet. | |
309 | assert_desired_user_transitions(only_alphabet) :- | |
310 | retractall(desired_user_transition(_,_)),get_alphabet_signatures(Ab), | |
311 | graph_type(GT),member(X,Ab), | |
312 | assertz(desired_user_transition(GT,X)),fail. | |
313 | assert_desired_user_transitions(only_alphabet). | |
314 | ||
315 | % Assert that the user wants to see all of the transitions in the alphabet, for | |
316 | % a particular graph type. | |
317 | assert_desired_user_transitions(GT,only_alphabet) :- | |
318 | retractall(desired_user_transition(GT,_)),get_alphabet_signatures(Ab), | |
319 | graph_type(GT),member(X,Ab), | |
320 | assertz(desired_user_transition(GT,X)),fail. | |
321 | assert_desired_user_transitions(_,only_alphabet). | |
322 | ||
323 | ||
324 | :- dynamic goal_nodes/1. | |
325 | ||
326 | :- use_module(probsrc(model_checker),[node_satisfies_goal/1]). | |
327 | assert_goal_nodes :- | |
328 | retractall(goal_nodes(_)),findall(X,(visited_expression_id(X), | |
329 | node_satisfies_goal(X)),R),sort(R,Rr),assertz(goal_nodes(Rr)). | |
330 | ||
331 | ||
332 | :- dynamic use_all_operations/2,use_no_arguments/2,user_has_made_op_selection/1, | |
333 | user_has_made_arg_selection/1. | |
334 | reset_use_all_ops_args :- | |
335 | retractall(use_all_operations(_,_)), | |
336 | retractall(use_no_arguments(_,_)), | |
337 | retractall(user_has_made_op_selection(_)), | |
338 | retractall(user_has_made_arg_selection(_)), | |
339 | assertz(use_all_operations(signature_merge,yes)), | |
340 | assertz(use_no_arguments(signature_merge,yes)), | |
341 | assertz(use_all_operations(dfa_abstraction,yes)), | |
342 | assertz(use_no_arguments(dfa_abstraction,yes)), | |
343 | assertz(user_has_made_op_selection(no)), | |
344 | assertz(user_has_made_arg_selection(no)). | |
345 | ||
346 | user_made_op_selection :- | |
347 | (user_has_made_op_selection(yes) -> | |
348 | true | |
349 | ; retractall(user_has_made_op_selection(no)),print('change just made'),nl, | |
350 | assertz(user_has_made_op_selection(yes))). | |
351 | user_made_arg_selection :- | |
352 | (user_has_made_arg_selection(yes) -> | |
353 | true | |
354 | ; retractall(user_has_made_arg_selection(no)), | |
355 | assertz(user_has_made_arg_selection(yes))). | |
356 | ||
357 | set_use_all_operations(Type, Yes) :- | |
358 | retractall(use_all_operations(Type,_)), | |
359 | ((Yes == yes) -> | |
360 | assertz(use_all_operations(Type,yes)), | |
361 | assert_desired_user_transitions(Type,only_alphabet) | |
362 | ; assertz(use_all_operations(Type,no))). | |
363 | set_use_no_arguments(Type, Yes) :- | |
364 | retractall(use_no_arguments(Type,_)), | |
365 | ((Yes == yes) -> | |
366 | assertz(use_no_arguments(Type,yes)), | |
367 | assert_all_transition_arg_dont_cares(ignore_previous_dont_cares) | |
368 | ; assertz(use_no_arguments(Type,no))). | |
369 | ||
370 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
371 | End utility functions | |
372 | ==============================================================================*/ | |
373 | ||
374 | ||
375 | ||
376 | /*============================================================================== | |
377 | DFA minimisation applied and modified to prob state space graphs | |
378 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ | |
379 | ||
380 | :- use_module(library(ordsets)). | |
381 | ||
382 | :- dynamic distinguished/3,table_marked/1,equivalence_clazz/1,dfa_states_/2, | |
383 | dfa_tran_/3,final_states/1,min_dfa_state/2. | |
384 | ||
385 | dfa_cleanup :- | |
386 | retractall(equivalence_clazz(_)),retractall(distinguished(_,_,_)), | |
387 | retractall(table_marked(_)),retractall(min_dfa_state(_,_)). | |
388 | ||
389 | init :- | |
390 | dfa_cleanup,assertz(table_marked(no)),get_dfa_states(States),init(States). | |
391 | ||
392 | init([_|[]]). | |
393 | init([H|T]) :- | |
394 | setup_distinguished_table(H, T), | |
395 | init(T). | |
396 | ||
397 | setup_distinguished_table(_, []). | |
398 | setup_distinguished_table(X, [H|T]) :- | |
399 | final_states(Final_States), | |
400 | (((member(X, Final_States), \+member(H, Final_States)) | (\+member(X, Final_States), member(H, Final_States))) -> | |
401 | assertz(distinguished(X,H,yes)),retractall(table_marked(_)), assertz(table_marked(yes)) | |
402 | ; assertz(distinguished(X,H,no))), | |
403 | setup_distinguished_table(X,T). | |
404 | ||
405 | ||
406 | construct_distinguished_table :- | |
407 | distinguished(A,B,no), | |
408 | dfa_tran_(A,X,Aprime), | |
409 | dfa_tran_(B,X,Bprime), | |
410 | %print('('),print(A),print(','),print(B),print(' = no)'),print(' '),print(X),print(' ('),print(Aprime),print(','),print(Bprime),print(')'),nl, | |
411 | ((distinguished(Aprime,Bprime, yes) | distinguished(Bprime,Aprime,yes)) -> | |
412 | retract(distinguished(A,B,_)), assertz(distinguished(A,B, yes)), | |
413 | retractall(table_marked(_)), assertz(table_marked(yes)) | |
414 | ,print(A),print(' '),print(B),print(' '),print(yes),nl | |
415 | ;true), | |
416 | fail. | |
417 | construct_distinguished_table :- | |
418 | (table_marked(yes) -> | |
419 | retractall(table_marked(_)), assertz(table_marked(no)), construct_distinguished_table;true). | |
420 | ||
421 | assert_equivalence_clazz(Class, []) :- | |
422 | ((\+equivalence_clazz(Class),equivalence_clazz(Any),ord_intersection(Class,Any,[])) | |
423 | -> assertz(equivalence_clazz(Class)) | |
424 | ; true). | |
425 | assert_equivalence_clazz(Class, [H|T]) :- | |
426 | ((ord_intersection(Class, H, [_|_]) -> | |
427 | ord_union(Class, H, Res),assert_equivalence_clazz(Res, T)) | |
428 | ; assert_equivalence_clazz(Class, T)). | |
429 | ||
430 | assert_equivalence_clazzes_([]). | |
431 | assert_equivalence_clazzes_([H|T]) :- | |
432 | assert_equivalence_clazz(H, T), | |
433 | assert_equivalence_clazzes_(T). | |
434 | ||
435 | assert_equivalence_clazzes :- | |
436 | findall([X,Y],distinguished(X,Y,'no'),Res), | |
437 | sort(Res, Result), | |
438 | assert_equivalence_clazzes_(Result), | |
439 | fail. | |
440 | assert_equivalence_clazzes. | |
441 | ||
442 | unflatten([], []). | |
443 | unflatten([H|T], [[H]|Res]) :- | |
444 | unflatten(T, Res). | |
445 | ||
446 | minimize_dfa(FullResult) :- | |
447 | init, construct_distinguished_table, assert_equivalence_clazzes, | |
448 | findall(X,equivalence_clazz(X),ReS),% retractall(equivalence_clazz(_)), | |
449 | findall([X,Y],distinguished(X,Y,'yes'),Result), | |
450 | %print(Result),nl, | |
451 | ent03r_flatten(Result, Flat_Re),remove_dups(Flat_Re, Resu), | |
452 | sort(Resu, Result_), | |
453 | %print('*'),print(Result_),nl, | |
454 | ent03r_flatten(ReS, Flat_Res),sort(Flat_Res,Flat_Res_), | |
455 | %print(Flat_Res_),nl, | |
456 | length(Result_,LR),length(Flat_Res_,FR), | |
457 | (LR =< FR -> | |
458 | ord_intersection(Result_, Flat_Res_,_,Diff) | |
459 | ; ord_intersection(Flat_Res_, Result_,_,Diff)), | |
460 | %print(Diff),nl, | |
461 | unflatten(Diff, Fat_Diff),append(ReS, Fat_Diff, FullResult),assert_min_dfa_states(FullResult). | |
462 | ||
463 | get_representative_from_list(L,Representative) :- | |
464 | member(Representative, L),!. | |
465 | ||
466 | assert_min_dfa_states([]). | |
467 | assert_min_dfa_states([H|T]) :- | |
468 | get_representative_from_list(H,Represen), | |
469 | assertz(min_dfa_state(H,Represen)), | |
470 | assert_min_dfa_states(T). | |
471 | ||
472 | print_min_dfa_states_representatives_for_dot :- | |
473 | min_dfa_state(_,ID), | |
474 | map_dfa_state_to_id(RealRep,ID), | |
475 | (RealRep == [] -> fail;true), | |
476 | (RealRep == [root] -> | |
477 | print(ID),print('[shape=invtriangle, color=green, label=""];'),nl,fail %"#0d9d03" | |
478 | ; print(ID), print('[shape=ellipse, color=black, label=\"'),print(ID), | |
479 | print('\", id='),print(ID),print('];'),nl,fail). | |
480 | print_min_dfa_states_representatives_for_dot. | |
481 | ||
482 | print_min_dfa__representatives_transitions_ :- | |
483 | min_dfa_state(_,Representative), | |
484 | dfa_tran_(Representative,Letter,Succ), | |
485 | min_dfa_state(State,SuccRepresentative), | |
486 | ||
487 | map_dfa_state_to_id(RealRep,Representative), | |
488 | RealRep \== [], | |
489 | map_dfa_state_to_id(RealSuccRep,SuccRepresentative), | |
490 | RealSuccRep \== [], | |
491 | ||
492 | member(Succ,State), | |
493 | print(Representative), | |
494 | print(' -> '), | |
495 | print(SuccRepresentative), | |
496 | (RealRep == [root] -> | |
497 | print('[style=dotted, color=black, label=\"') | |
498 | ; print('[color=blue, label=\"')), | |
499 | print(Letter), | |
500 | print('\"];'), | |
501 | nl, | |
502 | fail. | |
503 | print_min_dfa__representatives_transitions_. | |
504 | ||
505 | print_min_dfa_for_dot(File) :- | |
506 | nfa_to_dfa, | |
507 | minimize_dfa(_), | |
508 | % for each min_dfa_state, get a representative state, for each letter of the alphabet, print the transition | |
509 | % and the representative state to which the transition leads | |
510 | tell(File), | |
511 | print_graph_header(minimum_dfa), | |
512 | print_min_dfa_states_representatives_for_dot, | |
513 | print_min_dfa__representatives_transitions_, | |
514 | print_graph_footer, | |
515 | told. | |
516 | print_min_dfa_for_dot(_). | |
517 | ||
518 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
519 | End DFA minimisation | |
520 | ==============================================================================*/ | |
521 | ||
522 | /*============================================================================== | |
523 | NFA to DFA | |
524 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ | |
525 | ||
526 | % Use this to find out about all of the transitions - instead of using transition/3 directly. This predicate filters | |
527 | % out transitions which the user isn't interested in. | |
528 | nfa_to_dfa_transition_filter(A,B,Sig,D) :- | |
529 | transition(A,B,D), | |
530 | transition_info(B,_,_,SmallSig), | |
531 | remove_transition_arg_dont_cares(dfa_abstraction, B, Sig), | |
532 | desired_user_transition(dfa_abstraction,SmallSig). | |
533 | ||
534 | :- volatile transi_/2,map_dfa_state_to_id/2. | |
535 | :- dynamic transi_/2,map_dfa_state_to_id/2. | |
536 | findall_transitions(State,TransName,_) :- | |
537 | nfa_to_dfa_transition_filter(State,_,TransName,Succ), | |
538 | (transi_(State,Succ) -> | |
539 | true | |
540 | ; asserta(transi_(State,Succ))), | |
541 | fail. | |
542 | findall_transitions(State,_,Result) :- | |
543 | findall(Succ,transi_(State,Succ),Result),retractall(transi_(_,_)). | |
544 | ||
545 | nfa_cleanup :- | |
546 | retractall(dfa_states_(_,_)),retractall(dfa_tran_(_,_,_)), | |
547 | retractall(final_states(_)),retractall(map_dfa_state_to_id(_,_)). | |
548 | ||
549 | move_([],_,[]). | |
550 | move_([Head|Tail],T,R) :- | |
551 | move_(Head,T,R1), | |
552 | move_(Tail,T,R2),ent03r_union(R1,R2,R). | |
553 | move_(S,T,R) :- | |
554 | findall_transitions(S,T,R). | |
555 | move(S,T,R) :- move_(S,T,Rp), | |
556 | retractall(transi_(_,_)),ent03r_flatten(Rp,R),!. | |
557 | ||
558 | nfa_to_dfa_worker(Alphabet) :- | |
559 | repeat, | |
560 | (dfa_states_(S,no) -> true;!,fail), | |
561 | %print('testing S = '),print(S),nl, | |
562 | retract(dfa_states_(S,no)), | |
563 | asserta(dfa_states_(S,yes)), | |
564 | % print(treating_dfa_state(S)),nl, | |
565 | (map_dfa_state_to_id(S,_) -> | |
566 | true | |
567 | ; next_equivalence_class_id(ID0), | |
568 | % print(new_equiv_class(ID0)),nl, | |
569 | asserta(map_dfa_state_to_id(S,ID0))), | |
570 | %print('*'), | |
571 | member(Letter,Alphabet), | |
572 | % print(computing_move(S,Letter)),nl, | |
573 | move(S,Letter,Res), | |
574 | sort(Res,Result), | |
575 | % print(move(S,Letter,Res)),nl, | |
576 | (dfa_states_(Result,_) -> | |
577 | true /* state already exists */ | |
578 | ; asserta(dfa_states_(Result,no)), % register new, untreated state | |
579 | % print(new_successor_state(Result)),nl, | |
580 | (map_dfa_state_to_id(Result,_) -> | |
581 | true | |
582 | ; next_equivalence_class_id(ID1), | |
583 | % print(new_equiv_class(ID1)),nl, | |
584 | asserta(map_dfa_state_to_id(Result,ID1)))), | |
585 | %print('asserting '),print(Result),nl), | |
586 | map_dfa_state_to_id(S,ID2), | |
587 | map_dfa_state_to_id(Result,ID3), | |
588 | % print(dfa_tran(ID2,Letter,ID3)),nl, | |
589 | asserta(dfa_tran_(ID2,Letter,ID3)),fail. | |
590 | nfa_to_dfa_worker(_). | |
591 | ||
592 | get_dfa_states(States) :- | |
593 | findall(S,map_dfa_state_to_id(_,S),Statess), | |
594 | sort(Statess,States). | |
595 | ||
596 | ||
597 | ||
598 | nfa_to_dfa :- | |
599 | nfa_cleanup, | |
600 | init_equivalence_class_id, | |
601 | /* findall(X,desired_user_transition(dfa_abstraction,X),Alphabet), */ | |
602 | get_alphabet(dfa_abstraction,Alphabet), | |
603 | print('% Alphabet: '), print(Alphabet),nl, | |
604 | asserta(dfa_states_([root],no)), | |
605 | nfa_to_dfa_worker(Alphabet). | |
606 | nfa_to_dfa :- | |
607 | get_dfa_states(States), | |
608 | map_dfa_state_to_id([root],ID1), | |
609 | (map_dfa_state_to_id([],ID2) -> | |
610 | List = [ID2,ID1], %add other final states here | |
611 | sort(List,SList), | |
612 | ord_subtract(States,SList,Finals) | |
613 | ; ord_subtract(States,[ID1],Finals)), | |
614 | ||
615 | assertz(final_states(Finals)). | |
616 | ||
617 | ||
618 | ||
619 | print_dfa_from_nfa_states_id :- | |
620 | map_dfa_state_to_id(Reals,ID), | |
621 | ((Reals == []) -> fail;true), | |
622 | ||
623 | % work out outline colour | |
624 | ((member(A,Reals),transition(A,_,_)) -> % this node not is open (**in this dfa graph) | |
625 | get_preference(dot_normal_node_colour,OutColour) | |
626 | ; get_preference(dot_open_node_colour,OutColour)), % this node is open | |
627 | ||
628 | % work out fill colour | |
629 | ((invariant_violated(C), member(C,Reals)) -> | |
630 | get_preference(dot_invariant_violated_node_colour,InColour) | |
631 | ; true), | |
632 | ||
633 | % work out shape | |
634 | ((Reals == [root]) -> % its the root | |
635 | get_preference(dot_root_shape,Shape), | |
636 | print(root),print('[id="root", shape='),print(Shape),print(', color=green, label=""];'),nl,fail | |
637 | ; ((state_space:current_state_id(B),member(B,Reals)) -> % it contains the current state | |
638 | get_preference(dot_current_node_shape,Shape) | |
639 | ; get_preference(dot_normal_node_shape,Shape))), % it doesn't contain the current state | |
640 | ||
641 | % do the printing | |
642 | print(ID),print('[id='),print(ID),print(', shape='),print(Shape),print(', color=\"'),print(OutColour),print('\"'), | |
643 | (nonvar(InColour) -> print(', style=filled, fillcolor='),print(InColour); true),print('];'),nl, | |
644 | fail. | |
645 | print_dfa_from_nfa_states_id. | |
646 | ||
647 | print_dot_for_dfa_from_nfa_ :- | |
648 | dfa_tran_(ID1,Letter,ID2), | |
649 | map_dfa_state_to_id(ID1_reals, ID1), | |
650 | map_dfa_state_to_id(ID2_reals, ID2), | |
651 | ((ID2_reals == []) -> fail;true), | |
652 | ((ID1_reals == [root]) -> | |
653 | print(root) | |
654 | ; print(ID1)), | |
655 | print(' -> '), | |
656 | print(ID2), | |
657 | (map_dfa_state_to_id([root], ID1) -> | |
658 | print('[color=black, label=\"') %style=dotted, | |
659 | ; ((ID1_reals \== ID2_reals,ord_subset(ID2_reals, ID1_reals)) -> | |
660 | print('[style=dotted,') | |
661 | ; print('[')), | |
662 | print('color=blue, label=\"')), | |
663 | print(Letter), | |
664 | print('\"];'), | |
665 | nl, | |
666 | fail. | |
667 | print_dot_for_dfa_from_nfa_. | |
668 | ||
669 | print_dot_for_dfa_from_nfa(File) :- | |
670 | % use all operations if desired | |
671 | (use_all_operations(dfa_abstraction,yes) -> | |
672 | set_use_all_operations(dfa_abstraction,yes) | |
673 | ; true), | |
674 | % use no arguments if desired | |
675 | (use_no_arguments(dfa_abstraction,yes) -> | |
676 | set_use_no_arguments(dfa_abstraction,yes) | |
677 | ; true), | |
678 | print('% Converting NFA to DFA'),nl, | |
679 | nfa_to_dfa, | |
680 | number_of_equivalence_classes(Nr), | |
681 | format('% Writing DFA with ~w states to file: ~w~n',[Nr,File]), | |
682 | tell(File), | |
683 | print_graph_header(nfa_to_dfa), | |
684 | print_dfa_from_nfa_states_id, | |
685 | nl, | |
686 | print_dot_for_dfa_from_nfa_, | |
687 | print_graph_footer, | |
688 | told, | |
689 | (Nr>100 -> format('% Warning: viewing ~w states with dot can take time!~n',[Nr]) ; true). | |
690 | ||
691 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
692 | End of NFA to DFA code | |
693 | ==============================================================================*/ | |
694 | ||
695 | ||
696 | ||
697 | /*============================================================================== | |
698 | Signature Merge based on a state's transitions | |
699 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ | |
700 | ||
701 | :- dynamic counter/1,state_signature/4, | |
702 | state_merge_equivalence_class/3,transition_printed/1,state_printed/1, | |
703 | %state_merge_filter_mode/1, | |
704 | state_merge_separate_invariant_violations/1,non_det_trans/3, | |
705 | signature_merge_show_all_transitions/1,non_def_trans/2. | |
706 | ||
707 | % Either no or yes. The former means we don't separate states that break the | |
708 | % invariant violation into their own equivalence class. The latter means we do. | |
709 | state_merge_separate_invariant_violations(no). | |
710 | ||
711 | % Either no or yes. The former means we don't view every outgoing transition for | |
712 | % each equivalence class. The latter means we do. | |
713 | signature_merge_show_all_transitions(yes). | |
714 | ||
715 | set_signature_merge_show_all_transitions(H) :- | |
716 | (signature_merge_show_all_transitions(H) -> | |
717 | true | |
718 | ; retractall(signature_merge_show_all_transitions(_)), | |
719 | assertz(signature_merge_show_all_transitions(H))). | |
720 | ||
721 | %state_merge_separate_iviolations(V) :- | |
722 | % (((V == yes) ; (V == no)) -> | |
723 | % retractall(state_merge_separate_invariant_violations(_)), | |
724 | % assertz(state_merge_separate_invariant_violations(V)) | |
725 | % ; print('invalid state_merge_separate_iviolations/1 mode: '),print(V), | |
726 | % print(' should be either, yes, or no'),nl). | |
727 | ||
728 | % Either normal ==> perform reduction on original state space | |
729 | % OR nfa_to_dfa ==> perform reduction on state space outputted from nfa_to_dfa function | |
730 | % NB: SPELL YOUR OPTION CORRECTLY OR GET WEIRD RESULTS! | |
731 | %state_merge_filter_mode(normal). | |
732 | ||
733 | % clean up the database | |
734 | cleanup_state_merge :- | |
735 | retractall(state_signature(_,_,_,_)),retractall(state_merge_equivalence_class(_,_,_)), | |
736 | retractall(counter(_)), | |
737 | retractall(non_det_trans(_,_,_)), | |
738 | retractall(non_def_trans(_,_)) | |
739 | /*,retractall(desired_user_transition(_,_))*/. | |
740 | ||
741 | % get the transitions: take care that we regard the different modes | |
742 | state_merge_transition_filter(A,B,Sig,D) :- | |
743 | transition(A,B,D),transition_info(B,_,_,Sig), | |
744 | desired_user_transition(signature_merge,Sig). | |
745 | ||
746 | % get the states: take care that we regard the different modes | |
747 | state_merge_state_filter(A,B,B) :- visited_expression(A,B). | |
748 | ||
749 | % assert the transitions stemming from each state | |
750 | assert_state_merges :- | |
751 | state_merge_state_filter(ID,State,_), | |
752 | compute_signature_for_state(ID,State,Res), | |
753 | % check whether to separate each invariant violation in it's own | |
754 | % equivalence class. | |
755 | (state_merge_separate_invariant_violations(no) -> | |
756 | assert_state_signature(ID,Res,ok) | |
757 | ; (invariant_violated(ID) -> | |
758 | assert_state_signature(ID,Res,invariant_violated) | |
759 | ; assert_state_signature(ID,Res,ok))), | |
760 | fail. | |
761 | assert_state_merges. | |
762 | ||
763 | assert_state_signature(ID,Signature,OK) :- | |
764 | (state_merge_equivalence_class(Signature,ClassID,OK) | |
765 | -> true | |
766 | ; increment_counter(ClassID), | |
767 | assertz(state_merge_equivalence_class(Signature,ClassID,OK)) | |
768 | ), | |
769 | assertz(state_signature(ID,Signature,OK,ClassID)). | |
770 | ||
771 | %:- dynamic observing_variable/1. | |
772 | /* set this predicate if we want to observe a particular variable instead of the signature */ | |
773 | %observing_variable('display_st'). | |
774 | ||
775 | %compute_signature_for_state(_,State,Res) :- | |
776 | % observing_variable(Var),store:lookup_value(Var,State,Val),!, Res=Val. | |
777 | compute_signature_for_state(ID,_,Res) :- | |
778 | findall(Tr,state_merge_transition_filter(ID,_,Tr,_),Res_), | |
779 | sort(Res_,Res). | |
780 | ||
781 | % find out the state equivalence class for a given state | |
782 | find_state_merge_equivalence_class_for_state(State,ClassID) :- | |
783 | state_signature(State,_TransSig,_Status,ClassID),!. | |
784 | ||
785 | % find out a state corresponding to a given equivalence class | |
786 | find_state_for_state_merge_equivalence_class(ClassID,State) :- | |
787 | state_signature(State,_SIG,_OK,ClassID). | |
788 | ||
789 | % apply the state merge algorithm | |
790 | state_merge :- | |
791 | cleanup_state_merge, | |
792 | % work on the correct state space e.g. the original one as opposed to | |
793 | % one outputted by another algorithm | |
794 | /*assert_desired_user_transitions,*/ | |
795 | print_message('Computing Signatures'), | |
796 | assert_state_merges. | |
797 | ||
798 | % the state merge state's colour | |
799 | state_merge_state_colour(State, Colour) :- | |
800 | (state_merge_equivalence_class([],State,_) -> | |
801 | get_preference(dot_open_node_colour,Colour) | |
802 | ; get_preference(dot_normal_node_colour,Colour)). | |
803 | ||
804 | % print a state's id for the state merge - print 'root' for this if the id maps to the root | |
805 | print_state_merge_state_id(State) :- | |
806 | (find_state_merge_equivalence_class_for_state(root,State) -> print(root) | |
807 | ; print(State)). | |
808 | ||
809 | % print a transition for dot | |
810 | print_transition_for_dot(A,IndividualSig,C) :- Trans = [A,IndividualSig,C], | |
811 | (transition_printed(Trans) -> | |
812 | true | |
813 | ; assertz(transition_printed(Trans)), | |
814 | print_state_merge_state_id(A),print('->'),print(C), | |
815 | (find_state_merge_equivalence_class_for_state(root, A) -> | |
816 | /* Style = 'solid', Color='blue' % dealing with the root */ | |
817 | (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
818 | Style = 'dotted' % there's more than one of these transitions | |
819 | ; Style = 'solid'), | |
820 | (non_def_trans(A,IndividualSig) -> | |
821 | Color = 'purple';Color = 'black') | |
822 | ; (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
823 | Style = 'dotted' % there's more than one of these transitions | |
824 | ; Style = 'solid'), | |
825 | (non_def_trans(A,IndividualSig) -> | |
826 | Color = 'purple';Color = 'blue')), | |
827 | print('[style='),print(Style),print(', color=\"'),print(Color), | |
828 | print('\", label=\"'),print(IndividualSig),print('\"];'),nl). | |
829 | ||
830 | % print a state for dot | |
831 | print_class_as_dotstate(ClassID,OK) :- | |
832 | (state_printed(ClassID) -> | |
833 | true | |
834 | ; assertz(state_printed(ClassID)), | |
835 | state_merge_state_colour(ClassID, StateColour), | |
836 | get_preference(dot_invariant_violated_node_colour,IColor), | |
837 | print_state_merge_state_id(ClassID), | |
838 | print(' ['), | |
839 | (find_state_merge_equivalence_class_for_state(root,ClassID) -> | |
840 | print('shape=invtriangle, color=green, '), | |
841 | print('label=\"\", id=\"'),print(root) | |
842 | ; ((OK = invariant_violated) -> | |
843 | print('shape=ellipse, style=filled, fillcolor="'), | |
844 | print(IColor),print('\", label=\"'), | |
845 | print_node_label(ClassID),print('\" , id=\"'),print_node_label(ClassID) | |
846 | ; print('shape=ellipse, color=\"'),print(StateColour),print('\", label=\"'), | |
847 | print_node_label(ClassID),print('\" , id=\"'),print_node_label(ClassID))), | |
848 | print('\"];'),nl). | |
849 | ||
850 | print_node_label(ClassID) :- | |
851 | (preference(dot_print_node_ids,false) | |
852 | -> state_merge_equivalence_class(Signature,ClassID,_OK), | |
853 | print(Signature) | |
854 | ; preference(dot_print_node_info,true) | |
855 | -> state_merge_equivalence_class(Signature,ClassID,_OK), | |
856 | print(ClassID),print('\\n'), print(Signature) | |
857 | ; print(ClassID) | |
858 | ). | |
859 | ||
860 | % print the merged states | |
861 | print_state_merge_states_for_dot :- | |
862 | state_merge_equivalence_class(_,ClassID,OK), | |
863 | print_class_as_dotstate(ClassID,OK),fail. | |
864 | print_state_merge_states_for_dot. | |
865 | ||
866 | % assert whether there is more than one transition from an equivalence class | |
867 | % with the same label. | |
868 | assert_non_det_trans(_State,StateID,IndividualTransSignature,_To1ID) :- | |
869 | non_det_trans(StateID,IndividualTransSignature,_Status),!. % already computed | |
870 | assert_non_det_trans(State,StateID,TransSignature,To1ID) :- | |
871 | find_state_for_state_merge_equivalence_class(StateID,AnotherState), | |
872 | State \= AnotherState, | |
873 | \+ not_all_transitions_added(AnotherState), % this is an open node; not yet computed | |
874 | /* state_merge_transition_filter */ | |
875 | transition(AnotherState,_,TransSignature,To2), | |
876 | \+(find_state_merge_equivalence_class_for_state(To2,To1ID)),!, | |
877 | %print_message(non_det(StateID,TransSignature,To1ID,AnotherState,To2)), | |
878 | asserta(non_det_trans(StateID,TransSignature,true)). | |
879 | assert_non_det_trans(_State,StateID,IndividualTransSignature,_To1ID) :- | |
880 | assertz(non_det_trans(StateID,IndividualTransSignature,false)). | |
881 | ||
882 | % print the transitions of the merged states. | |
883 | print_state_merge_transitions_for_dot :- | |
884 | transition(State,_,IndividualSig,To), | |
885 | find_state_merge_equivalence_class_for_state(State,ID1), | |
886 | find_state_merge_equivalence_class_for_state(To,ID2), | |
887 | assert_non_det_trans(State,ID1,IndividualSig,ID2), | |
888 | (desired_user_transition(signature_merge,IndividualSig) -> | |
889 | print_transition_for_dot(ID1,IndividualSig,ID2) | |
890 | ; (signature_merge_show_all_transitions(yes) -> | |
891 | (non_def_trans(ID1,IndividualSig) -> | |
892 | true | |
893 | ; assertz(non_def_trans(ID1,IndividualSig))), | |
894 | print_transition_for_dot(ID1,IndividualSig,ID2) | |
895 | ; true) | |
896 | ), | |
897 | fail. | |
898 | print_state_merge_transitions_for_dot. | |
899 | ||
900 | % print the merged state graph for dot | |
901 | print_state_merge_for_dot :- | |
902 | % check if user has specified all transitions | |
903 | (use_all_operations(signature_merge,yes) -> | |
904 | set_use_all_operations(signature_merge,yes) | |
905 | ; true), | |
906 | clean_up_after_printing, | |
907 | print_message('Performing State Merge'), | |
908 | state_merge, | |
909 | print_graph_header(state_merge), | |
910 | print_message('Generating Dot States'), | |
911 | print_state_merge_states_for_dot, | |
912 | print_message('Generating Dot Transitions'), | |
913 | print_state_merge_transitions_for_dot, | |
914 | print_graph_footer. | |
915 | ||
916 | print_state_merge_for_dot(File) :- print_state_merge_for_dot2(File). | |
917 | print_state_merge_for_dot2(File) :- | |
918 | tell(File),print_state_merge_for_dot,told. | |
919 | ||
920 | ||
921 | % For ProB 2.0 Graphical Visualizations | |
922 | extract_graph_of_state_merge(Graph) :- | |
923 | % check if user has specified all transitions | |
924 | (use_all_operations(signature_merge,yes) -> | |
925 | set_use_all_operations(signature_merge,yes) | |
926 | ; true), | |
927 | clean_up_after_printing, | |
928 | print_message('Performing State Merge'), | |
929 | state_merge, | |
930 | print_message('Generating States'), | |
931 | extract_state_merge_states(States), | |
932 | print_message('Generating Transitions'), | |
933 | extract_state_merge_transitions(Transitions), | |
934 | Graph = [States,Transitions]. | |
935 | ||
936 | extract_state_merge_states(States) :- | |
937 | findall(State,extract_state_for_graph(State),States). | |
938 | ||
939 | extract_state_for_graph(State) :- | |
940 | state_merge_equivalence_class(Sig,Id,OK), | |
941 | State = state(Sig,Id,OK). | |
942 | ||
943 | extract_state_merge_transitions(Transitions) :- | |
944 | findall(Trans,extract_state_merge_transition(Trans),Transitions). | |
945 | ||
946 | extract_state_merge_transition(Transition) :- | |
947 | transition(State,_,IndividualSig,To), | |
948 | find_state_merge_equivalence_class_for_state(State,ID1), | |
949 | find_state_merge_equivalence_class_for_state(To,ID2), | |
950 | assert_non_det_trans(State,ID1,IndividualSig,ID2), | |
951 | (desired_user_transition(signature_merge,IndividualSig) -> | |
952 | extract_transition_representation(ID1,IndividualSig,ID2,Color,Style) | |
953 | ; (signature_merge_show_all_transitions(yes) -> | |
954 | (non_def_trans(ID1,IndividualSig) -> | |
955 | true | |
956 | ; assertz(non_def_trans(ID1,IndividualSig))), | |
957 | extract_transition_representation(ID1,IndividualSig,ID2,Color,Style) | |
958 | ; true) | |
959 | ), | |
960 | Transition = trans(ID1,IndividualSig,ID2,Color,Style). | |
961 | ||
962 | ||
963 | extract_transition_representation(A,IndividualSig,C,Color,Style) :- | |
964 | Trans = [A,IndividualSig,C], | |
965 | (transition_printed(Trans) -> | |
966 | fail | |
967 | ; assertz(transition_printed(Trans)), | |
968 | (find_state_merge_equivalence_class_for_state(root, A) -> | |
969 | /* Style = 'solid', Color='blue' % dealing with the root */ | |
970 | (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
971 | Style = 'dotted' % there's more than one of these transitions | |
972 | ; Style = 'solid'), | |
973 | (non_def_trans(A,IndividualSig) -> | |
974 | Color = 'purple';Color = 'black') | |
975 | ; (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
976 | Style = 'dotted' % there's more than one of these transitions | |
977 | ; Style = 'solid'), | |
978 | (non_def_trans(A,IndividualSig) -> | |
979 | Color = 'purple';Color = 'blue')) | |
980 | ). | |
981 | ||
982 | ||
983 | ||
984 | % clean up the database from assertions used during graph printing. | |
985 | clean_up_after_printing :- | |
986 | retractall(state_printed(_)),retractall(transition_printed(_)). | |
987 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
988 | End of signature merge reduction | |
989 | ==============================================================================*/ | |
990 | ||
991 | ||
992 | :- volatile things/1. | |
993 | :- dynamic things/1. | |
994 | assert_associated_nodes([]). | |
995 | assert_associated_nodes([H|T]) :- | |
996 | (things(H) -> | |
997 | assert_associated_nodes(T) | |
998 | ; assertz(things(H)),findall(X,transition(X,_,H),Res), | |
999 | append(T,Res,Ress),assert_associated_nodes(Ress)). | |
1000 | ||
1001 | check_against_list(_,[]). | |
1002 | check_against_list(Element,[H|T]) :- | |
1003 | (state_printed(Element) -> | |
1004 | true | |
1005 | ; assertz(state_printed(Element)), | |
1006 | visualize_graph:tcltk_print_node_for_dot(Element)), | |
1007 | /* (transition_printed([Element,H]) -> | |
1008 | true | |
1009 | ; assertz(transition_printed([Element,H])), */ | |
1010 | (transition(Element,_,H) -> visualize_graph:tcltk_print_transitions_for_dot(Element,H) | |
1011 | ; true), | |
1012 | check_against_list(Element,T). | |
1013 | ||
1014 | print_dot_from_node_list(_,File) :- | |
1015 | tell(File), | |
1016 | retractall(state_printed(_)), | |
1017 | retractall(transition_printed(_)), | |
1018 | print_graph_header(general_graph),fail. | |
1019 | print_dot_from_node_list(Llist,_) :- | |
1020 | sort(Llist,List), | |
1021 | member(N1,List), | |
1022 | check_against_list(N1,List),fail. | |
1023 | print_dot_from_node_list(_,_) :- | |
1024 | print_graph_footer,told. | |
1025 | ||
1026 | print_subgraph_associated_with_node(Node,File) :- | |
1027 | retractall(things(_)), | |
1028 | (is_list(Node) -> | |
1029 | assert_associated_nodes(Node) | |
1030 | ; assert_associated_nodes([Node])), | |
1031 | findall(X,reduce_graph_state_space:things(X),Result), | |
1032 | print_dot_from_node_list(Result,File). | |
1033 | ||
1034 | print_subgraph_associated_with_invariant_violations(File) :- | |
1035 | findall(X,invariant_violated(X),R),remove_dups(R,Rr), | |
1036 | print_subgraph_associated_with_node(Rr,File). | |
1037 | ||
1038 | print_subgraph_of_goal_nodes(File) :- | |
1039 | assert_goal_nodes,goal_nodes(L),print_dot_from_node_list(L,File). | |
1040 | ||
1041 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
1042 | End of Iterative Deepening search for a node | |
1043 | ==============================================================================*/ | |
1044 | ||
1045 | ||
1046 | ||
1047 | ||
1048 | ||
1049 |