visualize_graph

convert_state_to_string(root,'root') :- !.

convert_state_to_string(State,String) :-
    get_animation_expression_value(State,V),!,
    String=V.

convert_state_to_string(StateTempl,StateAsString) :- animation_mode(xtl),!,
    convert_state_to_string_default(StateTempl,StateAsString).

convert_state_to_string(concrete_constants(CurTemp),StateAsString) :- !,
    findall(FProp,elementary_prop(CurTemp,FProp),State), /* was fd_findall */
    translate_params_for_dot(State,StateAsString).

convert_state_to_string(const_and_vars(ConstID,StateTempl),StateAsString) :- !,
    set_translation_constants(ConstID),
    convert_state_to_string(StateTempl,StateAsString),
    clear_translation_constants.

convert_state_to_string(csp_and_b(CSPState,BState),StateAsString) :- !,
    translate_cspm_state(CSPState,CSPText),
    convert_state_to_string(BState,BString),
    string_concatenate(CSPText,'\n',C2),
    string_concatenate(C2,BString,StateAsString).

convert_state_to_string([H|T],StateAsString) :- !,
    CurTemp=[H|T],
    findall(FProp,elementary_prop(CurTemp,FProp),State), /* was fd_findall */
    translate_params_for_dot(State,StateAsString).

convert_state_to_string(StateTempl,StateAsString) :-
    convert_state_to_string_default(StateTempl,StateAsString).

convert_state_to_string_default(StateTempl,StateAsString) :-
    findall(FProp,
    (property(StateTempl,Prop),filter_elementary_prop(Prop,FProp)),
    State), /* was fd_findall */
    translate_params_for_dot(State,StateAsString).

dfs(ID,Dist) :- unfiltered_state(ID,D1), (D1>=Dist -> ! ; retract(unfiltered_state(ID,D1))),fail.

dfs(ID,Dist) :- assertz(unfiltered_state(ID,Dist)), D1 is Dist-1,
    D1>0,
    any_transition(ID,_,NodeID),
    dfs(NodeID,D1).

directly_representable_element(X) :- dot_state_basic_type(X).

directly_representable_element((X1,X2)) :-
    dot_state_basic_type(X1),
    dot_state_basic_type(X2).

dot_arc_color(_,Action,ArcCol) :-
    get_label_nr(Action,Nr), Nr>0,
    translate_int_col(Nr,ArcCol),
    !.

dot_arc_color(_TransId,_Action, ArcCol) :-
    (preference(dot_normal_arc_colour,ArcCol) -> true ; ArcCol=blue).

dot_def_node(0,none,'No DEFINITIONS visible',box,none,red) :-
    \+ b_get_definition(_,_,_,_,_),!.

dot_def_node(DEFID,SubGraph,Desc,box,none,Color) :-
    findall(Called, (b_get_definition(_,_,_,_,Deps), member(Called,Deps)),CD),
    (CD=[] -> get_preference(dot_definitions_show_all,true) ; true), !,
    sort(CD,CalledDefs),
    b_get_definition(DEFID,DefType,Args,_Body,Deps),
    length(Args,NrArgs),
    tools:ajoin([DEFID,'/',NrArgs],Desc), % TO DO: improve
    (get_preference(dot_definitions_use_sub_graph,true) -> SubGraph = DefType ; SubGraph=none),
    (get_preference(dot_definitions_show_all,true) -> true
    ; Deps = [_|_] -> true % show if it calls another one
    ; ord_member(DEFID,CalledDefs) % show if called
    ),
    (DefType = predicate -> Color = green ; Color = blue).

dot_def_node(0,none,'No DEFINITIONS called',box,none,blue).

dot_def_subgraph(SubGraph,filled,lightgray) :-
    get_preference(dot_definitions_use_sub_graph,true),
    member(SubGraph,[predicate,expression,substitution]),
    (b_get_definition(_,SubGraph,_,_,_) -> true).

dot_def_trans(NodeID,Label,SuccNodeID,Color,Style) :- Style=solid,
    b_get_definition(NodeID,_DefType,_Args,_Body,Deps),
    Label = 'call',
    member(SuccNodeID,Deps),
    (Deps = [_] -> Color = black ; Color = blue).

dot_node_color(StateId,Color) :-
    % an open state where not all transitions are yet calculated
    not_all_transitions_added(StateId),!,
    get_preference(dot_open_node_colour,Color).

dot_node_color(StateId,Color) :-
    % a state which is outside the user-defined state space that should be model-checked
    not_interesting(StateId),!,
    get_preference(dot_scope_limit_node_colour,Color).

dot_node_color(StateId,Color) :-
    transition(StateId,'*permute*',_),!, Color = lightgray.

dot_node_color(StateId,Color) :-
    %get_preference(dot_normal_node_colour,Color),
    compute_heuristic_function_for_state_id(StateId,HRes),
    !,
    translate_bvalue_to_colour(HRes,Color). %tools:print_message(heur(HRes,Color)).

dot_node_color(_StateId,Color) :-
    get_preference(dot_normal_node_colour,Color).

dot_node_shape(_StateId,State,triangle) :-
    % state with abort values
    memberchk(bind(_,term(no_value_for(_))),State),!.

dot_node_shape(root,_State,Shape) :-
    % the root state
    !,get_preference(dot_root_shape,Shape).

dot_node_shape(StateId,_State,Shape) :-
    % the currently displayed state in the animation
    current_state_id(StateId),!,
    get_preference(dot_current_node_shape,Shape).

dot_node_shape(StateId,_State,diamond) :-
    % a state which was subject to permutation flooding
    transition(StateId,'*permute*',_),!.

dot_node_shape(_StateId,_State,Shape) :-
    % a normal state
    get_preference(dot_normal_node_shape,Shape).

dot_pred_node(Preds,PID,none,EDesc,box,none,blue) :- member(pred(PID,Pred,_),Preds),
    translate:translate_bexpression_with_limit(Pred,Desc),
    string_escape(Desc,EDesc).

dot_pred_trans(Preds,NodeID,Label,SuccNodeID,Color,Style) :- Style=solid, Color=black,
    member(pred(NodeID,_,Ids1),Preds),
    member(pred(SuccNodeID,_,Ids2),Preds), SuccNodeID>NodeID,
    ord_intersection(Ids1,Ids2,Label), Label \= [].

dot_print_action(_) :- preference(dot_print_edge_labels,false),!.

dot_print_action(Action) :- preference(dot_print_action_arguments,true),
    translate:translate_event(Action,ActionAsString),
    print_string_for_dot(ActionAsString),!.

dot_print_action('-->'(FAction,_R)) :- nonvar(FAction),
    functor(FAction,OperationName,_),!,
    print_string_for_dot(OperationName).

dot_print_action(Action) :- nonvar(Action), functor(Action,OperationName,_),!,
    print_string_for_dot(OperationName).

dot_print_action(Action) :- print('err:'),print_string_for_dot(Action).

dot_state_basic_pair((X1,X2),X1,X2).

dot_state_basic_pair([H|T],X1,X2) :- member((X1,X2),[H|T]).

dot_state_basic_pair(avl_set(A),X1,X2) :- avl_member((X1,X2),A).

dot_state_basic_type(fd(_,_)).

dot_state_basic_type(int(_)).

dot_state_basic_type(pred_false /* bool_false */).

dot_state_basic_type(pred_true /* bool_true */).

dot_state_basic_type(string(_)).

dot_state_basic_type_or_element(X,X) :- dot_state_basic_type(X).

dot_state_basic_type_or_element(S,X) :- member(X,S), dot_state_basic_type(X).

dot_state_basic_type_or_element([],empty_set).

dot_state_node(ID,SET,Desc,box,none,Color) :-
    b_global_set(SET), Desc = ID,
    if(is_b_global_constant(SET,_Nr,Cst),
    (Color=red,ID = Cst),
    (Color=blue,
    all_elements_of_type(SET,AllVals),
    member(X,AllVals),
    translate_bvalue(X,ID)
)
).

dot_state_node(root,none,'','Mdiamond',none,green).

dot_state_trans(State,NodeID,Label,SuccNodeID,Color,Style) :- Style=solid,
    get_id_value(VarOrConstant,State,VarValue),
    dot_state_trans_var(VarValue,NodeID,SuccNodeID,VarOrConstant,Label),
    (b_is_constant(VarOrConstant) -> Color=blue ; Color=black).

dot_state_trans_internal(IntNode,Kind,VarValue,NodeID,SuccNodeID,Label) :-
    dot_state_basic_type_or_element(VarValue,V),
    translate_bvalue(V,SuccNodeID),
    NodeID = IntNode, Label=Kind.

dot_state_trans_internal(IntNode,Kind,VarValue,NodeID,SuccNodeID,Label) :-
    dot_state_basic_pair(VarValue,X1,X2), /* we have a relation or a pair */
    dot_state_basic_type_or_element(X1,El1),
    dot_state_basic_type_or_element(X2,El2),
    NodeID = IntNode,
    ( (translate_bvalue(El1,SuccNodeID), Label = prj1(Kind))
    ;(translate_bvalue(El2,SuccNodeID), Label = prj2(Kind))
).

dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Var) :-
    dot_state_basic_pair(VarValue,X1,X2), /* we have a relation or a pair */
    dot_state_basic_type(X1), El1=X1,
    dot_state_basic_type(X2), El2=X2, /* in case it is a function: we can also accept El2 to be dot_state_basic_type_or_element */
    translate_bvalue(El1,NodeID),
    translate_bvalue(El2,SuccNodeID).

dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Var) :-
    dot_state_basic_type_or_element(VarValue,V),
    NodeID = root,
    translate_bvalue(V,SuccNodeID).

dot_state_trans_var(VarValue,NodeID,SuccNodeID,Var,Label) :-
    ( (member(X,VarValue),Kind=el)
    ; (VarValue=(X,_),Kind=prj1)
    ; (VarValue=(_,X),Kind=prj2)
    ),
    \+ directly_representable_element(X),
    gensym(Var,IntNode),
    ((NodeID = root, SuccNodeID = IntNode, Label=Var)
    ;
    dot_state_trans_internal(IntNode,Kind,X,NodeID,SuccNodeID,Label)
).

dot_subgraph(SubGraph,filled,lightgray) :-
    b_global_set(SubGraph).

extract_b_store(csp_and_b(_,T),R) :- !, R=T.

extract_b_store(R,R).

extract_full_store(concrete_constants(C),R) :- !,R=C.

extract_full_store(const_and_vars(ConstID,Vars),R) :- !,
    specfile:expand_const_and_vars(ConstID,Vars,R).

extract_full_store(R,R).

filter_elementary_prop(X,R) :- \+ b_or_z_mode,!,R=X.

filter_elementary_prop('='(Cst,_V),_) :- nonvar(Cst),
    b_is_constant(Cst),!,fail.

filter_elementary_prop(Relation,_) :-
    functor(Relation,Func,_),
    b_is_constant(Func),!,fail.

filter_elementary_prop('='(_X,pred_false /* bool_false */),_) :- !,fail. /* do not show boolean variables that are false */

filter_elementary_prop('='( X,pred_true /* bool_true */), X) :- !. /* just show the boolean variable, not that it is = true */

filter_elementary_prop(X,X).

get_animation_expression_value(State,PropAsString) :-
    b_or_z_mode,
    b_get_machine_animation_expression('ANIMATION_EXPRESSION',AExpr),
    state_corresponds_to_fully_setup_b_machine(State,BState),
    b_interpreter:b_compute_expression_nowf(AExpr,[],BState,AValue,'ANIMATION_EXPRESSION',0),
    translate:translate_bvalue(AValue,PropAsString).

get_label_nr(Action,Nr) :- functor(Action,F,_),
    (label_nr(F,FNr) -> Nr=FNr
    ; retract(next_label_nr(N)), N1 is N+1, assertz(next_label_nr(N1)), assertz(label_nr(F,N)), Nr=N).

get_pred_ids([],_,[]).

get_pred_ids([Pred|T],N,[pred(N,Pred,Ids)|PT]) :- predicate_identifiers(Pred,Ids),
    N1 is N+1, get_pred_ids(T,N1,PT).

get_state_property(State,PropAsString) :-
    specfile:property(State,Prop),
    translate:translate_property_with_limit(Prop,320,PropAsString).

is_goal_node(NodeID) :- preference(dot_colour_goal_nodes,true),
    node_satisfies_goal(NodeID). % TO DO csp goal

my_conjunction_to_list(b(exists(_,Body),pred,_),L) :- !, my_conjunction_to_list(Body,L).

my_conjunction_to_list(B,L) :- conjunction_to_list(B,L).

my_parse_predicate(RawAST,Typed) :- compound(RawAST),!,
    type_with_errors(RawAST,[variables],Type,Typed),
    (Type=pred -> true
    ; add_error(visualize_graph,'Expected predicate by got:',Type),fail).

my_parse_predicate(Pred,Typed) :-
    atom_codes(Pred,Codes),
    eval_strings:repl_parse_predicate(Codes,exists,Typed,_).

next_label_nr(0).

print_graph_footer :- print('}'),nl.

print_graph_header(Type) :-
    format('digraph ~w {~n',[Type]),
    % print('graph [orientation=landscape, page="8.5, 11",ratio=fill,size="7.5,10"];'),nl. % old default layout
    % print('graph [page="8.5, 11",ratio=fill,size="7.5,10"];'),nl.
    print('graph [nodesep=1.5, ranksep=1.5];'), nl.

print_graph_header_with_layout(Type,Layout) :-
    format('digraph ~w {~n',[Type]),
    format('graph [nodesep=1.5, ranksep=1.5, layout=~w];~n',[Layout]).

print_node_properties(ID) :-
    print(' Prop={'),
    visited_expression(ID,State),
    get_state_property(State,PropAsString),
    print_string_for_dot(PropAsString), print('\\'),print('n'),
    fail.

print_node_properties(_) :- print('}').

print_predicate_dependency_as_graph_for_dot(Typed,File) :-
    my_conjunction_to_list(Typed,Conj),
    get_pred_ids(Conj,1,Preds),
    gen_dot_graph(File,dot_pred_node(Preds),dot_pred_trans(Preds)).

print_string_for_dot(String) :- string_escape(String,EString),
    wrap_and_truncate_atom(EString,50,350,NS), print(NS).

print_trace_to_current_state(IDList) :-
    samsort(IDList,SIDList), % keeps duplicates
    clumps(SIDList,Clumps),
    member([NodeID|T],Clumps),
    (length([NodeID|T],Len),Len>1
    -> ajoin(['repeated (',Len,')'],Lbl),
    tcltk_print_node_for_dot(NodeID,[extralabel/Lbl])
    ; tcltk_print_node_for_dot(NodeID)),
    fail.

print_trace_to_current_state(IDList) :-
    temporary_set_preference(dot_print_self_loops,true,CHNG3),
    print_trace_to_current_state2(IDList),
    preferences:reset_temporary_preference(dot_print_self_loops,CHNG3).

print_trace_to_current_state2([]).

print_trace_to_current_state2([_]).

print_trace_to_current_state2([ID1,ID2|Tail]) :-
    tcltk_print_transitions_for_dot(ID1,ID2),
    print_trace_to_current_state2([ID2|Tail]).

print_trace_with_neighbors_to_current_state(IDList) :- sort(IDList,SIDList),
    member(NodeID,SIDList),
    tcltk_print_node_for_dot(NodeID),
    fail.

print_trace_with_neighbors_to_current_state(IDList) :-
    current_state_id(CurID),
    nth1(N,IDList,CurID,_Rest),!,
    append_length(PathToLoop,LoopIDs,IDList,N),
    %format(user_output,'~w pos=~w : ~w , path to loop=~w, loop=~w~n',[CurID,N,IDList,PathToLoop,LoopIDs]),
    temporary_set_preference(dot_print_self_loops,true,CHNG3),
    print_trace_to_current_state2(PathToLoop), % print path to loop
    print_trace_with_neighbors_to_current_state2([CurID|LoopIDs],IDList), % print loop (with neighbors, because of the fairness check),
    preferences:reset_temporary_preference(dot_print_self_loops,CHNG3).

print_trace_with_neighbors_to_current_state2([],_).

print_trace_with_neighbors_to_current_state2([ID|Tail],IDList) :-
    findall(ID,(transition(ID,_,_,SuccID),
    \+ append(_,[ID,SuccID|_],IDList), % check if the edge is not already shown
    % format(user_output,'Neighb: ~w -> ~w : idlist=~w, tail=~w~n',[ID,SuccID,IDList,Tail]),
    tcltk_print_transitions_for_dot(ID,SuccID)),_IDList),
    print_trace_with_neighbors_to_current_state2(Tail,IDList).

reset_label_nr :- retractall(label_nr(_,_)), retractall(next_label_nr(_)).

reset_label_nr(Colour) :- reset_label_nr,
    (Colour=colour_transitions
    -> assertz(next_label_nr(0)) % asserts next label nr: we will colour transitions
    ; true).

tcltk_print_csp_process_states_for_dot :-
    dvisited(NodeID),
    tcltk_print_node_for_dot(NodeID),
    tcltk_print_transitions_for_dot(NodeID,_),
    fail.

tcltk_print_csp_process_states_for_dot :-
    print_graph_footer.

tcltk_print_csp_process_states_for_dot(F,ProcID) :-
    tell(F),(tcltk_print_csp_process_states_for_dot_root(ProcID) -> true ; true),told.

tcltk_print_csp_process_states_for_dot_root(ProcID) :-
    reset_label_nr,
    print_graph_header(csp_process),
    tcltk_print_node_for_dot(root),
    tcltk_print_transitions_for_dot(root,ProcID),
    tcltk_print_csp_process_states_for_dot.

tcltk_print_current_state_as_graph_for_dot(File) :-
    current_expression(_CurID,State),
    tcltk_print_state_as_graph_for_dot(State,File).

tcltk_print_current_state_for_dot :-
    reset_label_nr,
    print_graph_header(current_state),
    current_state_id(CurID),
    ( NodeID=CurID ;
    any_transition(CurID,_,NodeID)),
    tcltk_print_node_for_dot(NodeID),
    fail.

tcltk_print_current_state_for_dot :-
    current_state_id(CurID),
    tcltk_print_transitions_for_dot(CurID,_),
    fail.

tcltk_print_current_state_for_dot :-
    print_graph_footer.

tcltk_print_current_state_for_dot(F) :-
    tell(F), (tcltk_print_current_state_for_dot -> true ; true),told.

tcltk_print_definitions_as_graph_for_dot(File) :-
    gen_dot_graph(File,dot_def_node,dot_def_trans,dot_no_same_rank,dot_def_subgraph).

tcltk_print_history_to_current_state_for_dot :-
    reset_label_nr,
    print_graph_header(history),
    current_state_id(CurID),
    history(H),
    reverse([CurID|H],IDList),
    print_trace_to_current_state(IDList),
    print_graph_footer.

tcltk_print_history_to_current_state_for_dot(F) :-
    tell(F), (tcltk_print_history_to_current_state_for_dot -> true ; true),told.

tcltk_print_history_to_current_state_with_neighbors_for_dot :-
    reset_label_nr,
    print_graph_header(history),
    current_state_id(CurID),
    history(H),
    reverse([CurID|H],IDList),
    print_trace_with_neighbors_to_current_state(IDList),
    print_graph_footer.

tcltk_print_history_to_current_state_with_neighbors_for_dot(F) :-
    tell(F), (tcltk_print_history_to_current_state_with_neighbors_for_dot -> true ; true),told.

tcltk_print_neighbourhood_states_for_dot(Dist,F) :-
    retractall(unfiltered_state(_,_)),
    current_state_id(CurID),
    (dfs(CurID,Dist) -> true ; true), % mark neighbours until distance Dist
    tell(F),(tcltk_print_unfiltered_states_for_dot -> true ; true),told.

tcltk_print_node_for_dot(ID) :- tcltk_print_node_for_dot(ID,[]).

tcltk_print_node_for_dot(NodeID,Options) :-
    animation_mode(AM),
    visited_expression(NodeID,CurT),
    extract_b_store(CurT,CurBT),
    extract_full_store(CurBT,CurTemp),
    (NodeID=root -> preference(dot_print_root,true) ; true),
    (member(shape/Shape,Options) -> true ; dot_node_shape(NodeID,CurTemp,Shape)),
    % TO DO: penwidth=2.0, fillcolor="#F1F2D8"
    (find_invariant_error(AM,NodeID,CurTemp,_)
    -> get_preference(dot_invariant_violated_node_colour,NodeColor),
    Style=filled
    ; counterexample_node(NodeID)
    -> get_preference(dot_counterexample_node_colour,NodeColor),
    (is_goal_node(NodeID) -> Style = 'rounded,filled', get_preference(dot_goal_node_colour,FillColor)
    ; Style=none, FillColor=none)
    ; is_goal_node(NodeID)
    -> get_preference(dot_goal_node_colour,NodeColor),
    Style='rounded,filled'
    ; (preference(dot_fill_normal_nodes,true) -> Style='rounded,filled' ; Style=none),
    (member(color/NodeColor,Options) -> true ; dot_node_color(NodeID,NodeColor))
    ),
    (member(fontsize/FSize,Options) -> true ; get_preference(dot_node_font_size,FSize)),
    (Style=none
    -> format('~w [shape=~w, color=\"~w\", fontsize=~w',[NodeID,Shape,NodeColor,FSize])
    ; FillColor=none
    -> format('~w [shape=~w, style=\"~w\", color=\"~w\", fontsize=~w',[NodeID,Shape,Style, NodeColor,FSize])
    ; format('~w [shape=~w, style=\"~w\", color=\"~w\", fillcolor=\"~w\", fontsize=~w',
    [NodeID,Shape,Style, NodeColor,FillColor,FSize])
    ),
   
    (member(pendwidth/PenWidth,Options) -> true ; get_preference(dot_node_penwidth,PenWidth)),
    (PenWidth = 1 -> true ; print(', penwidth='), print(PenWidth)),
    print(', label=\"'),"
    (member(extralabel/ExtraLbl,Options) -> print_escaped(ExtraLbl), print('\\n') ; true),
    (preference(dot_print_node_ids,true) -> print(NodeID), print(':\\n') ; true),
    (preference(dot_print_node_info,true)
    -> convert_state_to_string(CurT,StateAsString),
    print_escaped(StateAsString) % quoted encode; except for
    ; true
    ),
    (preference(dot_print_node_properties,true)
    -> print_node_properties(NodeID)
    ; true
    ),
    print('\"];'),nl,"
    fail.

tcltk_print_node_for_dot(_NodeID,_) :- nl.

tcltk_print_predicate_dependency_as_graph_for_dot(Pred,File) :-
    my_parse_predicate(Pred,Typed),
    print_predicate_dependency_as_graph_for_dot(Typed,File).

tcltk_print_shortest_trace_to_current_state_for_dot :-
    reset_label_nr,
    print_graph_header(shortest_trace_to_current_state),
    current_state_id(CurID),
    find_shortest_trace_to_node(root,CurID,_,StateIDList),
    print_trace_to_current_state(StateIDList),
    print_graph_footer.

tcltk_print_shortest_trace_to_current_state_for_dot(F) :-
    tell(F), (tcltk_print_shortest_trace_to_current_state_for_dot -> true ; true),told.

tcltk_print_state_as_graph_for_dot(State,File) :-
    %print(gen_graph(State)),nl,
    gen_dot_graph(File,dot_state_node,dot_state_trans(State),dot_no_same_rank,dot_subgraph).

tcltk_print_states_for_dot(F) :- tcltk_print_states_for_dot(F,no_colour_for_transitions).

tcltk_print_states_for_dot(F,ColourTransitions) :-
    format('Writing states to dot file ~w~n',[F]),
    tell(F),(tcltk_print_states_for_dot_aux(ColourTransitions) -> true ; true),told.

tcltk_print_states_for_dot_aux(ColourTransitions) :-
    reset_label_nr(ColourTransitions),
    print_graph_header(visited_states),
    visited_expression_id(NodeID),
    tcltk_print_node_for_dot(NodeID),
    tcltk_print_transitions_for_dot(NodeID,_),
    fail.

tcltk_print_states_for_dot_aux(_ColourTransitions) :-
    print_graph_footer.

tcltk_print_states_for_dot_sfdp(F) :-
    tcltk_print_states_for_dot_sfdp(F,colour_transitions).

tcltk_print_states_for_dot_sfdp(F,ColourTransitions) :-
    temporary_set_preference(dot_print_node_info,false,CHNG1),
    temporary_set_preference(dot_print_node_properties,false,CHNG2),
    temporary_set_preference(dot_print_self_loops,false,CHNG3),
    temporary_set_preference(dot_fill_normal_nodes,true,CHNG4),
    call_cleanup(tcltk_print_states_for_dot(F,ColourTransitions),
    (preferences:reset_temporary_preference(dot_print_node_info,CHNG1),
    preferences:reset_temporary_preference(dot_print_node_properties,CHNG2),
    preferences:reset_temporary_preference(dot_print_self_loops,CHNG3),
    preferences:reset_temporary_preference(dot_fill_normal_nodes,CHNG4))).

tcltk_print_transitions_for_dot(NodeID,SuccID) :-
    transition(NodeID,Action,TransID,SuccID),
    visited_expression(NodeID,State), set_translation_context(State),
    (NodeID=root -> preference(dot_print_root,true) ; true),
    (Action = '-->'(_Func,_)
    -> (NodeID \= SuccID ; preference(dot_print_functions,true))
    ; true),
    (NodeID \= SuccID -> true ; preference(dot_print_self_loops,true)),
    format('~w -> ~w',[NodeID,SuccID]),
    (preference(dot_print_arc_colors,true) ->
    (NodeID==root
    -> print(' [style = dotted, color = black, label=\"')"
    ; (Action = '*permute*'
    -> ArcCol=gray
    ; counterexample_op(TransID)
    -> get_preference(dot_counterexample_op_colour,ArcCol)
    ; dot_arc_color(TransID, Action, ArcCol)
    ),
    format(' [color = \"~w\", label=\"',[ArcCol])"
    )
    ; print(' [label=\"')"
    ),
    dot_print_action(Action),
    (get_preference(dot_print_transition_ids,true) -> format('\n~w',[TransID]) ; true),
    get_preference(dot_edge_font_size,FSize),
    get_preference(dot_edge_penwidth,PenWidth),
    (PenWidth = 1
    -> format('\", fontsize=~w];~n',[FSize])"
    ; format('\", fontsize=~w, penwidth=~w];~n',[FSize,PenWidth])"
    ),
    fail.

tcltk_print_transitions_for_dot(_NodeID,_SuccID) :- clear_translation_constants,nl.

tcltk_print_unfiltered_states_for_dot :- reset_label_nr,
    print_graph_header_with_layout(neighbourhood,sfdp),
    unfiltered_state(NodeID,Dist),
    tcltk_print_node_for_dot(NodeID,[pendwidth/Dist]),
    tcltk_print_transitions_for_dot(NodeID,_),
    fail.

tcltk_print_unfiltered_states_for_dot :-
    print_graph_footer.