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