promela_ncprinter

analyse_env(env(VarsA,_,_)) :-
    avl_member(Key, VarsA, Val),
    Key \= key(_,_), Key \= type(_), Key \= sys(_),
    Key \= child(_,_), Key \= chan(_),
    Val \= [_|_],
    print(Key),
    print(' == '),
    print_env_value(Val),
    print(' && '),
    fail.

analyse_env(_) :-
    print('true').

analyse_stat(assign(vt(Name,Type),Value), PID, In) :-
    In = env(Vars,_,_),
    % check if variable is global
    ( avl_fetch(key(Name,PID),Vars,_) -> fail; true ),
    print_name(Name,PID,In),
    print(' == '),
    print_value(Name,Type,Value,PID,In).

check_env(EnvA, NodeB) :-
    %print('('),
    analyse_env(EnvA),
    print(') -> goto N'),
    print(NodeB),
    print(';'),nl.

check_stat(_NodeA, EnvA, Trans, NodeB) :-
    print(' assert('),
    Trans = io([Statement], proc(PID,_Proc), _Span),
    analyse_stat(Statement, PID, EnvA),
    print(') -> goto N'),print(NodeB),print(';'),nl.

gen_process :-
    visited_expression(NodeA,EnvA),
    print_process_declaration_header(NodeA),
    %retractall(selectsymbol),
    (transition(NodeA,Trans,NodeB)
    -> (check_stat(NodeA,EnvA,Trans,NodeB)
    -> true
    ; check_env(EnvA,NodeB) )
    /*; (not_all_transitions_added(NodeIDs)
    -> print_open_detail(NodeIDs)
    ; print_stop_detail(NodeIDs))),*/
    ; print_end),
    print_process_declaration_footer(NodeA), fail.

gen_process :-
    print_transition_footer.

print_array(Name, expr(K), PID, In) :-
    h_int:eval(K,PID,In,R),
    print(Name),
    print('['),
    print(R),
    print(']').

print_end :-
    print(' do'),nl,
    print(' :: true'),nl,
    print(' od;'),nl.

print_env_value(V) :-
    number(V),
    print(V),!.

print_env_value(ctype(V)) :-
    print(V).

print_name(Name, PID, In) :-
    ( Name = record(Name2)
    -> print_record(Name2,PID,In)
    ; Name = array(Name2,K)
    -> print_array(Name2,K,PID,In)
    ; print(Name) ).

print_process_declaration_footer(_) :-
    true.

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

print_record([], _, _).

print_record([H|T], PID, In) :-
    print_name(H,PID,In),
    print('.'),
    print_record(T,PID,In).

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

print_transition_header(FileIn) :-
    print('#include "'),print(FileIn),print('"'),nl,nl,
    print('never {'),nl.

print_value(Name, Type, expr(V), PID, In) :-
    h_int:eval(V,PID,In,V1),
    %%print(nt(Name,Type,V1)),nl,
    h_int:check_type(Name,Type,V1,V2,In),
    ( V2 = ctype(V3) -> true; V3 = V2),
    print(V3).

promela_save_as_neverclaim(FileIn, FileOut) :-
    print_message('Saving State Space to never-claim file: '),
    print_message(FileOut),
    tell(FileOut),
    print_transition_header(FileIn),
    (gen_process -> true; true),
    told,
    print_message('Finished').