h_int

assign_channel_value(CID, Value, In, Out) :-
    number(CID),
    store(In, chan(CID,Value), global, Out),!.

assign_channel_value([], _, In, In).

assign_channel_value([H|Tail], Value, In, Out) :-
    store(In, chan(H,Value), global, In2),
    assign_channel_value(Tail,Value, In2, Out).

chan_length(empty,0).

chan_length([],0).

chan_length([[empty]|_],0).

chan_length([H|T],R) :-
    H \= [empty], chan_length(T,X), R is X+1.

check_jump(PC, NewPC) :-
    ( inst(PC,S), check_jump2(S, PC2)
    -> check_jump(PC2, NewPC)
    ; NewPC = PC ).

check_jump2(igoto(X), NewPC) :-
    ( number(X)
    -> NewPC is X
    ; inst(Y,label(X)), NewPC is Y ).

check_jump2(ibreak(X), NewPC) :-
    number(X),
    NewPC is X.

check_jump2(p_atomic(igoto(X)), NewPC) :-
    check_jump2(igoto(X), NewPC).

check_jump2(p_atomic(ibreak(X)), NewPC) :-
    check_jump2(ibreak(X), NewPC).

check_jump2(d_step(igoto(X)), NewPC) :-
    check_jump2(igoto(X), NewPC).

check_jump2(d_step(ibreak(X)), NewPC) :-
    check_jump2(ibreak(X), NewPC).

check_mode(normal, _).

check_mode(p_atomic, p_atomic(_)).

check_mode(d_step, d_step(_)).

check_type(Name,Type,Value,NewValue,In) :-
    ( check_type2(Type,Value,Value2,In)
    -> ( (Type == bool; Type == mtype)
    -> hone_value(Type,Value2,NewValue,In)
    ; NewValue = Value2 )
    ; print('Warning: Overflow of '),print(variable(Name,Type,Value)),
    hone_value(Type,Value,NewValue,In),
    print(', '),print(new_value(NewValue)),print('.'),nl ).

check_type2(bit, Value, NewValue, _) :-
    number(Value),
    NewValue is round(Value),
    (NewValue == 0; NewValue == 1),!.

check_type2(bool, Value, NewValue, _) :-
    number(Value),
    NewValue is round(Value),
    (NewValue == 0; NewValue == 1),!.

check_type2(byte, Value, NewValue, _) :-
    number(Value),
    NewValue is round(Value),
    NewValue >= 0,
    NewValue =< 255,!.

check_type2(pid, Value, NewValue, _) :-
    number(Value),
    NewValue is round(Value),
    NewValue >= 0,
    NewValue =< 255,!.

check_type2(short, Value, NewValue, _) :-
    number(Value),
    NewValue is round(Value),
    NewValue >= -32768,
    NewValue =< 32767,!.

check_type2(int, Value, NewValue, _) :-
    number(Value),
    NewValue is round(Value),
    NewValue >= -2147483648,
    NewValue =< 2147483647,!.

check_type2(mtype, Value, Value2, In) :-
    number(Value),
    Value2 is round(Value),
    lookup(var(mtype), global, In, MList),
    length(MList, N),
    Value2 >= 1,
    Value2 =< N,!.

check_type2(chan, Value, _, _) :-
    % what's the maximum chan_id?
    number(Value),
    print('chan typecheck. Use define(In var(chan(..)..) instead. chan_id: '),print(Value),nl.

consult_without_redefine_warning(File) :-
    current_prolog_flag(redefine_warnings, Old),
    set_prolog_flag(redefine_warnings, off),
    current_prolog_flag(single_var_warnings, Old2),
    set_prolog_flag(single_var_warnings2, off),
    (consult(File)
    -> OK=true ; OK=false),
    set_prolog_flag(redefine_warnings, Old),
    set_prolog_flag(single_var_warnings, Old2),
    OK=true.

define(env(Vars,Procs,Chans), var(Name,Value), PID, env(NewVars,Procs,Chans)) :-
    PID \= global,
    store2(Vars, key(Name,PID), Value, NewVars),!.

define(env(Vars,Procs,Chans), var(Name,Value), global, env(NewVars,Procs,Chans)) :-
    store2(Vars, Name, Value, NewVars).

delete([X|T],X,T).

delete([Y|T],X,[Y|DT]) :- delete(T,X,DT).

eval(cond(X,Y,Z), PID, In, R) :-
    eval(X, PID, In, X1),
    ( true(X1)
    -> eval(Y, PID, In, R)
    ; eval(Z, PID, In, R) ).

eval(or(X,Y), PID, In, R) :-
    eval(X, PID, In, R2),
    ( true(R2)
    -> R=R2
    ; eval(Y, PID, In, R) ).

eval(and(X,Y), PID, In, R) :-
    eval(X, PID, In, R2),
    ( true(R2)
    -> eval(Y, PID, In, R)
    ; R=R2 ).

eval(eq(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    ( X1==Y1
    -> R=1
    ; R=0 ).

eval(uneq(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    ( X1==Y1
    -> R=0
    ; R=1 ).

eval(lt(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    ( X1<Y1 -> R=1; R=0 ).

eval(gt(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    ( X1>Y1 -> R=1; R=0 ).

eval(leqt(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    ( X1=<Y1 -> R=1; R=0 ).

eval(geqt(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    ( X1>=Y1 -> R=1; R=0 ).

eval('+'(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1+Y1.

eval('-'(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1-Y1.

eval('*'(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1*Y1.

eval('/'(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1/Y1.

eval('mod'(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1 mod Y1.

eval(not(X), PID, In, R) :-
    eval(X, PID, In, X1),
    ( true(X1) -> R=0; R=1 ).

eval(compl(X), PID, In, R) :-
    eval(X, PID, In, X1),
    R is \ X1.

eval(bitor(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    R is X1 \/ Y1.

eval(bitxor(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    R is (X1 \/ Y1) /\ \(X1 /\ Y1).

eval(bitand(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    R is X1 /\ Y1.

eval(lshift(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    R is X1 << Y1.

eval(rshift(X,Y), PID, In, R) :-
    eval(X, PID, In, X1), eval(Y, PID, In, Y1),
    R is X1 >> Y1.

eval((expr(X)), PID, In, R) :-
    eval(X, PID, In, R),!.

eval(true, _, _, 1) :- !.

eval(false, _, _, 0) :- !.

eval(skip, _, _, 1) :- !.

eval(X, _, _, X) :-
    (number(X); X=[_|_]),!.

eval(ctype(X), _, In, R) :-
    lookup(var(mtype), global, In, Value),
    get_element(K, Value, X),
    length(Value, N),
    R is N - K.

eval(string(X), _, _, R) :-
    atom_codes(X,R).

eval(timeout, _, In, R) :-
    ( find_exec(In) -> R=0; R=1 ),!.

eval(pid, PID, _, PID) :- !.

eval(nr_pr, _, env(_,Procs,_), R) :-
    %length(Procs,R),!.
    avl_size(Procs,R),!.

eval(Name, PID, In, R) :-
    % looks up singles, chan(Name), array(Name,K), record(Name).
    (atomic(Name); Name=chan(_); Name=array(_,_); Name=record(_)),
    lookup(var(Name), PID, In, R2),
    eval(R2, PID, In, R).

eval(nfull(chan(Name)), PID, In, R) :-
    eval(empty(chan(Name)), PID, In, R). % fixed by leuschel

eval(empty(chan(Name)), PID, In, R) :-
    lookup(var(chan(Name)), PID, In, CID),
    lookup(chan(CID), global, In, Value),
    ( Value = [[empty]|_] -> R=1; R=0 ).

eval(full(chan(Name)), PID, In, R) :-
    eval(nempty(chan(Name)), PID, In, R).

eval(nempty(chan(Name)), PID, In, R) :-
    lookup(var(chan(Name)), PID, In, CID),
    lookup(chan(CID), global, In, Value),
    ( Value = [[empty]|_] -> R=0; R=1 ).

eval(len(chan(Name)), PID, In, R) :-
    lookup(var(chan(Name)), PID, In, CID),
    lookup(chan(CID), global, In, Value),
    chan_length(Value,R).

eval(expr_poll(Name,Msg), PID, In, R) :-
    ( trans3(poll(Name,Msg),PID,In,_) -> R=1; R=0 ).

eval(expr_random_poll(Name,Msg), PID, In, R) :-
    ( trans3(random_poll(Name,Msg),PID,In,_) -> R=1; R=0 ).

eval_list([], _, _, []).

eval_list([expr(H)|T], PID, In, [H2|T2]) :-
    eval(H, PID, In, H2),
    eval_list(T, PID, In, T2),!.

false(X) :-
    X==0.

find_exec(In) :-
    lookup(proc(active(PID,_)), global, In, PC),
    inst(PC,Statement),
    Statement \= expr(timeout),
    trans2(Statement, _, PC, _, PID, _, In, _).

find_exec(Alt, PID, In) :-
    member(A, Alt),
    inst(A,Statement),
    trans2(Statement, _, A, _, PID, _, In, _).

generate_chan(0,_,[]) :- !.

generate_chan(X,Msg,[Msg|R]) :- Y is X-1, generate_chan(Y,Msg,R).

generate_chanid(CID, In, Out) :-
    lookup(var(sys(chan_id)), global, In, CID),
    CID2 is CID+1,
    define(In, var(sys(chan_id),CID2), global, In2),
    store(In2, chan(CID,empty), global, Out),!.

generate_chanid_array(0, [], In, In) :- !.

generate_chanid_array(K, [CID|Tail], In, Out) :-
    generate_chanid(CID, In, In2),
    K2 is K-1,
    generate_chanid_array(K2, Tail, In2, Out).

generate_false(0,[]) :- !.

generate_false(X,[false|R]) :- Y is X-1, generate_false(Y,R).

generate_usertype(Type, N, ValueIn, ValueOut, In, Out) :-
    inst(_,typedef(Type,N,def(EType,EName))),
    get_init_value(def(EType,EName), Value, In, In2),
    append(ValueIn, [Value], ValueIn2),
    N2 is N+1,
    generate_usertype(Type, N2, ValueIn2, ValueOut ,In2, Out),!.

generate_usertype(_, _, Value, Value, In, In).

generate_usertype_array(0, _, [], In, In) :-!.

generate_usertype_array(K, Type, [Value|Tail], In, Out) :-
    generate_usertype(Type, 0, [], Value, In, In2),
    K2 is K-1,
    generate_usertype_array(K2, Type, Tail, In2, Out).

generate_zero(0,[]) :- !.

generate_zero(X,[0|R]) :- Y is X-1, generate_zero(Y,R).

get_element(R,List,E) :- get_element2(0,List,E,R).

get_element2(X,[E|_],E,X).

get_element2(X,[_|T],E,R) :- Y is X+1, get_element2(Y,T,E,R).

get_init_value(def(Type,array(Name,K)), Value, In, Out) :-
    ( Type=bool
    -> generate_false(K,Value), In=Out;
    Type=chan
    -> generate_chanid_array(K, Value, In, Out);
    (Type=bit; Type=byte;
    Type=pid; Type=short; Type=int;
    Type=unsigned; Type=mtype)
    -> generate_zero(K,Value), In=Out;
    %else: user-defined type
    generate_usertype_array(K, Type, Value, In, In2),
    define(In2, var(type(Name),Type), global, Out) ),!.

get_init_value(def(Type,Name), Value, In, Out) :-
    ( Type=bool
    -> Value=false, In=Out;
    Type=chan
    -> generate_chanid(Value, In, Out);
    (Type=bit; Type=byte;
    Type=pid; Type=short; Type=int;
    Type=unsigned; Type=mtype)
    -> Value=0, In=Out;
    %else: user-defined type
    generate_usertype(Type, 0, [], Value, In, In2),
    define(In2, var(type(Name),Type), global, Out) ).

get_record_element(Type, [array(EName,expr(K))], Value, PID, In, R) :-
    inst(_, typedef(Type,X,def(_,array(EName,_)))),
    get_element(X, Value, Value2),
    eval(K, PID, In, K2),
    get_element(K2, Value2, R),!.

get_record_element(Type, [EName], Value, _, _, R) :-
    inst(_, typedef(Type,X,def(_,EName))),
    get_element(X,Value,R),!.

get_record_element(Type, [array(EName,expr(K))|T], Value, PID, In, R) :-
    inst(_, typedef(Type,X,def(EType,array(EName,_)))),
    get_element(X, Value, Value2),
    eval(K, PID, In, K2),
    get_element(K2, Value2, V2),
    get_record_element(EType, T, V2, PID, In, R),!.

get_record_element(Type, [EName|T], Value, PID, In, R) :-
    inst(_, typedef(Type,X,def(EType,EName))),
    get_element(X, Value, V2),
    get_record_element(EType, T, V2, PID, In, R).

handle(def(Type,Name), In, Out) :-
    trans3(def(Type,Name), global, In, Out).

handle(typedef(_,_,_),In,In).

handle(assign(mtype,Value), In, Out) :-
    define(In, var(mtype,Value), global, Out),!.

handle(assign(Name,Value), In, Out) :-
    trans3(assign(Name,Value), global, In, Out).

handle(proctype(_,_,_), _, _) :- fail.

handle2(proctype(active(X),Proc,_), PC, In, Out) :-
    NewPC is PC+1,
    lookup(var(sys(pid)), global, In, PID),
    store(In, proc(active(PID,Proc),NewPC), global, In2),
    NewPID is PID+1,
    define(In2, var(sys(pid),NewPID), global, In3),
    (X =< 1
    -> In3=Out
    ; NewX is X-1,
    handle2(proctype(active(NewX),Proc,_), PC, In3, Out)
    ),!.

handle2(proctype(inactive,_,_), _, In, In).

handle2(init, PC, In, Out) :-
    NewPC is PC+1,
    lookup(var(sys(pid)), global, In, PID),
    store(In, proc(active(PID,init),NewPC), global, In2),
    NewPID is PID+1,
    define(In2, var(sys(pid),NewPID), global, Out).

handle2(_,_,In,In).

hone_value(bit, Value, NewValue, _) :-
    NewValue is Value mod 2,!.

hone_value(bool, Value, NewValue, _) :-
    Value2 is Value mod 2,
    ( false(Value2)
    -> NewValue = false
    ; NewValue = true ),!.

hone_value(byte, Value, NewValue, _) :-
    NewValue is Value mod 256,!.

hone_value(pid, Value, NewValue, _) :-
    NewValue is Value mod 256,!.

hone_value(short, Value, NewValue, _) :-
    ( Value > 32767
    -> Value2 is Value mod 32768,
    NewValue is Value2 - 32768 ),
    ( Value < -32768
    -> Value2 is Value mod 32769,
    NewValue is Value2 - 1 ),!.

hone_value(int, Value, NewValue, _) :-
    ( Value > 2147483647
    -> Value2 is Value mod 2147483648,
    NewValue is Value2 - 2147483648 ),
    ( Value < -2147483648
    -> Value2 is Value mod 2147483649,
    NewValue is Value2 - 1 ),!.

hone_value(mtype, Value, ctype(NewValue), In) :-
    lookup(var(mtype), global, In, MList),
    length(MList, N),
    Value2 is Value -1,
    Value3 is Value2 mod N,
    Value4 is Value3 + 1,
    K is N - Value4,
    get_element(K, MList, NewValue),!.

hone_value(chan, Value, Value, _).

init(PC, PC2, In, Out) :-
    inst(PC,S),
    %print(inst(PC,S)),nl,
    handle(S,In,In2),
    NewPC is PC+1,
    init(NewPC,PC2,In2,Out),!.

init(PC,PC,In,In).

init2(PC, In, Out) :-
    inst(PC,S),
    %print(inst(PC,S)),nl,
    handle2(S,PC,In,In2),
    NewPC is PC+1,
    init2(NewPC,In2,Out),!.

init2(_,In,In).

lookup(var(Name), PID, env(Vars,Procs,Chans), Value3) :-
    % set Name4
    %print(lookup(var(Name))),nl,
    ( Name = record([Name2|Tail]) -> true; Name2 = Name ),
    ( Name2 = array(Name3,expr(K)) -> true; Name3 = Name2 ),
    ( (PID \= global, lookup2(key(Name3,PID),Vars,_))
    -> Name4 = key(Name3,PID)
    ; Name4 = Name3 ),
    lookup2(Name4, Vars, Value),
    % get Value3
    ( Name2 = array(_,_)
    -> (eval(K,PID,env(Vars,Procs,Chans),K2), get_element(K2,Value,Value2))
    ; Value2 = Value ),
    ( Name = record(_)
    -> (lookup2(type(Name3),Vars,Type), get_record_element(Type,Tail,Value2,PID,env(Vars,_,_),Value3))
    ; Value3 = Value2 ).

lookup(proc(PID), global, env(_,Procs,_), PC) :-
    lookup3(PID, Procs, PC).

lookup(chan(Name), global, env(_,_,Chans), Value) :-
    lookup2(Name, Chans, Value).

lookup2(Key,AVL,Value) :-
    avl_fetch(Key,AVL,Value).

lookup3(Key,AVL,Value) :-
    avl_member(Key,AVL,Value).

n_send(CID, Name, Msg, Statement, PID, In, Out) :-
    lookup(chan(CID), global, In, Value),
    get_element(K, Value, [empty]), % Backtracking!
    %print(map_send(Msg)),nl,
    eval_list(Msg, PID, In, Msg2),
    %print(map2_send(Msg2)),nl,
    set_element(K, Value, Msg2, NewValue),
    store(In, chan(CID,NewValue), global, Out),
    Statement = send(Name,Msg),!.

open_promela_file(File) :-
    print(open_promela_file(File)),nl,
    consult_without_redefine_warning(File),
    retractall(current_promela_file_opened(_)),
    assertz(current_promela_file_opened(File)),
    print(new_xtl_file(File)),nl.

promela_property(env(Vars,_,_), '='('OrderedPair'(PID,Name),Value)) :- %var(key(Name,PID),Value)) :-
    lookup3(key(Name,PID), Vars, Value).

promela_property(env(Vars,_,_), var(Name,Value)) :-
    lookup3(Name, Vars, Value), Name \= key(_,_).

promela_property(env(_,Procs,_), proc(active(PID,Name),PC)) :-
    lookup3(active(PID,Name), Procs, PC).

promela_property(env(_,_,Chans), chan(Id,Value)) :-
    Chans \= [],
    lookup3(Id, Chans, Value).

promela_property(env(_,Procs,_), active_proctypes(N)) :-
    avl_size(Procs,N).

promela_property(env(Vars,_,_), unsafe) :-
    lookup2(sys(unsafe), Vars, Value),
    ( Value == true
    -> true
    ; fail ).

promela_transition(root, start_Promela, X) :- start(X).

promela_transition(S, L, S2) :- trans(L,S,S2).

r_send(CID, Name, Msg, Statement, PID, Span, In, Out) :-
    eval_list(Msg, PID, In, Msg2),
    %print(msg3(Msg2)),nl,
    store(In, chan(CID,[Msg2]), global, In2),
    % search matching receive
    lookup(proc(active(RPID,Proc)), global, In, PC),
    inst(PC, S),
    % S can be recv(), igoto(), ibreak(), etc.
    trans2(S,recv(RName,RMsg), PC, NewPC, RPID, Span, In2, In3),
    lookup(chan(CID), global, In3, [[empty]]),
    % reset channel
    store(In3, chan(CID,[]), global, In4),
    store(In4, proc(active(RPID,Proc), NewPC), global, Out),
    Statement = '.'(r_send(Name,Msg),r_recv(RName,RMsg)).

recv_eval([], _, In, In, []).

recv_eval([ctype(A)|T], PID, In, Out, [R|T2]) :-
    check_type(recv(ctype(A)),mtype,R,ctype(A),In),
    recv_eval(T, PID, In, Out, T2),!.

recv_eval([true|T], PID, In, Out, [R|T2]) :-
    check_type(recv(true),bool,R,true,In),
    recv_eval(T, PID, In, Out, T2),!.

recv_eval([false|T], PID, In, Out, [R|T2]) :-
    check_type(recv(false),bool,R,false,In),
    recv_eval(T, PID, In, Out, T2),!.

recv_eval([skip|T], PID, In, Out, [skip|T2]) :-
    recv_eval(T, PID, In, Out, T2),!.

recv_eval([chan(A)|T], PID, In, Out, [CID|T2]) :-
    define(In, var(chan(A),CID), PID, In2),
    recv_eval(T, PID, In2, Out, T2),!.

recv_eval([A|T], PID, In, Out, [A|T2]) :-
    number(A),
    recv_eval(T, PID, In, Out, T2),!.

recv_eval([underscore|T], PID, In, Out, [_|T2]) :-
    recv_eval(T, PID, In, Out, T2),!.

recv_eval([eval(Expr)|T], PID, In, Out, [R|T2]) :-
    eval(Expr, PID, In, R),
    %% print(evaluated_expr(Expr,R)),nl,
    recv_eval(T, PID, In, Out, T2),!.

recv_eval([vt(A,AType)|T], PID, In, Out, [R|T2]) :-
    atomic(A),
    store(In, var(A,AType,expr(R)), PID, In2),
    recv_eval(T, PID, In2, Out, T2).

remove(Key,AVL,NewAVL) :-
    avl_delete(Key, AVL, _, NewAVL).

remove_channels([], _, Chans, Chans).

remove_channels([ID|Tail], Vars, Chans, NewChans) :-
    number(ID),
    ( (lookup3(chan(_),Vars,ID); lookup3(key(chan(_),_),Vars,ID))
    -> Chans2=Chans
    ; remove(ID, Chans, Chans2) ),
    %print(remove_channel(ID)),nl,
    remove_channels(Tail, Vars, Chans2, NewChans).

remove_channels([[]|Tail], Vars, Chans, NewChans) :-
    remove_channels(Tail, Vars, Chans, NewChans).

remove_channels([[H|T]|Tail], Vars, Chans, NewChans) :-
    number(H),
    ( (lookup3(chan(_),Vars,H); lookup3(key(chan(_),_),Vars,H))
    -> Chans2=Chans
    ; remove(H, Chans, Chans2) ),
    %print(remove_channels(H)),nl,
    remove_channels([T|Tail], Vars, Chans2, NewChans).

remove_chans(PID, env(Vars,Procs,Chans), env(NewVars,Procs,NewChans)) :-
    findall(key(chan(Name),PID), lookup3(key(chan(Name),PID),Vars,_), List),
    remove_func(List,Vars,NewVars),
    findall(CID, lookup3(key(chan(_),PID),Vars,CID), List2),
    remove_channels(List2,NewVars,Chans,NewChans).

remove_children(PID2, env(Vars,Procs,Chans), env(NewVars,Procs,Chans)) :-
    findall(child(PID1, PID2), lookup3(child(PID1,PID2), Vars, true), List),
    remove_func(List,Vars,NewVars).

remove_element(0,[_|T1],T1).

remove_element(X,[H1|T1],[H1|T2]) :- Y is X-1, remove_element(Y,T1,T2).

remove_func([], Vars, Vars).

remove_func([H|T], Vars, NewVars) :-
    remove(H, Vars, Vars2),
    remove_func(T, Vars2, NewVars).

remove_proc(active(PID,Name), env(Vars,Procs,Chans), env(Vars,NewProcs,Chans)) :-
    remove(active(PID,Name), Procs, NewProcs).

remove_vars(PID, env(Vars,Procs,Chans), env(NewVars,Procs,Chans)) :-
    %findall(key(Name,PID), lookup2(key(Name,PID),Vars,_), List),
    findall(key(Name,PID), lookup3(key(Name,PID),Vars,_), List),
    remove_func(List,Vars,NewVars).

s_send(CID, Name, Msg, Statement, PID, In, Out) :-
    lookup(chan(CID), global, In, Value),
    get_element(K, Value, [empty]), % Backtracking!
    %print(map_send(Msg)),nl,
    eval_list(Msg, PID, In, Msg2),
    %print(map2_send(Msg2)),nl,
    set_element(K, Value, Msg2, NewValue),
    %print(newValue(NewValue)),nl,
    samsort(NewValue, SortedValue),
    %print(sortedValue(SortedValue)),nl,
    store(In, chan(CID,SortedValue), global, Out),
    Statement = sorted_send(Name,Msg),!.

set_all_elements([],_,[]).

set_all_elements([_|T1],E,[E|T2]) :-
    set_all_elements(T1,E,T2).

set_element(0,[_|T1],V,[V|T1]).

set_element(X,[H1|T1],V,[H1|T2]) :- Y is X-1, set_element(Y,T1,V,T2).

set_local_vars([], [], _, _, In, In).

set_local_vars([def(chan,H1)|T1], [expr(H2)|T2], PID, PID2, In, Out) :-
    lookup(var(H2), PID, In, Value),
    define(In, var(chan(H1),Value), PID2, In2),
    set_local_vars(T1, T2, PID, PID2, In2, Out),!.

set_local_vars([def(Type,H1)|T1], [expr(H2)|T2], PID, PID2, In, Out) :-
    eval(H2,PID,In,V),
    check_type(H1,Type,V,V2,In),
    define(In, var(H1,V2), PID2, In2),
    set_local_vars(T1, T2, PID, PID2, In2, Out).