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').