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