reduce_graph_state_space

assert_all_transition_arg_dont_cares :-
    graph_type(GT),
    transition(_,Trans,_),transition_info(Trans,_,ArgsLength,Sig),
    (transition_arg_dont_cares(GT,Sig,_) -> fail;true),
    % check if argslength is < 0, then add one if it is.
    ((ArgsLength < 0) ->
    ArgLength is (-ArgsLength-1)
    ; ArgLength is ArgsLength),
    make_counting_list(ArgLength,[],DontCares),
    make_counting_list(ArgLength,DontCares,ArgFormat),
    assert_transition_dont_cares(GT,Sig,ArgFormat),fail.

assert_all_transition_arg_dont_cares.

assert_all_transition_arg_dont_cares(ignore_previous_dont_cares) :-
    retractall_transition_arg_dont_cares,
    graph_type(GT),
    transition(_,Trans,_),transition_info(Trans,_,ArgsLength,Sig),
    % check if argslength is < 0, then add one if it is.
    ((ArgsLength < 0) ->
    ArgLength is (-ArgsLength-1)
    ; ArgLength is ArgsLength),
    make_counting_list(ArgLength,[],DontCares),
    make_counting_list(ArgLength,DontCares,ArgFormat),
    assert_transition_dont_cares(GT,Sig,ArgFormat),fail.

assert_all_transition_arg_dont_cares(ignore_previous_dont_cares).

assert_associated_nodes([]).

assert_associated_nodes([H|T]) :-
    (things(H) ->
    assert_associated_nodes(T)
    ; assertz(things(H)),findall(X,transition(X,_,H),Res),
    append(T,Res,Ress),assert_associated_nodes(Ress)).

assert_desired_user_transitions(alphabet) :-
    retractall(desired_user_transition(_,_)),
    retractall_transition_info,retractall_transition_arg_dont_cares,
    assert_all_transition_arg_dont_cares,get_alphabet_signatures(Ab),/* print(Ab),nl, */
    graph_type(GT),member(X,Ab),
    assertz(desired_user_transition(GT,X)),fail.

assert_desired_user_transitions(alphabet).

assert_desired_user_transitions(only_alphabet) :-
    retractall(desired_user_transition(_,_)),get_alphabet_signatures(Ab),
    graph_type(GT),member(X,Ab),
    assertz(desired_user_transition(GT,X)),fail.

assert_desired_user_transitions(only_alphabet).

assert_desired_user_transitions(GT,only_alphabet) :-
    retractall(desired_user_transition(GT,_)),get_alphabet_signatures(Ab),
    graph_type(GT),member(X,Ab),
    assertz(desired_user_transition(GT,X)),fail.

assert_desired_user_transitions(_,only_alphabet).

assert_equivalence_clazz(Class, []) :-
    ((\+equivalence_clazz(Class),equivalence_clazz(Any),ord_intersection(Class,Any,[]))
    -> assertz(equivalence_clazz(Class))
    ; true).

assert_equivalence_clazz(Class, [H|T]) :-
    ((ord_intersection(Class, H, [_|_]) ->
    ord_union(Class, H, Res),assert_equivalence_clazz(Res, T))
    ; assert_equivalence_clazz(Class, T)).

assert_equivalence_clazzes :-
    findall([X,Y],distinguished(X,Y,'no'),Res),
    sort(Res, Result),
    assert_equivalence_clazzes_(Result),
    fail.

assert_equivalence_clazzes.

assert_equivalence_clazzes_([]).

assert_equivalence_clazzes_([H|T]) :-
    assert_equivalence_clazz(H, T),
    assert_equivalence_clazzes_(T).

assert_goal_nodes :-
    retractall(goal_nodes(_)),findall(X,(visited_expression_id(X),
    node_satisfies_goal(X)),R),sort(R,Rr),assertz(goal_nodes(Rr)).

assert_min_dfa_states([]).

assert_min_dfa_states([H|T]) :-
    get_representative_from_list(H,Represen),
    assertz(min_dfa_state(H,Represen)),
    assert_min_dfa_states(T).

assert_non_det_trans(_State,StateID,IndividualTransSignature,_To1ID) :-
    non_det_trans(StateID,IndividualTransSignature,_Status),!. % already computed

assert_non_det_trans(State,StateID,TransSignature,To1ID) :-
    find_state_for_state_merge_equivalence_class(StateID,AnotherState),
    State \= AnotherState,
    \+ not_all_transitions_added(AnotherState), % this is an open node; not yet computed
    /* state_merge_transition_filter */
    transition(AnotherState,_,TransSignature,To2),
    \+(find_state_merge_equivalence_class_for_state(To2,To1ID)),!,
    %print_message(non_det(StateID,TransSignature,To1ID,AnotherState,To2)),
    asserta(non_det_trans(StateID,TransSignature,true)).

assert_non_det_trans(_State,StateID,IndividualTransSignature,_To1ID) :-
    assertz(non_det_trans(StateID,IndividualTransSignature,false)).

assert_state_merges :-
    state_merge_state_filter(ID,State,_),
    compute_signature_for_state(ID,State,Res),
    % check whether to separate each invariant violation in it's own
    % equivalence class.
    (state_merge_separate_invariant_violations(no) ->
    assert_state_signature(ID,Res,ok)
    ; (invariant_violated(ID) ->
    assert_state_signature(ID,Res,invariant_violated)
    ; assert_state_signature(ID,Res,ok))),
    fail.

assert_state_merges.

assert_state_signature(ID,Signature,OK) :-
    (state_merge_equivalence_class(Signature,ClassID,OK)
    -> true
    ; increment_counter(ClassID),
    assertz(state_merge_equivalence_class(Signature,ClassID,OK))
    ),
    assertz(state_signature(ID,Signature,OK,ClassID)).

assert_transition_dont_cares(GT,TransitionSig, DontCareIndices) :-
    retractall(transition_arg_dont_cares(GT,TransitionSig,_)),
    assertz(transition_arg_dont_cares(GT,TransitionSig, DontCareIndices)).

check_against_list(_,[]).

check_against_list(Element,[H|T]) :-
    (state_printed(Element) ->
    true
    ; assertz(state_printed(Element)),
    visualize_graph:tcltk_print_node_for_dot(Element)),
    /* (transition_printed([Element,H]) ->
    true
    ; assertz(transition_printed([Element,H])), */
    (transition(Element,_,H) -> visualize_graph:tcltk_print_transitions_for_dot(Element,H)
    ; true),
    check_against_list(Element,T).

clean_up_after_printing :-
    retractall(state_printed(_)),retractall(transition_printed(_)).

cleanup_state_merge :-
    retractall(state_signature(_,_,_,_)),retractall(state_merge_equivalence_class(_,_,_)),
    retractall(counter(_)),
    retractall(non_det_trans(_,_,_)),
    retractall(non_def_trans(_,_))
/*,retractall(desired_user_transition(_,_))*/.

compute_signature(Name, Arity, Signature) :-
    (transition_info(Name,Arity,Signature) ->
    true
    ; FS_cl = "/",
    /* Arity for operations that return a value is one less than it
    actually is: so that later predicates can test for a return
    value by the arity being a negative number; and being one less
    enables coping with returning operations with 0 arity. */
    (Arity < 0 ->
    RealArity is (-Arity-1), Arrow_cl = "-->",
    number_codes(1, Return_Len),
    LP_cl = "(", RP_cl = ")"
    ; RealArity is Arity, Arrow_cl = [],
    Return_Len = [], LP_cl = [], RP_cl = []),
    atom_codes(Name, Nn), number_codes(RealArity, Aa),
    NnAa = [Nn, FS_cl, Aa],
    ent03r_flatten(NnAa, F_cl),
    RES = [F_cl, Arrow_cl, LP_cl, Return_Len, RP_cl],
    ent03r_flatten(RES, Flat_RES), atom_codes(Signature, Flat_RES),
    assertz(transition_info(Name,Arity,Signature))),
    !.

compute_signature_for_state(ID,_,Res) :-
    findall(Tr,state_merge_transition_filter(ID,_,Tr,_),Res_),
    sort(Res_,Res).

construct_distinguished_table :-
    distinguished(A,B,no),
    dfa_tran_(A,X,Aprime),
    dfa_tran_(B,X,Bprime),
    %print('('),print(A),print(','),print(B),print(' = no)'),print(' '),print(X),print(' ('),print(Aprime),print(','),print(Bprime),print(')'),nl,
    ((distinguished(Aprime,Bprime, yes) | distinguished(Bprime,Aprime,yes)) ->
    retract(distinguished(A,B,_)), assertz(distinguished(A,B, yes)),
    retractall(table_marked(_)), assertz(table_marked(yes))
    ,print(A),print(' '),print(B),print(' '),print(yes),nl
    ;true),
    fail.

construct_distinguished_table :-
    (table_marked(yes) ->
    retractall(table_marked(_)), assertz(table_marked(no)), construct_distinguished_table;true).

convert_string_to_code_list(ListA, CodeListA, Delimitor) :-
    atom_codes(Delimitor,DelimitorCodeList),
    convert_string_to_code_list_helper(ListA, CodeListA,DelimitorCodeList).

convert_string_to_code_list_helper([],[],_).

convert_string_to_code_list_helper([H|T],[Hhh|Tt],DelimitorCodeList_) :-
    (T == [] ->
    DelimitorCodeList = [];DelimitorCodeList = DelimitorCodeList_),
    atom_codes(H,Hh),append(Hh,DelimitorCodeList,Hhh),
    convert_string_to_code_list_helper(T,Tt,DelimitorCodeList).

dfa_cleanup :-
    retractall(equivalence_clazz(_)),retractall(distinguished(_,_,_)),
    retractall(table_marked(_)),retractall(min_dfa_state(_,_)).

ent03r_flatten([],[]) :- !.

ent03r_flatten([X|L],R) :- !, ent03r_flatten(X,XR), ent03r_flatten(L,LR), append(XR,LR,R).

ent03r_flatten(X,[X]).

ent03r_union([],X,X).

ent03r_union([X|R],Y,Z) :- member(X,Y),!,ent03r_union(R,Y,Z).

ent03r_union([X|R],Y,[X|Z]) :- ent03r_union(R,Y,Z).

extract_graph_of_state_merge(Graph) :-
    % check if user has specified all transitions
    (use_all_operations(signature_merge,yes) ->
    set_use_all_operations(signature_merge,yes)
    ; true),
    clean_up_after_printing,
    print_message('Performing State Merge'),
    state_merge,
    print_message('Generating States'),
    extract_state_merge_states(States),
    print_message('Generating Transitions'),
    extract_state_merge_transitions(Transitions),
    Graph = [States,Transitions].

extract_state_for_graph(State) :-
    state_merge_equivalence_class(Sig,Id,OK),
    State = state(Sig,Id,OK).

extract_state_merge_states(States) :-
    findall(State,extract_state_for_graph(State),States).

extract_state_merge_transition(Transition) :-
    transition(State,_,IndividualSig,To),
    find_state_merge_equivalence_class_for_state(State,ID1),
    find_state_merge_equivalence_class_for_state(To,ID2),
    assert_non_det_trans(State,ID1,IndividualSig,ID2),
    (desired_user_transition(signature_merge,IndividualSig) ->
    extract_transition_representation(ID1,IndividualSig,ID2,Color,Style)
    ; (signature_merge_show_all_transitions(yes) ->
    (non_def_trans(ID1,IndividualSig) ->
    true
    ; assertz(non_def_trans(ID1,IndividualSig))),
    extract_transition_representation(ID1,IndividualSig,ID2,Color,Style)
    ; true)
    ),
    Transition = trans(ID1,IndividualSig,ID2,Color,Style).

extract_state_merge_transitions(Transitions) :-
    findall(Trans,extract_state_merge_transition(Trans),Transitions).

extract_transition_representation(A,IndividualSig,C,Color,Style) :-
    Trans = [A,IndividualSig,C],
    (transition_printed(Trans) ->
    fail
    ; assertz(transition_printed(Trans)),
    (find_state_merge_equivalence_class_for_state(root, A) ->
    /* Style = 'solid', Color='blue' % dealing with the root */
    (non_det_trans(A,IndividualSig,true) -> % not dealing with root
    Style = 'dotted' % there's more than one of these transitions
    ; Style = 'solid'),
    (non_def_trans(A,IndividualSig) ->
    Color = 'purple';Color = 'black')
    ; (non_det_trans(A,IndividualSig,true) -> % not dealing with root
    Style = 'dotted' % there's more than one of these transitions
    ; Style = 'solid'),
    (non_def_trans(A,IndividualSig) ->
    Color = 'purple';Color = 'blue'))
).

find_state_for_state_merge_equivalence_class(ClassID,State) :-
    state_signature(State,_SIG,_OK,ClassID).

find_state_merge_equivalence_class_for_state(State,ClassID) :-
    state_signature(State,_TransSig,_Status,ClassID),!.

findall_transitions(State,TransName,_) :-
    nfa_to_dfa_transition_filter(State,_,TransName,Succ),
    (transi_(State,Succ) ->
    true
    ; asserta(transi_(State,Succ))),
    fail.

findall_transitions(State,_,Result) :-
    findall(Succ,transi_(State,Succ),Result),retractall(transi_(_,_)).

gen_underscores(0,R) :- !,R=[].

gen_underscores(N,['_'|T]) :- N1 is N-1, gen_underscores(N1,T).

get_alphabet(GT, Alphabet) :-
    findall(Letter,(transition(_,L,_), %transition_for_user(L,LU),
    remove_transition_arg_dont_cares(GT,L,Letter)),Alphabet_),
    remove_dups(Alphabet_,Alphabet).

get_alphabet_signatures(Alphabet) :-
    findall(Letter,(transition(_,L,_),transition_info(L,_,_,Letter)),Alphabet_),remove_dups(Alphabet_,Alphabet).

get_args_as_strings([],[]).

get_args_as_strings([First|SecondPlus],[String|Tail]) :-
    translate_bvalue(First,String),
    get_args_as_strings(SecondPlus,Tail).

get_dfa_states(States) :-
    findall(S,map_dfa_state_to_id(_,S),Statess),
    sort(Statess,States).

get_representative_from_list(L,Representative) :-
    member(Representative, L),!.

get_transition_arguments('-->'(FAction,_),Args) :-
    nonvar(FAction),FAction =.. [_|Args],!.

get_transition_arguments(Action, Args) :- nonvar(Action), Action =.. [_|Args],!.

get_transition_arguments(_, Args) :- Args = 'err'.

graph_type(signature_merge).

graph_type(dfa_abstraction).

increment_counter(C) :-
    (counter(D) -> C is D + 1,retract(counter(_)),assertz(counter(C));C is 0,
    assertz(counter(C))).

init :-
    dfa_cleanup,assertz(table_marked(no)),get_dfa_states(States),init(States).

init([_|[]]).

init([H|T]) :-
    setup_distinguished_table(H, T),
    init(T).

init_equivalence_class_id :-
    (curr_equivalence_class_id(X) ->
    retract(curr_equivalence_class_id(X))
    ;true),
    assertz(curr_equivalence_class_id(0)).

make_counting_list(Length,DontCares,List) :-
    make_counting_list(0,Length,DontCares,List).

make_counting_list(End,End,_,[]) :- !.

make_counting_list(Counter,Length,DontCares,[Head|Tail]) :-
    (member(Counter,DontCares) ->
    Head = '_'
    ; Head is Counter),
    CounterAddOne is (Counter + 1),
    make_counting_list(CounterAddOne,Length,DontCares,Tail).

minimize_dfa(FullResult) :-
    init, construct_distinguished_table, assert_equivalence_clazzes,
    findall(X,equivalence_clazz(X),ReS),% retractall(equivalence_clazz(_)),
    findall([X,Y],distinguished(X,Y,'yes'),Result),
    %print(Result),nl,
    ent03r_flatten(Result, Flat_Re),remove_dups(Flat_Re, Resu),
    sort(Resu, Result_),
    %print('*'),print(Result_),nl,
    ent03r_flatten(ReS, Flat_Res),sort(Flat_Res,Flat_Res_),
    %print(Flat_Res_),nl,
    length(Result_,LR),length(Flat_Res_,FR),
    (LR =< FR ->
    ord_intersection(Result_, Flat_Res_,_,Diff)
    ; ord_intersection(Flat_Res_, Result_,_,Diff)),
    %print(Diff),nl,
    unflatten(Diff, Fat_Diff),append(ReS, Fat_Diff, FullResult),assert_min_dfa_states(FullResult).

move(S,T,R) :- move_(S,T,Rp),
    retractall(transi_(_,_)),ent03r_flatten(Rp,R),!.

move_([],_,[]).

move_([Head|Tail],T,R) :-
    move_(Head,T,R1),
    move_(Tail,T,R2),ent03r_union(R1,R2,R).

move_(S,T,R) :-
    findall_transitions(S,T,R).

next_equivalence_class_id(ID) :-
    (curr_equivalence_class_id(X) ->
    ID is X+1,
    retract(curr_equivalence_class_id(X)),
    assertz(curr_equivalence_class_id(ID))
    ; ID=0, assertz(curr_equivalence_class_id(ID))).

nfa_cleanup :-
    retractall(dfa_states_(_,_)),retractall(dfa_tran_(_,_,_)),
    retractall(final_states(_)),retractall(map_dfa_state_to_id(_,_)).

nfa_to_dfa :-
    nfa_cleanup,
    init_equivalence_class_id,
    /* findall(X,desired_user_transition(dfa_abstraction,X),Alphabet), */
    get_alphabet(dfa_abstraction,Alphabet),
    print('% Alphabet: '), print(Alphabet),nl,
    asserta(dfa_states_([root],no)),
    nfa_to_dfa_worker(Alphabet).

nfa_to_dfa :-
    get_dfa_states(States),
    map_dfa_state_to_id([root],ID1),
    (map_dfa_state_to_id([],ID2) ->
    List = [ID2,ID1], %add other final states here
    sort(List,SList),
    ord_subtract(States,SList,Finals)
    ; ord_subtract(States,[ID1],Finals)),
   
    assertz(final_states(Finals)).

nfa_to_dfa_transition_filter(A,B,Sig,D) :-
    transition(A,B,D),
    transition_info(B,_,_,SmallSig),
    remove_transition_arg_dont_cares(dfa_abstraction, B, Sig),
    desired_user_transition(dfa_abstraction,SmallSig).

nfa_to_dfa_worker(Alphabet) :-
    repeat,
    (dfa_states_(S,no) -> true;!,fail),
    %print('testing S = '),print(S),nl,
    retract(dfa_states_(S,no)),
    asserta(dfa_states_(S,yes)),
    % print(treating_dfa_state(S)),nl,
    (map_dfa_state_to_id(S,_) ->
    true
    ; next_equivalence_class_id(ID0),
    % print(new_equiv_class(ID0)),nl,
    asserta(map_dfa_state_to_id(S,ID0))),
    %print('*'),
    member(Letter,Alphabet),
    % print(computing_move(S,Letter)),nl,
    move(S,Letter,Res),
    sort(Res,Result),
    % print(move(S,Letter,Res)),nl,
    (dfa_states_(Result,_) ->
    true /* state already exists */
    ; asserta(dfa_states_(Result,no)), % register new, untreated state
    % print(new_successor_state(Result)),nl,
    (map_dfa_state_to_id(Result,_) ->
    true
    ; next_equivalence_class_id(ID1),
    % print(new_equiv_class(ID1)),nl,
    asserta(map_dfa_state_to_id(Result,ID1)))),
    %print('asserting '),print(Result),nl),
    map_dfa_state_to_id(S,ID2),
    map_dfa_state_to_id(Result,ID3),
    % print(dfa_tran(ID2,Letter,ID3)),nl,
    asserta(dfa_tran_(ID2,Letter,ID3)),fail.

nfa_to_dfa_worker(_).

number_of_equivalence_classes(X) :- curr_equivalence_class_id(X).

print_class_as_dotstate(ClassID,OK) :-
    (state_printed(ClassID) ->
    true
    ; assertz(state_printed(ClassID)),
    state_merge_state_colour(ClassID, StateColour),
    get_preference(dot_invariant_violated_node_colour,IColor),
    print_state_merge_state_id(ClassID),
    print(' ['),
    (find_state_merge_equivalence_class_for_state(root,ClassID) ->
    print('shape=invtriangle, color=green, '),
    print('label=\"\", id=\"'),print(root)"
    ; ((OK = invariant_violated) ->
    print('shape=ellipse, style=filled, fillcolor="'),"
    print(IColor),print('\", label=\"'),
    print_node_label(ClassID),print('\" , id=\"'),print_node_label(ClassID)
    ; print('shape=ellipse, color=\"'),print(StateColour),print('\", label=\"'),"
    print_node_label(ClassID),print('\" , id=\"'),print_node_label(ClassID))),
    print('\"];'),nl)."

print_dfa_from_nfa_states_id :-
    map_dfa_state_to_id(Reals,ID),
    ((Reals == []) -> fail;true),
   
    % work out outline colour
    ((member(A,Reals),transition(A,_,_)) -> % this node not is open (**in this dfa graph)
    get_preference(dot_normal_node_colour,OutColour)
    ; get_preference(dot_open_node_colour,OutColour)), % this node is open
   
    % work out fill colour
    ((invariant_violated(C), member(C,Reals)) ->
    get_preference(dot_invariant_violated_node_colour,InColour)
    ; true),
   
    % work out shape
    ((Reals == [root]) -> % its the root
    get_preference(dot_root_shape,Shape),
    print(root),print('[id="root", shape='),print(Shape),print(', color=green, label=""];'),nl,fail
    ; ((state_space:current_state_id(B),member(B,Reals)) -> % it contains the current state
    get_preference(dot_current_node_shape,Shape)
    ; get_preference(dot_normal_node_shape,Shape))), % it doesn't contain the current state
   
    % do the printing
    print(ID),print('[id='),print(ID),print(', shape='),print(Shape),print(', color=\"'),print(OutColour),print('\"'),
    (nonvar(InColour) -> print(', style=filled, fillcolor='),print(InColour); true),print('];'),nl,
    fail.

print_dfa_from_nfa_states_id.

print_dot_for_dfa_from_nfa(File) :-
    % use all operations if desired
    (use_all_operations(dfa_abstraction,yes) ->
    set_use_all_operations(dfa_abstraction,yes)
    ; true),
    % use no arguments if desired
    (use_no_arguments(dfa_abstraction,yes) ->
    set_use_no_arguments(dfa_abstraction,yes)
    ; true),
    print('% Converting NFA to DFA'),nl,
    nfa_to_dfa,
    number_of_equivalence_classes(Nr),
    format('% Writing DFA with ~w states to file: ~w~n',[Nr,File]),
    tell(File),
    print_graph_header(nfa_to_dfa),
    print_dfa_from_nfa_states_id,
    nl,
    print_dot_for_dfa_from_nfa_,
    print_graph_footer,
    told,
    (Nr>100 -> format('% Warning: viewing ~w states with dot can take time!~n',[Nr]) ; true).

print_dot_for_dfa_from_nfa_ :-
    dfa_tran_(ID1,Letter,ID2),
    map_dfa_state_to_id(ID1_reals, ID1),
    map_dfa_state_to_id(ID2_reals, ID2),
    ((ID2_reals == []) -> fail;true),
    ((ID1_reals == [root]) ->
    print(root)
    ; print(ID1)),
    print(' -> '),
    print(ID2),
    (map_dfa_state_to_id([root], ID1) ->
    print('[color=black, label=\"') %style=dotted,"
    ; ((ID1_reals \== ID2_reals,ord_subset(ID2_reals, ID1_reals)) ->
    print('[style=dotted,')
    ; print('[')),
    print('color=blue, label=\"')),"
    print(Letter),
    print('\"];'),"
    nl,
    fail.

print_dot_for_dfa_from_nfa_.

print_dot_from_node_list(_,File) :-
    tell(File),
    retractall(state_printed(_)),
    retractall(transition_printed(_)),
    print_graph_header(general_graph),fail.

print_dot_from_node_list(Llist,_) :-
    sort(Llist,List),
    member(N1,List),
    check_against_list(N1,List),fail.

print_dot_from_node_list(_,_) :-
    print_graph_footer,told.

print_min_dfa__representatives_transitions_ :-
    min_dfa_state(_,Representative),
    dfa_tran_(Representative,Letter,Succ),
    min_dfa_state(State,SuccRepresentative),
   
    map_dfa_state_to_id(RealRep,Representative),
    RealRep \== [],
    map_dfa_state_to_id(RealSuccRep,SuccRepresentative),
    RealSuccRep \== [],
   
    member(Succ,State),
    print(Representative),
    print(' -> '),
    print(SuccRepresentative),
    (RealRep == [root] ->
    print('[style=dotted, color=black, label=\"')"
    ; print('[color=blue, label=\"')),"
    print(Letter),
    print('\"];'),"
    nl,
    fail.

print_min_dfa__representatives_transitions_.

print_min_dfa_for_dot(File) :-
    nfa_to_dfa,
    minimize_dfa(_),
    % for each min_dfa_state, get a representative state, for each letter of the alphabet, print the transition
    % and the representative state to which the transition leads
    tell(File),
    print_graph_header(minimum_dfa),
    print_min_dfa_states_representatives_for_dot,
    print_min_dfa__representatives_transitions_,
    print_graph_footer,
    told.

print_min_dfa_for_dot(_).

print_min_dfa_states_representatives_for_dot :-
    min_dfa_state(_,ID),
    map_dfa_state_to_id(RealRep,ID),
    (RealRep == [] -> fail;true),
    (RealRep == [root] ->
    print(ID),print('[shape=invtriangle, color=green, label=""];'),nl,fail "#0d9d03"
    ; print(ID), print('[shape=ellipse, color=black, label=\"'),print(ID),"
    print('\", id='),print(ID),print('];'),nl,fail)."

print_min_dfa_states_representatives_for_dot.

print_node_label(ClassID) :-
    (preference(dot_print_node_ids,false)
    -> state_merge_equivalence_class(Signature,ClassID,_OK),
    print(Signature)
    ; preference(dot_print_node_info,true)
    -> state_merge_equivalence_class(Signature,ClassID,_OK),
    print(ClassID),print('\\n'), print(Signature)
    ; print(ClassID)
).

print_state_merge_for_dot :-
    % check if user has specified all transitions
    (use_all_operations(signature_merge,yes) ->
    set_use_all_operations(signature_merge,yes)
    ; true),
    clean_up_after_printing,
    print_message('Performing State Merge'),
    state_merge,
    print_graph_header(state_merge),
    print_message('Generating Dot States'),
    print_state_merge_states_for_dot,
    print_message('Generating Dot Transitions'),
    print_state_merge_transitions_for_dot,
    print_graph_footer.

print_state_merge_for_dot(File) :- print_state_merge_for_dot2(File).

print_state_merge_for_dot2(File) :-
    tell(File),print_state_merge_for_dot,told.

print_state_merge_state_id(State) :-
    (find_state_merge_equivalence_class_for_state(root,State) -> print(root)
    ; print(State)).