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