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 | | |