1 | % (c) 2009-2019 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(tools). | |
44 | ||
45 | :- use_module(module_information,[module_info/2]). | |
46 | :- module_info(group,dot). | |
47 | :- module_info(description,'Various minimization/reduction algorithms for the state space.'). | |
48 | ||
49 | :- use_module(debug). | |
50 | ||
51 | :- use_module(library(lists)). | |
52 | %:- use_module(library(system)). | |
53 | :- use_module(preferences). | |
54 | %:- use_module(graph_canon). | |
55 | %:- use_module(library(terms)). | |
56 | ||
57 | :- use_module(visualize_graph,[print_graph_header/1, | |
58 | print_graph_footer/0]). | |
59 | :- use_module(state_space,[visited_expression/2, visited_expression_id/1, | |
60 | transition/3, store_transition/4, | |
61 | invariant_violated/1, not_all_transitions_added/1]). | |
62 | :- use_module(specfile,[csp_mode/0]). | |
63 | :- use_module(translate,[translate_bvalue/2]). | |
64 | ||
65 | reduce_graph_reset :- assert_desired_user_transitions(alphabet), | |
66 | reset_use_all_ops_args, reset_counter. | |
67 | ||
68 | :- use_module(eventhandling,[register_event_listener/3]). | |
69 | :- register_event_listener(clear_specification,reduce_graph_reset, | |
70 | 'Reset reduce_graph_state_space.'). | |
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 | assert(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 | assert(curr_equivalence_class_id(ID)) | |
108 | ; ID=0, assert(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(_)),assert(counter(C));C is 0, | |
114 | assert(counter(C))). | |
115 | reset_counter :- (counter(_) -> retract(counter(_));true),assert(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 | specfile: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 | assert(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: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 | assert(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 | specfile: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 | assert(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 | assert(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 | assert(desired_user_transition(GT,X)),fail. | |
321 | assert_desired_user_transitions(_,only_alphabet). | |
322 | ||
323 | ||
324 | :- dynamic goal_nodes/1. | |
325 | ||
326 | assert_goal_nodes :- | |
327 | retractall(goal_nodes(_)),findall(X,(visited_expression_id(X), | |
328 | user:test_goal_in_node(X)),R),sort(R,Rr),assert(goal_nodes(Rr)). | |
329 | ||
330 | ||
331 | :- dynamic use_all_operations/2,use_no_arguments/2,user_has_made_op_selection/1, | |
332 | user_has_made_arg_selection/1. | |
333 | reset_use_all_ops_args :- | |
334 | retractall(use_all_operations(_,_)), | |
335 | retractall(use_no_arguments(_,_)), | |
336 | retractall(user_has_made_op_selection(_)), | |
337 | retractall(user_has_made_arg_selection(_)), | |
338 | assert(use_all_operations(signature_merge,yes)), | |
339 | assert(use_no_arguments(signature_merge,yes)), | |
340 | assert(use_all_operations(dfa_abstraction,yes)), | |
341 | assert(use_no_arguments(dfa_abstraction,yes)), | |
342 | assert(user_has_made_op_selection(no)), | |
343 | assert(user_has_made_arg_selection(no)). | |
344 | ||
345 | user_made_op_selection :- | |
346 | (user_has_made_op_selection(yes) -> | |
347 | true | |
348 | ; retractall(user_has_made_op_selection(no)),print('change just made'),nl, | |
349 | assert(user_has_made_op_selection(yes))). | |
350 | user_made_arg_selection :- | |
351 | (user_has_made_arg_selection(yes) -> | |
352 | true | |
353 | ; retractall(user_has_made_arg_selection(no)), | |
354 | assert(user_has_made_arg_selection(yes))). | |
355 | ||
356 | set_use_all_operations(Type, Yes) :- | |
357 | retractall(use_all_operations(Type,_)), | |
358 | ((Yes == yes) -> | |
359 | assert(use_all_operations(Type,yes)), | |
360 | assert_desired_user_transitions(Type,only_alphabet) | |
361 | ; assert(use_all_operations(Type,no))). | |
362 | set_use_no_arguments(Type, Yes) :- | |
363 | retractall(use_no_arguments(Type,_)), | |
364 | ((Yes == yes) -> | |
365 | assert(use_no_arguments(Type,yes)), | |
366 | assert_all_transition_arg_dont_cares(ignore_previous_dont_cares) | |
367 | ; assert(use_no_arguments(Type,no))). | |
368 | ||
369 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
370 | End utility functions | |
371 | ==============================================================================*/ | |
372 | ||
373 | ||
374 | ||
375 | /*============================================================================== | |
376 | DFA minimisation applied and modified to prob state space graphs | |
377 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ | |
378 | ||
379 | :- use_module(library(ordsets)). | |
380 | ||
381 | :- dynamic distinguished/3,table_marked/1,equivalence_clazz/1,dfa_states_/2, | |
382 | dfa_tran_/3,final_states/1,min_dfa_state/2. | |
383 | ||
384 | dfa_cleanup :- | |
385 | retractall(equivalence_clazz(_)),retractall(distinguished(_,_,_)), | |
386 | retractall(table_marked(_)),retractall(min_dfa_state(_,_)). | |
387 | ||
388 | init :- | |
389 | dfa_cleanup,assert(table_marked(no)),get_dfa_states(States),init(States). | |
390 | ||
391 | init([_|[]]). | |
392 | init([H|T]) :- | |
393 | setup_distinguished_table(H, T), | |
394 | init(T). | |
395 | ||
396 | setup_distinguished_table(_, []). | |
397 | setup_distinguished_table(X, [H|T]) :- | |
398 | final_states(Final_States), | |
399 | (((member(X, Final_States), \+member(H, Final_States)) | (\+member(X, Final_States), member(H, Final_States))) -> | |
400 | assert(distinguished(X,H,yes)),retractall(table_marked(_)), assert(table_marked(yes)) | |
401 | ; assert(distinguished(X,H,no))), | |
402 | setup_distinguished_table(X,T). | |
403 | ||
404 | ||
405 | construct_distinguished_table :- | |
406 | distinguished(A,B,no), | |
407 | dfa_tran_(A,X,Aprime), | |
408 | dfa_tran_(B,X,Bprime), | |
409 | %print('('),print(A),print(','),print(B),print(' = no)'),print(' '),print(X),print(' ('),print(Aprime),print(','),print(Bprime),print(')'),nl, | |
410 | ((distinguished(Aprime,Bprime, yes) | distinguished(Bprime,Aprime,yes)) -> | |
411 | retract(distinguished(A,B,_)), assert(distinguished(A,B, yes)), | |
412 | retractall(table_marked(_)), assert(table_marked(yes)) | |
413 | ,print(A),print(' '),print(B),print(' '),print(yes),nl | |
414 | ;true), | |
415 | fail. | |
416 | construct_distinguished_table :- | |
417 | (table_marked(yes) -> | |
418 | retractall(table_marked(_)), assert(table_marked(no)), construct_distinguished_table;true). | |
419 | ||
420 | assert_equivalence_clazz(Class, []) :- | |
421 | ((\+equivalence_clazz(Class),equivalence_clazz(Any),ord_intersection(Class,Any,[])) | |
422 | -> assert(equivalence_clazz(Class)) | |
423 | ; true). | |
424 | assert_equivalence_clazz(Class, [H|T]) :- | |
425 | ((ord_intersection(Class, H, [_|_]) -> | |
426 | ord_union(Class, H, Res),assert_equivalence_clazz(Res, T)) | |
427 | ; assert_equivalence_clazz(Class, T)). | |
428 | ||
429 | assert_equivalence_clazzes_([]). | |
430 | assert_equivalence_clazzes_([H|T]) :- | |
431 | assert_equivalence_clazz(H, T), | |
432 | assert_equivalence_clazzes_(T). | |
433 | ||
434 | assert_equivalence_clazzes :- | |
435 | findall([X,Y],distinguished(X,Y,'no'),Res), | |
436 | sort(Res, Result), | |
437 | assert_equivalence_clazzes_(Result), | |
438 | fail. | |
439 | assert_equivalence_clazzes. | |
440 | ||
441 | unflatten([], []). | |
442 | unflatten([H|T], [[H]|Res]) :- | |
443 | unflatten(T, Res). | |
444 | ||
445 | minimize_dfa(Res) :- | |
446 | init, construct_distinguished_table, assert_equivalence_clazzes, | |
447 | findall(X,equivalence_clazz(X),ReS),% retractall(equivalence_clazz(_)), | |
448 | findall([X,Y],distinguished(X,Y,'yes'),Result), | |
449 | %print(Result),nl, | |
450 | ent03r_flatten(Result, Flat_Re),remove_dups(Flat_Re, Resu), | |
451 | sort(Resu, Result_), | |
452 | %print('*'),print(Result_),nl, | |
453 | ent03r_flatten(ReS, Flat_Res),sort(Flat_Res,Flat_Res_), | |
454 | %print(Flat_Res_),nl, | |
455 | length(Result_,LR),length(Flat_Res_,FR), | |
456 | (LR =< FR -> | |
457 | ord_intersection(Result_, Flat_Res_,_,Diff) | |
458 | ; ord_intersection(Flat_Res_, Result_,_,Diff)), | |
459 | %print(Diff),nl, | |
460 | unflatten(Diff, Fat_Diff),append(ReS, Fat_Diff, Res),assert_min_dfa_states(Res). | |
461 | ||
462 | get_representative_from_list(L,Representative) :- | |
463 | member(Representative, L),!. | |
464 | ||
465 | assert_min_dfa_states([]). | |
466 | assert_min_dfa_states([H|T]) :- | |
467 | get_representative_from_list(H,Represen), | |
468 | assert(min_dfa_state(H,Represen)), | |
469 | assert_min_dfa_states(T). | |
470 | ||
471 | print_min_dfa_states_representatives_for_dot :- | |
472 | min_dfa_state(_,ID), | |
473 | map_dfa_state_to_id(RealRep,ID), | |
474 | (RealRep == [] -> fail;true), | |
475 | (RealRep == [root] -> | |
476 | print(ID),print('[shape=invtriangle, color=green, label=""];'),nl,fail %"#0d9d03" | |
477 | ; print(ID), print('[shape=ellipse, color=black, label=\"'),print(ID), | |
478 | print('\", id='),print(ID),print('];'),nl,fail). | |
479 | print_min_dfa_states_representatives_for_dot. | |
480 | ||
481 | print_min_dfa__representatives_transitions_ :- | |
482 | min_dfa_state(_,Representative), | |
483 | dfa_tran_(Representative,Letter,Succ), | |
484 | min_dfa_state(State,SuccRepresentative), | |
485 | ||
486 | map_dfa_state_to_id(RealRep,Representative), | |
487 | RealRep \== [], | |
488 | map_dfa_state_to_id(RealSuccRep,SuccRepresentative), | |
489 | RealSuccRep \== [], | |
490 | ||
491 | member(Succ,State), | |
492 | print(Representative), | |
493 | print(' -> '), | |
494 | print(SuccRepresentative), | |
495 | (RealRep == [root] -> | |
496 | print('[style=dotted, color=black, label=\"') | |
497 | ; print('[color=blue, label=\"')), | |
498 | print(Letter), | |
499 | print('\"];'), | |
500 | nl, | |
501 | fail. | |
502 | print_min_dfa__representatives_transitions_. | |
503 | ||
504 | print_min_dfa_for_dot(File) :- | |
505 | nfa_to_dfa, | |
506 | minimize_dfa(_), | |
507 | % for each min_dfa_state, get a representative state, for each letter of the alphabet, print the transition | |
508 | % and the representative state to which the transition leads | |
509 | tell(File), | |
510 | print_graph_header(minimum_dfa), | |
511 | print_min_dfa_states_representatives_for_dot, | |
512 | print_min_dfa__representatives_transitions_, | |
513 | print_graph_footer, | |
514 | told. | |
515 | print_min_dfa_for_dot(_). | |
516 | ||
517 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
518 | End DFA minimisation | |
519 | ==============================================================================*/ | |
520 | ||
521 | /*============================================================================== | |
522 | NFA to DFA | |
523 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ | |
524 | ||
525 | % Use this to find out about all of the transitions - instead of using transition/3 directly. This predicate filters | |
526 | % out transitions which the user isn't interested in. | |
527 | nfa_to_dfa_transition_filter(A,B,Sig,D) :- | |
528 | transition(A,B,D), | |
529 | transition_info(B,_,_,SmallSig), | |
530 | remove_transition_arg_dont_cares(dfa_abstraction, B, Sig), | |
531 | desired_user_transition(dfa_abstraction,SmallSig). | |
532 | ||
533 | :- volatile transi_/2,map_dfa_state_to_id/2. | |
534 | :- dynamic transi_/2,map_dfa_state_to_id/2. | |
535 | findall_transitions(State,TransName,_) :- | |
536 | nfa_to_dfa_transition_filter(State,_,TransName,Succ), | |
537 | (transi_(State,Succ) -> | |
538 | true | |
539 | ; asserta(transi_(State,Succ))), | |
540 | fail. | |
541 | findall_transitions(State,_,Result) :- | |
542 | findall(Succ,transi_(State,Succ),Result),retractall(transi_(_,_)). | |
543 | ||
544 | nfa_cleanup :- | |
545 | retractall(dfa_states_(_,_)),retractall(dfa_tran_(_,_,_)), | |
546 | retractall(final_states(_)),retractall(map_dfa_state_to_id(_,_)). | |
547 | ||
548 | move_([],_,[]). | |
549 | move_([Head|Tail],T,R) :- | |
550 | move_(Head,T,R1), | |
551 | move_(Tail,T,R2),ent03r_union(R1,R2,R). | |
552 | move_(S,T,R) :- | |
553 | findall_transitions(S,T,R). | |
554 | move(S,T,R) :- move_(S,T,Rp), | |
555 | retractall(transi_(_,_)),ent03r_flatten(Rp,R),!. | |
556 | ||
557 | nfa_to_dfa_worker(Alphabet) :- | |
558 | repeat, | |
559 | (dfa_states_(S,no) -> true;!,fail), | |
560 | %print('testing S = '),print(S),nl, | |
561 | retract(dfa_states_(S,no)), | |
562 | asserta(dfa_states_(S,yes)), | |
563 | % print(treating_dfa_state(S)),nl, | |
564 | (map_dfa_state_to_id(S,_) -> | |
565 | true | |
566 | ; next_equivalence_class_id(ID0), | |
567 | % print(new_equiv_class(ID0)),nl, | |
568 | asserta(map_dfa_state_to_id(S,ID0))), | |
569 | %print('*'), | |
570 | member(Letter,Alphabet), | |
571 | % print(computing_move(S,Letter)),nl, | |
572 | move(S,Letter,Res), | |
573 | sort(Res,Result), | |
574 | % print(move(S,Letter,Res)),nl, | |
575 | (dfa_states_(Result,_) -> | |
576 | true /* state already exists */ | |
577 | ; asserta(dfa_states_(Result,no)), % register new, untreated state | |
578 | % print(new_successor_state(Result)),nl, | |
579 | (map_dfa_state_to_id(Result,_) -> | |
580 | true | |
581 | ; next_equivalence_class_id(ID1), | |
582 | % print(new_equiv_class(ID1)),nl, | |
583 | asserta(map_dfa_state_to_id(Result,ID1)))), | |
584 | %print('asserting '),print(Result),nl), | |
585 | map_dfa_state_to_id(S,ID2), | |
586 | map_dfa_state_to_id(Result,ID3), | |
587 | % print(dfa_tran(ID2,Letter,ID3)),nl, | |
588 | asserta(dfa_tran_(ID2,Letter,ID3)),fail. | |
589 | nfa_to_dfa_worker(_). | |
590 | ||
591 | get_dfa_states(States) :- | |
592 | findall(S,map_dfa_state_to_id(_,S),Statess), | |
593 | sort(Statess,States). | |
594 | ||
595 | ||
596 | ||
597 | nfa_to_dfa :- | |
598 | nfa_cleanup, | |
599 | init_equivalence_class_id, | |
600 | /* findall(X,desired_user_transition(dfa_abstraction,X),Alphabet), */ | |
601 | get_alphabet(dfa_abstraction,Alphabet), | |
602 | print('% Alphabet: '), print(Alphabet),nl, | |
603 | asserta(dfa_states_([root],no)), | |
604 | nfa_to_dfa_worker(Alphabet). | |
605 | nfa_to_dfa :- | |
606 | get_dfa_states(States), | |
607 | map_dfa_state_to_id([root],ID1), | |
608 | (map_dfa_state_to_id([],ID2) -> | |
609 | List = [ID2,ID1], %add other final states here | |
610 | sort(List,SList), | |
611 | ord_subtract(States,SList,Finals) | |
612 | ; ord_subtract(States,[ID1],Finals)), | |
613 | ||
614 | assert(final_states(Finals)). | |
615 | ||
616 | ||
617 | ||
618 | print_dfa_from_nfa_states_id :- | |
619 | map_dfa_state_to_id(Reals,ID), | |
620 | ((Reals == []) -> fail;true), | |
621 | ||
622 | % work out outline colour | |
623 | ((member(A,Reals),transition(A,_,_)) -> % this node not is open (**in this dfa graph) | |
624 | get_preference(dot_normal_node_colour,OutColour) | |
625 | ; get_preference(dot_open_node_colour,OutColour)), % this node is open | |
626 | ||
627 | % work out fill colour | |
628 | ((invariant_violated(C), member(C,Reals)) -> | |
629 | get_preference(dot_invariant_violated_node_colour,InColour) | |
630 | ; true), | |
631 | ||
632 | % work out shape | |
633 | ((Reals == [root]) -> % its the root | |
634 | get_preference(dot_root_shape,Shape), | |
635 | print(root),print('[id="root", shape='),print(Shape),print(', color=green, label=""];'),nl,fail | |
636 | ; ((state_space:current_state_id(B),member(B,Reals)) -> % it contains the current state | |
637 | get_preference(dot_current_node_shape,Shape) | |
638 | ; get_preference(dot_normal_node_shape,Shape))), % it doesn't contain the current state | |
639 | ||
640 | % do the printing | |
641 | print(ID),print('[id='),print(ID),print(', shape='),print(Shape),print(', color=\"'),print(OutColour),print('\"'), | |
642 | (nonvar(InColour) -> print(', style=filled, fillcolor='),print(InColour); true),print('];'),nl, | |
643 | fail. | |
644 | print_dfa_from_nfa_states_id. | |
645 | ||
646 | print_dot_for_dfa_from_nfa_ :- | |
647 | dfa_tran_(ID1,Letter,ID2), | |
648 | map_dfa_state_to_id(ID1_reals, ID1), | |
649 | map_dfa_state_to_id(ID2_reals, ID2), | |
650 | ((ID2_reals == []) -> fail;true), | |
651 | ((ID1_reals == [root]) -> | |
652 | print(root) | |
653 | ; print(ID1)), | |
654 | print(' -> '), | |
655 | print(ID2), | |
656 | (map_dfa_state_to_id([root], ID1) -> | |
657 | print('[color=black, label=\"') %style=dotted, | |
658 | ; ((ID1_reals \== ID2_reals,ord_subset(ID2_reals, ID1_reals)) -> | |
659 | print('[style=dotted,') | |
660 | ; print('[')), | |
661 | print('color=blue, label=\"')), | |
662 | print(Letter), | |
663 | print('\"];'), | |
664 | nl, | |
665 | fail. | |
666 | print_dot_for_dfa_from_nfa_. | |
667 | ||
668 | print_dot_for_dfa_from_nfa(File) :- | |
669 | % use all operations if desired | |
670 | (use_all_operations(dfa_abstraction,yes) -> | |
671 | set_use_all_operations(dfa_abstraction,yes) | |
672 | ; true), | |
673 | % use no arguments if desired | |
674 | (use_no_arguments(dfa_abstraction,yes) -> | |
675 | set_use_no_arguments(dfa_abstraction,yes) | |
676 | ; true), | |
677 | print('% Converting NFA to DFA'),nl, | |
678 | nfa_to_dfa, | |
679 | number_of_equivalence_classes(Nr), | |
680 | format('% Writing DFA with ~w states to file: ~w~n',[Nr,File]), | |
681 | tell(File), | |
682 | print_graph_header(nfa_to_dfa), | |
683 | print_dfa_from_nfa_states_id, | |
684 | nl, | |
685 | print_dot_for_dfa_from_nfa_, | |
686 | print_graph_footer, | |
687 | told, | |
688 | (Nr>100 -> format('% Warning: viewing ~w states with dot can take time!~n',[Nr]) ; true). | |
689 | ||
690 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
691 | End of NFA to DFA code | |
692 | ==============================================================================*/ | |
693 | ||
694 | ||
695 | ||
696 | /*============================================================================== | |
697 | Signature Merge based on a state's transitions | |
698 | - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ | |
699 | ||
700 | :- dynamic counter/1,state_signature/4, | |
701 | state_merge_equivalence_class/3,transition_printed/1,state_printed/1, | |
702 | %state_merge_filter_mode/1, | |
703 | state_merge_separate_invariant_violations/1,non_det_trans/3, | |
704 | signature_merge_show_all_transitions/1,non_def_trans/2. | |
705 | ||
706 | % Either no or yes. The former means we don't separate states that break the | |
707 | % invariant violation into their own equivalence class. The latter means we do. | |
708 | state_merge_separate_invariant_violations(no). | |
709 | ||
710 | % Either no or yes. The former means we don't view every outgoing transition for | |
711 | % each equivalence class. The latter means we do. | |
712 | signature_merge_show_all_transitions(yes). | |
713 | ||
714 | set_signature_merge_show_all_transitions(H) :- | |
715 | (signature_merge_show_all_transitions(H) -> | |
716 | true | |
717 | ; retractall(signature_merge_show_all_transitions(_)), | |
718 | assert(signature_merge_show_all_transitions(H))). | |
719 | ||
720 | %state_merge_separate_iviolations(V) :- | |
721 | % (((V == yes) ; (V == no)) -> | |
722 | % retractall(state_merge_separate_invariant_violations(_)), | |
723 | % assert(state_merge_separate_invariant_violations(V)) | |
724 | % ; print('invalid state_merge_separate_iviolations/1 mode: '),print(V), | |
725 | % print(' should be either, yes, or no'),nl). | |
726 | ||
727 | % Either normal ==> perform reduction on original state space | |
728 | % OR nfa_to_dfa ==> perform reduction on state space outputted from nfa_to_dfa function | |
729 | % NB: SPELL YOUR OPTION CORRECTLY OR GET WEIRD RESULTS! | |
730 | %state_merge_filter_mode(normal). | |
731 | ||
732 | % clean up the database | |
733 | cleanup_state_merge :- | |
734 | retractall(state_signature(_,_,_,_)),retractall(state_merge_equivalence_class(_,_,_)), | |
735 | retractall(counter(_)), | |
736 | retractall(non_det_trans(_,_,_)), | |
737 | retractall(non_def_trans(_,_)) | |
738 | /*,retractall(desired_user_transition(_,_))*/. | |
739 | ||
740 | % get the transitions: take care that we regard the different modes | |
741 | state_merge_transition_filter(A,B,Sig,D) :- | |
742 | transition(A,B,D),transition_info(B,_,_,Sig), | |
743 | desired_user_transition(signature_merge,Sig). | |
744 | ||
745 | % get the states: take care that we regard the different modes | |
746 | state_merge_state_filter(A,B,B) :- visited_expression(A,B). | |
747 | ||
748 | % assert the transitions stemming from each state | |
749 | assert_state_merges :- | |
750 | state_merge_state_filter(ID,State,_), | |
751 | compute_signature_for_state(ID,State,Res), | |
752 | % check whether to separate each invariant violation in it's own | |
753 | % equivalence class. | |
754 | (state_merge_separate_invariant_violations(no) -> | |
755 | assert_state_signature(ID,Res,ok) | |
756 | ; (invariant_violated(ID) -> | |
757 | assert_state_signature(ID,Res,invariant_violated) | |
758 | ; assert_state_signature(ID,Res,ok))), | |
759 | fail. | |
760 | assert_state_merges. | |
761 | ||
762 | assert_state_signature(ID,Signature,OK) :- | |
763 | (state_merge_equivalence_class(Signature,ClassID,OK) | |
764 | -> true | |
765 | ; increment_counter(ClassID), | |
766 | assert(state_merge_equivalence_class(Signature,ClassID,OK)) | |
767 | ), | |
768 | assert(state_signature(ID,Signature,OK,ClassID)). | |
769 | ||
770 | %:- dynamic observing_variable/1. | |
771 | /* set this predicate if we want to observe a particular variable instead of the signature */ | |
772 | %observing_variable('display_st'). | |
773 | ||
774 | %compute_signature_for_state(_,State,Res) :- | |
775 | % observing_variable(Var),store:lookup_value(Var,State,Val),!, Res=Val. | |
776 | compute_signature_for_state(ID,_,Res) :- | |
777 | findall(Tr,state_merge_transition_filter(ID,_,Tr,_),Res_), | |
778 | sort(Res_,Res). | |
779 | ||
780 | % find out the state equivalence class for a given state | |
781 | find_state_merge_equivalence_class_for_state(State,ClassID) :- | |
782 | state_signature(State,_TransSig,_Status,ClassID),!. | |
783 | ||
784 | % find out a state corresponding to a given equivalence class | |
785 | find_state_for_state_merge_equivalence_class(ClassID,State) :- | |
786 | state_signature(State,_SIG,_OK,ClassID). | |
787 | ||
788 | % apply the state merge algorithm | |
789 | state_merge :- | |
790 | cleanup_state_merge, | |
791 | % work on the correct state space e.g. the original one as opposed to | |
792 | % one outputted by another algorithm | |
793 | /*assert_desired_user_transitions,*/ | |
794 | print_message('Computing Signatures'), | |
795 | assert_state_merges. | |
796 | ||
797 | % the state merge state's colour | |
798 | state_merge_state_colour(State, Colour) :- | |
799 | (state_merge_equivalence_class([],State,_) -> | |
800 | get_preference(dot_open_node_colour,Colour) | |
801 | ; get_preference(dot_normal_node_colour,Colour)). | |
802 | ||
803 | % print a state's id for the state merge - print 'root' for this if the id maps to the root | |
804 | print_state_merge_state_id(State) :- | |
805 | (find_state_merge_equivalence_class_for_state(root,State) -> print(root) | |
806 | ; print(State)). | |
807 | ||
808 | % print a transition for dot | |
809 | print_transition_for_dot(A,IndividualSig,C) :- Trans = [A,IndividualSig,C], | |
810 | (transition_printed(Trans) -> | |
811 | true | |
812 | ; assert(transition_printed(Trans)), | |
813 | print_state_merge_state_id(A),print('->'),print(C), | |
814 | (find_state_merge_equivalence_class_for_state(root, A) -> | |
815 | /* Style = 'solid', Color='blue' % dealing with the root */ | |
816 | (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
817 | Style = 'dotted' % there's more than one of these transitions | |
818 | ; Style = 'solid'), | |
819 | (non_def_trans(A,IndividualSig) -> | |
820 | Color = 'purple';Color = 'black') | |
821 | ; (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
822 | Style = 'dotted' % there's more than one of these transitions | |
823 | ; Style = 'solid'), | |
824 | (non_def_trans(A,IndividualSig) -> | |
825 | Color = 'purple';Color = 'blue')), | |
826 | print('[style='),print(Style),print(', color=\"'),print(Color), | |
827 | print('\", label=\"'),print(IndividualSig),print('\"];'),nl). | |
828 | ||
829 | % print a state for dot | |
830 | print_class_as_dotstate(ClassID,OK) :- | |
831 | (state_printed(ClassID) -> | |
832 | true | |
833 | ; assert(state_printed(ClassID)), | |
834 | state_merge_state_colour(ClassID, StateColour), | |
835 | get_preference(dot_invariant_violated_node_colour,IColor), | |
836 | print_state_merge_state_id(ClassID), | |
837 | print(' ['), | |
838 | (find_state_merge_equivalence_class_for_state(root,ClassID) -> | |
839 | print('shape=invtriangle, color=green, '), | |
840 | print('label=\"\", id=\"'),print(root) | |
841 | ; ((OK = invariant_violated) -> | |
842 | print('shape=ellipse, style=filled, fillcolor="'), | |
843 | print(IColor),print('\", label=\"'), | |
844 | print_node_label(ClassID),print('\" , id=\"'),print_node_label(ClassID) | |
845 | ; print('shape=ellipse, color=\"'),print(StateColour),print('\", label=\"'), | |
846 | print_node_label(ClassID),print('\" , id=\"'),print_node_label(ClassID))), | |
847 | print('\"];'),nl). | |
848 | ||
849 | print_node_label(ClassID) :- | |
850 | (preference(dot_print_node_ids,false) | |
851 | -> state_merge_equivalence_class(Signature,ClassID,_OK), | |
852 | print(Signature) | |
853 | ; preference(dot_print_node_info,true) | |
854 | -> state_merge_equivalence_class(Signature,ClassID,_OK), | |
855 | print(ClassID),print('\\n'), print(Signature) | |
856 | ; print(ClassID) | |
857 | ). | |
858 | ||
859 | % print the merged states | |
860 | print_state_merge_states_for_dot :- | |
861 | state_merge_equivalence_class(_,ClassID,OK), | |
862 | print_class_as_dotstate(ClassID,OK),fail. | |
863 | print_state_merge_states_for_dot. | |
864 | ||
865 | % assert whether there is more than one transition from an equivalence class | |
866 | % with the same label. | |
867 | assert_non_det_trans(_State,StateID,IndividualTransSignature,_To1ID) :- | |
868 | non_det_trans(StateID,IndividualTransSignature,_Status),!. % already computed | |
869 | assert_non_det_trans(State,StateID,TransSignature,To1ID) :- | |
870 | find_state_for_state_merge_equivalence_class(StateID,AnotherState), | |
871 | State \= AnotherState, | |
872 | \+ not_all_transitions_added(AnotherState), % this is an open node; not yet computed | |
873 | /* state_merge_transition_filter */ | |
874 | transition(AnotherState,_,TransSignature,To2), | |
875 | \+(find_state_merge_equivalence_class_for_state(To2,To1ID)),!, | |
876 | %print_message(non_det(StateID,TransSignature,To1ID,AnotherState,To2)), | |
877 | asserta(non_det_trans(StateID,TransSignature,true)). | |
878 | assert_non_det_trans(_State,StateID,IndividualTransSignature,_To1ID) :- | |
879 | assert(non_det_trans(StateID,IndividualTransSignature,false)). | |
880 | ||
881 | % print the transitions of the merged states. | |
882 | print_state_merge_transitions_for_dot :- | |
883 | transition(State,_,IndividualSig,To), | |
884 | find_state_merge_equivalence_class_for_state(State,ID1), | |
885 | find_state_merge_equivalence_class_for_state(To,ID2), | |
886 | assert_non_det_trans(State,ID1,IndividualSig,ID2), | |
887 | (desired_user_transition(signature_merge,IndividualSig) -> | |
888 | print_transition_for_dot(ID1,IndividualSig,ID2) | |
889 | ; (signature_merge_show_all_transitions(yes) -> | |
890 | (non_def_trans(ID1,IndividualSig) -> | |
891 | true | |
892 | ; assert(non_def_trans(ID1,IndividualSig))), | |
893 | print_transition_for_dot(ID1,IndividualSig,ID2) | |
894 | ; true) | |
895 | ), | |
896 | fail. | |
897 | print_state_merge_transitions_for_dot. | |
898 | ||
899 | % print the merged state graph for dot | |
900 | print_state_merge_for_dot :- | |
901 | % check if user has specified all transitions | |
902 | (use_all_operations(signature_merge,yes) -> | |
903 | set_use_all_operations(signature_merge,yes) | |
904 | ; true), | |
905 | clean_up_after_printing, | |
906 | print_message('Performing State Merge'), | |
907 | state_merge, | |
908 | print_graph_header(state_merge), | |
909 | print_message('Generating Dot States'), | |
910 | print_state_merge_states_for_dot, | |
911 | print_message('Generating Dot Transitions'), | |
912 | print_state_merge_transitions_for_dot, | |
913 | print_graph_footer. | |
914 | ||
915 | print_state_merge_for_dot(File) :- time(print_state_merge_for_dot2(File)). | |
916 | print_state_merge_for_dot2(File) :- | |
917 | tell(File),print_state_merge_for_dot,told. | |
918 | ||
919 | ||
920 | % For ProB 2.0 Graphical Visualizations | |
921 | extract_graph_of_state_merge(Graph) :- | |
922 | % check if user has specified all transitions | |
923 | (use_all_operations(signature_merge,yes) -> | |
924 | set_use_all_operations(signature_merge,yes) | |
925 | ; true), | |
926 | clean_up_after_printing, | |
927 | print_message('Performing State Merge'), | |
928 | state_merge, | |
929 | print_message('Generating States'), | |
930 | extract_state_merge_states(States), | |
931 | print_message('Generating Transitions'), | |
932 | extract_state_merge_transitions(Transitions), | |
933 | Graph = [States,Transitions]. | |
934 | ||
935 | extract_state_merge_states(States) :- | |
936 | findall(State,extract_state_for_graph(State),States). | |
937 | ||
938 | extract_state_for_graph(State) :- | |
939 | state_merge_equivalence_class(Sig,Id,OK), | |
940 | State = state(Sig,Id,OK). | |
941 | ||
942 | extract_state_merge_transitions(Transitions) :- | |
943 | findall(Trans,extract_state_merge_transition(Trans),Transitions). | |
944 | ||
945 | extract_state_merge_transition(Transition) :- | |
946 | transition(State,_,IndividualSig,To), | |
947 | find_state_merge_equivalence_class_for_state(State,ID1), | |
948 | find_state_merge_equivalence_class_for_state(To,ID2), | |
949 | assert_non_det_trans(State,ID1,IndividualSig,ID2), | |
950 | (desired_user_transition(signature_merge,IndividualSig) -> | |
951 | extract_transition_representation(ID1,IndividualSig,ID2,Color,Style) | |
952 | ; (signature_merge_show_all_transitions(yes) -> | |
953 | (non_def_trans(ID1,IndividualSig) -> | |
954 | true | |
955 | ; assert(non_def_trans(ID1,IndividualSig))), | |
956 | extract_transition_representation(ID1,IndividualSig,ID2,Color,Style) | |
957 | ; true) | |
958 | ), | |
959 | Transition = trans(ID1,IndividualSig,ID2,Color,Style). | |
960 | ||
961 | ||
962 | extract_transition_representation(A,IndividualSig,C,Color,Style) :- | |
963 | Trans = [A,IndividualSig,C], | |
964 | (transition_printed(Trans) -> | |
965 | fail | |
966 | ; assert(transition_printed(Trans)), | |
967 | (find_state_merge_equivalence_class_for_state(root, A) -> | |
968 | /* Style = 'solid', Color='blue' % dealing with the root */ | |
969 | (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
970 | Style = 'dotted' % there's more than one of these transitions | |
971 | ; Style = 'solid'), | |
972 | (non_def_trans(A,IndividualSig) -> | |
973 | Color = 'purple';Color = 'black') | |
974 | ; (non_det_trans(A,IndividualSig,true) -> % not dealing with root | |
975 | Style = 'dotted' % there's more than one of these transitions | |
976 | ; Style = 'solid'), | |
977 | (non_def_trans(A,IndividualSig) -> | |
978 | Color = 'purple';Color = 'blue')) | |
979 | ). | |
980 | ||
981 | ||
982 | ||
983 | % clean up the database from assertions used during graph printing. | |
984 | clean_up_after_printing :- | |
985 | retractall(state_printed(_)),retractall(transition_printed(_)). | |
986 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
987 | End of signature merge reduction | |
988 | ==============================================================================*/ | |
989 | ||
990 | ||
991 | :- volatile things/1. | |
992 | :- dynamic things/1. | |
993 | assert_associated_nodes([]). | |
994 | assert_associated_nodes([H|T]) :- | |
995 | (things(H) -> | |
996 | assert_associated_nodes(T) | |
997 | ; assert(things(H)),findall(X,transition(X,_,H),Res), | |
998 | append(T,Res,Ress),assert_associated_nodes(Ress)). | |
999 | ||
1000 | check_against_list(_,[]). | |
1001 | check_against_list(Element,[H|T]) :- | |
1002 | (state_printed(Element) -> | |
1003 | true | |
1004 | ; assert(state_printed(Element)), | |
1005 | visualize_graph:tcltk_print_node_for_dot(Element)), | |
1006 | /* (transition_printed([Element,H]) -> | |
1007 | true | |
1008 | ; assert(transition_printed([Element,H])), */ | |
1009 | (transition(Element,_,H) -> visualize_graph:tcltk_print_transitions_for_dot(Element,H) | |
1010 | ; true), | |
1011 | check_against_list(Element,T). | |
1012 | ||
1013 | print_dot_from_node_list(_,File) :- | |
1014 | tell(File), | |
1015 | retractall(state_printed(_)), | |
1016 | retractall(transition_printed(_)), | |
1017 | print_graph_header(general_graph),fail. | |
1018 | print_dot_from_node_list(Llist,_) :- | |
1019 | sort(Llist,List), | |
1020 | member(N1,List), | |
1021 | check_against_list(N1,List),fail. | |
1022 | print_dot_from_node_list(_,_) :- | |
1023 | print_graph_footer,told. | |
1024 | ||
1025 | print_subgraph_associated_with_node(Node,File) :- | |
1026 | retractall(things(_)), | |
1027 | (is_list(Node) -> | |
1028 | assert_associated_nodes(Node) | |
1029 | ; assert_associated_nodes([Node])), | |
1030 | findall(X,reduce_graph_state_space:things(X),Result), | |
1031 | print_dot_from_node_list(Result,File). | |
1032 | ||
1033 | print_subgraph_associated_with_invariant_violations(File) :- | |
1034 | findall(X,invariant_violated(X),R),remove_dups(R,Rr), | |
1035 | print_subgraph_associated_with_node(Rr,File). | |
1036 | ||
1037 | print_subgraph_of_goal_nodes(File) :- | |
1038 | assert_goal_nodes,goal_nodes(L),print_dot_from_node_list(L,File). | |
1039 | ||
1040 | /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - | |
1041 | End of Iterative Deepening search for a node | |
1042 | ==============================================================================*/ | |
1043 | ||
1044 | ||
1045 | ||
1046 | ||
1047 | ||
1048 |