fdr_csp_generator

assert_tau_found_fail :- \+ tau_found, assertz(tau_found), fail.

convert :-
    print_overall_header,
    (current_mode(fdr) -> true /* no need to print channels */ ; print_channels),
    gen_process.

convert_b_2_csp :-
    retractall(current_mode(_)), assertz(current_mode(fdr)),
    convert.

convert_b_2_promela :-
    retractall(current_mode(_)), assertz(current_mode(spin)),
    convert.

current_mode(fdr).

fdr_translate_event(Transition,String) :-
    csp_with_bz_mode,!,
    fdr_translate_event2(Transition,String).

fdr_translate_event(Transition,String) :-
    translate_event(Transition,String).

fdr_translate_event2(io(Values,Channel,_Span),String) :- !,
    translate_event(io(Values,Channel),String). % omit "CSP: ..."

fdr_translate_event2('-->'(Operation,OutputValues),String) :- !,
    Operation =.. [Channel|InputValues],
    append(InputValues,OutputValues,Values),
    fdr_translate_operation(Channel,Values,String).

fdr_translate_event2(Event,String) :-
    is_csp_event(Event),!,translate_event(Event,String).

fdr_translate_event2(Operation,String) :-
    Operation =.. [Channel|Values],
    fdr_translate_operation(Channel,Values,String).

fdr_translate_operation(Name,Values,String) :-
    maplist(translate_bvalue,Values,ValueStrings),
    inject_dots([Name|ValueStrings],Strings),
    ajoin(Strings,String).

gen_process :- print_transition_header,fail.

gen_process :-
    visited_expression_id(NodeIDs),
    print_process_declaration_header(NodeIDs),
    retractall(selectsymbol),
    (transition_for_fdr(NodeIDs,_,_) -> process_detail(NodeIDs)
    ; (not_all_transitions_added(NodeIDs)
    -> print_open_detail(NodeIDs) ; print_stop_detail(NodeIDs))
    ),
    print_process_declaration_footer(NodeIDs), fail.

gen_process:- print_transition_footer.

gen_tran:-
    transition_for_fdr(StateID,TransAsTerm,TID),
    (channel(TransAsTerm,_,StateID,_) -> fail
    ; (translate_event(TransAsTerm,Trans),
    generate_transition_id(TransAsTerm,Trans,FDRTransID),
    assertz(channel(TransAsTerm,FDRTransID,StateID,TID))
    )
    ),fail.

gen_tran.

generate_transition_id(TransAsTerm,_,TransID) :-
    var(TransAsTerm),!,TransID = error_trans_is_var.

generate_transition_id(TransAsTerm,_,TransID) :- atomic(TransAsTerm),!,TransID = TransAsTerm.

generate_transition_id(TransAsTerm,Transs,TransID) :-
    functor(TransAsTerm,Func,_),
    (Func = ('-->')
    -> arg(1,TransAsTerm,Arg), generate_transition_id(Arg,Transs,TransID)
    ; ((Func = '$initialise_machine' ; Func = '$setup_constants')
    -> TransID = Func
    ; Transs = TransID %char_translate(Transs,TransID)
)
).

inject_dots([],[]).

inject_dots([E],[E]) :- !.

inject_dots([H|T],[H,'.'|NT]) :-
    inject_dots(T,NT).

is_csp_event(start_cspm(_)).

is_csp_event(tick(_)).

is_csp_event(tau(_)).

is_csp_event(io(_,_,_)).

is_csp_event(io(_,_)).

is_tau(tau(_)).

is_tau(start_cspm_MAIN).

print_channel_keyword :- current_mode(fdr),!,
    print('channel ').

print_channel_keyword :- print('chan ').

print_channels :-
    %time(fdr_csp_generator:gen_tran),
    gen_tran,
    retractall(commasymbol),
    retractall(written_channel(_)),
    write_tran,nl.

print_comma:-
    (commasymbol -> print(',') ; assertz(commasymbol)).

print_detail(TransAsTerm,_Node1,Node2):-
    fdr_translate_event(TransAsTerm,TransAsString),
    (selectsymbol -> print(' [] '); (current_mode(fdr) -> assertz(selectsymbol) ; true)),
    print_single_transition(TransAsString,Node2).

print_end_of_construct :- current_mode(fdr),!,nl.

print_end_of_construct :- print(';'),nl.

print_open_detail(_NodeIDs) :- current_mode(fdr),!,print('prob__open__node -> STOP'),nl,
    assertz(prob__open__node_generated).

print_open_detail(NodeIDs) :- print_single_transition(prob__open__node,NodeIDs).

print_overall_header :- retractall(prob__open__node_generated),
    current_mode(fdr),!,
    print('-- ProB State Space Encoded for FDR in CSP'),nl,
    currently_opened_file(F),
    (animation_mode(cspm) -> (nl, print('include "'),"
    print(F),print('"'),nl,nl,"
    print('assert MAIN [FD= Nroot'),nl,
    print('assert Nroot [FD= MAIN'),nl,nl)
    ; (print('-- Original file: '), print(F))
    ),
    print('--'),nl.

print_overall_header :- print('/* ProB State Space Encoded for Spin in Promela */'),nl,
    currently_opened_file(F),
    print('/* Original file: '), print(F), print(' */'),nl.

print_process_declaration_footer(_) :- current_mode(fdr),!,nl.

print_process_declaration_footer(_) :- print(' fi;'),nl.

print_process_declaration_header(ID) :- current_mode(fdr),!,
    print('N'),print(ID), print(' = ').

print_process_declaration_header(ID) :-
    print('N'),print(ID), print(':'),nl,
    print(' if'),nl.

print_single_tau_transition(TransName,ToNodeID) :- current_mode(fdr),!,
    print(' {- '),print(TransName),print('->'), print(' -} N'),print(ToNodeID).

print_single_tau_transition(TransName,ToNodeID) :- !,print(' :: printf("'),"
    print(TransName),print('\\n") -> goto '), print('N'),print(ToNodeID)."

print_single_tau_transition(TransName,ToNodeID) :- print(' :: '),
    print(TransName),print('-> goto '), print('N'),print(ToNodeID).

print_single_transition(TransName,ToNodeID) :- current_mode(fdr),!,
    ((TransName = tick(_) ; TransName=tick)
    -> (print('SKIP {- N'),print(ToNodeID),print(' ( == STOP) -}'))
    ; ((TransName = i(_) ; TransName=i)
    -> (print('(STOP /\\ N'),print(ToNodeID), print(')') )
    ; (print(TransName),print('->'),print('N'),print(ToNodeID))
)
).

print_single_transition(TransName,ToNodeID) :- !,print(' :: printf("'),"
    print(TransName),print('\\n") -> goto '), print('N'),print(ToNodeID)."

print_single_transition(TransName,ToNodeID) :- print(' :: '),
    print(TransName),print('-> goto '), print('N'),print(ToNodeID).

print_stop_detail(_) :- current_mode(fdr),!,print('STOP'),nl.

print_stop_detail(NodeIDs) :- print_single_transition(prob__deadlock,NodeIDs).

print_tau_detail(Trans,Node2):-
    (selectsymbol -> print(' |~| '); (current_mode(fdr) -> assertz(selectsymbol) ; true)),
    print_single_tau_transition(Trans,Node2).

print_transition_footer :- current_mode(fdr),!,
    (prob__open__node_generated
    -> (print_channel_keyword, print('prob__open__node'),print_end_of_construct
    )
    ; true
    ),
    print('-- end of ProB Encoding'),nl.

print_transition_footer :- print('}'),nl, print('/* end of ProB Encoding */'),nl.

print_transition_header :- current_mode(fdr),!,nl.

print_transition_header :- nl, print('active proctype root()'),nl,print('{'),nl.

process_detail(Node1) :-
    retractall(tau_found), retractall(non_tau_found),
    %non_tau_transition_exists(Node1),!,
    process_non_tau_detail(Node1),!,
    (tau_found % tau_transition(Node1,_,_)
    -> ( print(' [> '), process_tau_instructions(Node1))
    ; true),
    nl.

process_detail(Node1) :- \+ non_tau_found,
    (tau_found % tau_transition(Node1,_,_)
    -> ( process_tau_instructions(Node1))
    ; print(' STOP ')
    ),
    nl.

process_non_tau_detail(Node1) :-
    transition_for_fdr(Node1,TransAsTerm,Node2),
    (is_tau(TransAsTerm) -> assert_tau_found_fail
    ; (non_tau_found -> true ; (print(' ( '),assertz(non_tau_found) ))),
    print_detail(TransAsTerm,Node1,Node2),nl,fail.

process_non_tau_detail(_) :- non_tau_found,
    (selectsymbol -> (print(' ) '),retract(selectsymbol)) ; print(' STOP ) ') ).

process_tau_instructions(Node1) :- print(' ( '),
    tau_transition(Node1,Trans,Node2),
    print_tau_detail(Trans,Node2),nl,fail.

process_tau_instructions(_) :- print(' ) ').

tau_transition(Node1,TransAsTerm,Node2) :-
    transition_for_fdr(Node1,TransAsTerm,Node2),is_tau(TransAsTerm).

tcltk_print_states_for_fdr(F) :-
    time(fdr_csp_generator:tcltk_print_states_for_fdr2(F)).

tcltk_print_states_for_fdr2(F) :-
    print_message('Saving State Space to FDR/CSP File: '), print_message(F),
    tell(F),(convert_b_2_csp -> true ; true),told,
    print_message('Finished').

tcltk_print_states_for_spin(F) :-
    print_message('Saving State Space to SPIN/Promela File: '), print_message(F),
    tell(F),(convert_b_2_promela -> true ; true),told,
    print_message('Finished').

to_be_ignored(io([_V1],print,_)). % comes from cspPrint

transition_for_fdr(FromID,Trans,ToID) :- transition(FromID,Trans,ToID),
    \+ to_be_ignored(Trans).

write_tran:-
    (animation_mode(cspm) -> print('-- ') ; true), /* Comment out if in CSP mode as original CSP will already define channels */
    print_channel_keyword,
    channel(_,ID,_,_),
    (written_channel(ID) -> true ; (
    assertz(written_channel(ID)),
    print_comma,
    print(ID))),
    fail.

write_tran:- print_end_of_construct,nl.