cspm_trans(X,_,_,_) :- undefined_process_construct(X),
(get_preference(cspm_animate_all_processes,true),string_term_with_args(X) ->
add_message(cspm_trans,'Warning: Tried to expand a process with non-ground arguments: ',X),fail
;add_error_fail(csp_interpreter,'### Undefined Construct in cspm_trans !! ',X)
).
cspm_trans(stop(_),_,_,_) :- fail.
cspm_trans(omega,_,_,_) :- fail.
cspm_trans(skip(SrcSpan),tick(SrcSpan),omega,_).
cspm_trans('CHAOS'(SrcSpan,_Set),tau(chaos_stop(SrcSpan)),stop(SrcSpan),_).
cspm_trans('CHAOS'(SrcSpan,Set),io(V1,Ch,SrcSpan),'CHAOS'(SrcSpan,Set),_WF) :- /* or should we add an intermediate tau ?? */
% print(evaluate_argument(Set,S)),nl,
evaluate_argument(Set,S),
% print(chaos(S)),nl,
expand_channel_pattern_expression(S,ECList,SrcSpan),
% print(setup_channel_skeleton(io(V1,Ch,SrcSpan))),nl,
setup_channel_skeleton(io(V1,Ch,SrcSpan)),
% print(chaos(io(V1,Ch),ECList)),nl,
hidden(io(V1,Ch,SrcSpan),ECList).
cspm_trans('[]'(X,Y,Span),NA,Res,WF) :- cspm_trans(X,A,X1,WF),
shift_span_for_left_branch(Span,LSpan),
merge_span_into_event(A,LSpan,NA),
( top_level_dif(A,tau(_)), Res=X1
;
A=tau(_), tl_normalise('[]'(X1,Y,Span),Res) ).
cspm_trans('[]'(X,Y,Span),NA,Res,WF) :- cspm_trans(Y,A,Y1,WF),
shift_span_for_right_branch(Span,RSpan),
merge_span_into_event(A,RSpan,NA),
( top_level_dif(A,tau(_)), Res=Y1
;
A=tau(_), tl_normalise('[]'(X,Y1,Span),Res) ).
cspm_trans('|~|'(X,_Y,SrcSpan),tau(int_choice_left(SrcSpan,LSpan)),X,_WF) :-
shift_span_for_left_branch(SrcSpan,LSpan).
cspm_trans('|~|'(_X,Y,SrcSpan),tau(int_choice_right(SrcSpan,RSpan)),Y,_WF) :-
shift_span_for_right_branch(SrcSpan,RSpan).
cspm_trans(prefix(SPAN1,Values,ChannelExpr,CSP,SPAN2), io(EV,Channel,SPAN), NormCSP,WF) :-
evaluate_channel_outputs(Values,ChannelExpr,EV,Channel,SPAN,WF),
unify_spans(SPAN1,SPAN2,SPAN),
full_normalise_csp_process(CSP,NormCSP). % ,print(prefix(io(EV,Channel))),nl.
cspm_trans('|||'(omega,omega,Span),tick(Span),omega,_).
cspm_trans('|||'(X,Y,ISpan),A,Res,WF) :-
cspm_trans(X, ActionX, X1,WF),
shift_span_for_left_branch(ISpan,LSpan),
( ActionX=tick(_), X2=omega
; functor_dif(ActionX,tick), X2=X1
),
merge_span_into_event(ActionX,LSpan,MA),
(ActionX=tick(_) -> A=tau(MA); A=MA),
tl_normalise('|||'(X2,Y,ISpan),Res).
cspm_trans('|||'(X,Y,ISpan),A,Res,WF) :-
cspm_trans(Y, ActionY, Y1,WF),
shift_span_for_right_branch(ISpan,RSpan),
( ActionY=tick(_), Y2=omega
; functor_dif(ActionY,tick), Y2=Y1
),
merge_span_into_event(ActionY,RSpan,MA),
(ActionY=tick(_) -> A=tau(MA); A=MA),
tl_normalise('|||'(X,Y2,ISpan),Res).
cspm_trans(';'(P,Q,SeqSpan),AX,Res,WF) :-
cspm_trans(P,A,P1,WF),
( A=tick(_),
merge_span_into_event(A,SeqSpan,MA),
AX = tau(MA),
full_normalise_csp_process(Q,Res) /* is this required ?? */
; functor_dif(A,tick), AX=A,
tl_normalise(';'(P1,Q,SeqSpan),Res)
).
cspm_trans(sharing(CList,X,Y,SrcSpan),A,Res,WF) :-
evaluate_argument(CList,EvCList),
expand_channel_pattern_expression(EvCList,ECList,SrcSpan),
cspm_trans(esharing(ECList,X,Y,SrcSpan),A,Res,WF).
cspm_trans(esharing(_,omega,omega,SrcSpan), tick(SrcSpan), omega ,_WF).
cspm_trans(esharing(CList,X,Y,SrcSpan), Action, Result,WF) :-
cspm_trans(X, ActionX, X1,WF),
( (ActionX=tick(TS),
shift_span_for_left_branch(SrcSpan,LSpan),
merge_span_into_event(tau(tick(TS)),LSpan,Action),
Result = esharing(CList,omega,Y,SrcSpan))
; (functor_dif(ActionX,tick),
shift_span_for_left_branch(SrcSpan,LSpan),
merge_span_into_event(ActionX,LSpan,Action),
not_hidden(ActionX,CList), /* covers tau */
Result = esharing(CList,X1,Y,SrcSpan))
; (ActionX=io(V1,Ch,Sp1), Action = io(V,Ch,Span),
%((transferReq,[int(3),ac1,ac2,true])=(Ch,V1) -> trace ; true),
Result = esharing(CList,X1,Y1,SrcSpan),
unify_spans(Sp1,SrcSpan,SP1b),
hidden(Action,CList),
unify_values(V1,V2,V,Ch,SP1b), % try and also incorporate Sp2 Span, without compromising speed
% print(call_cspm_transY_B1(Y,io(V2,Ch),Y1)),nl,
cspm_trans(Y, io(V2,Ch,Sp2), Y1,WF), /* <---- Y will be recomputed for every solution of X !!! */
unify_spans(SP1b,Sp2,Span3),
Span = span_info(sharing,Span3)
)
).
cspm_trans(esharing(CList,X,Y,SrcSpan), Action2, Result,WF) :-
shift_span_for_right_branch(SrcSpan,RSpan),
% print(esharing_call_cspm_transY_B2(Y,ActionY,Y1)),nl,
cspm_trans(Y,ActionY,Y1,WF), /* this gets computed a second time; is there a way to avoid this? */
%print(esharing_cspm_transY_B2(Y,ActionY)),nl,
( ActionY = tick(TS), Action=tau(tick(TS)), Result=esharing(CList,X,omega,SrcSpan)
; functor_dif(ActionY,tick), ActionY = Action,
%print(try_non_sharing(ActionY)),nl,
not_hidden(ActionY,CList), /* covers tau */
Result = esharing(CList,X,Y1,SrcSpan)
),
merge_span_into_event(Action,RSpan,Action2).
cspm_trans(lParallel(LinkList,X,Y,Span), Action,Result,WF) :-
evaluate_link_list(LinkList,EvLinkRenameList),
%print(evlinklist(LinkList,EvLinkRenameList)),nl,
cspm_trans(elinkParallel(EvLinkRenameList,X,Y,Span),Action,Result,WF).
cspm_trans(elinkParallel(_,omega,omega,Span), tick(Span), omega ,_WF).
cspm_trans(elinkParallel(EvLinkRenameList,X,Y,LinkSpan),Action,Result,WF) :-
cspm_trans(X,AX,X2,WF), % print(elink_x(X,AX,X2,EvLinkRenameList)),nl, print('State: '),print(X),nl,
( AX = tick(TS),
shift_span_for_left_branch(LinkSpan,LSpan),
merge_span_into_event(tau(tick(TS)),LSpan,Action),
Result=elinkParallel(EvLinkRenameList,omega,Y,LinkSpan)
;
functor_dif(AX,tick),
( shift_span_for_left_branch(LinkSpan,LSpan),
merge_span_into_event(AX,LSpan,Action),
Result = elinkParallel(EvLinkRenameList,X2,Y,LinkSpan),
not_renamed(AX,EvLinkRenameList)
% ,print(not_renamed(AX,EvLinkRenameList)),nl
;
Action=tau(link(AX,io(V,Ch,Span))),
Result = elinkParallel(EvLinkRenameList,X2,Y2,LinkSpan),
force_rename_action(AX,EvLinkRenameList,io(V1,Ch,Sp0)),
unify_spans(LinkSpan,Sp0,Sp1),
%% print(renamed(AX,io(V1,Ch),EvLinkRenameList)),nl,
unify_values(V1,V2,V,Ch,Sp1), % try and also incorporate Sp2 Span, without compromising speed
% MAYBE TO DO ?: instantiate V2 as much as possible ! --> in()/dot issues
%% print(cspm_trans(Y,io(V2,Ch,Sp2),Y2)),nl,
cspm_trans(Y,io(V2,Ch,Sp2),Y2,WF), /* <---- Y will be recomputed for every solution of X !!! */
unify_spans(Sp1,Sp2,Span3),
%% print(unify(Sp1,Sp2,Span3)),nl,
Span = span_info(sharing,Span3)
)
).
cspm_trans(elinkParallel(EvLinkRenameList,X,Y,LinkSpan),Action2,
elinkParallel(EvLinkRenameList,X,YR,LinkSpan),WF) :-
shift_span_for_right_branch(LinkSpan,RSpan),
rev_rename_list(EvLinkRenameList,RevList),
cspm_trans(Y,ActionY,Y2,WF), /* TO DO: try and avoid recomputation of cspm_trans(Y) ?! */
( ActionY=tick(TS), Action=tau(tick(TS)), YR=omega
;
functor_dif(ActionY,tick),ActionY=Action,YR=Y2,not_renamed(Action,RevList)
),
merge_span_into_event(Action,RSpan,Action2).
cspm_trans(aParallel(CListX,X,CListY,Y,SrcSpan),A,NewState,WF) :- %print(expanding_aparx),nl,
evaluate_argument(CListX,EvCListX),
expand_channel_pattern_expression(EvCListX,ECListX,SrcSpan), %print(expanding_apary),nl,
evaluate_argument(CListY,EvCListY),
expand_channel_pattern_expression(EvCListY,ECListY,SrcSpan),
Expanded = eaParallel(ECListX,X,ECListY,Y,SrcSpan),
%we have expanded the channel synchronisation sets; avoid recomputing them every time
% TO DO: investigate whether it also makes sense to precompute intersection
cspm_trans(Expanded,A,NewState,WF).
cspm_trans(eaParallel(_,omega,_,omega,SrcSpan), tick(SrcSpan), omega ,_WF).
cspm_trans(eaParallel(ECListX,X,ECListY,Y,SrcSpan),A,eaParallel(ECListX,X2,ECListY,Y1,SrcSpan),WF) :-
%trans_pre_compute(Y,Results),
cspm_trans(X, AX, X1,WF),
% print(apar_x(AX, from(X))),nl,
( X2=X1,Y1=Y,
hidden_or_tau(AX,ECListX),
not_hidden(AX,ECListY),
shift_span_for_left_branch(SrcSpan,LSpan),
merge_span_into_event(AX,LSpan,A)
;
AX=tick(_TS), X2=omega,Y1=Y,
shift_span_for_left_branch(SrcSpan,LSpan),
merge_span_into_event(tau(AX),LSpan,A)
;
AX=io(V1,Ch,Sp1), X2=X1, A = io(V,Ch,Span),
% nl,print(try_apar_sync(V1,Ch)),nl,
hidden(io(V1,Ch,Sp1),ECListX), % print(left_ok),nl, % do V1 instead of V ?
hidden(io(V,Ch,Span),ECListY), % print(right_ok),nl, % V2 instead of V
% Synchronisation possible
unify_spans(Sp1,SrcSpan,SP1b),
unify_values(V1,V2,V,Ch,SP1b), % try and also incorporate Sp2 Span, without compromising speed
%print(trying(aparY(io(V2,Ch,Sp2)))),nl,
cspm_trans(Y, io(V2,Ch,Sp2), Y1,WF), /* <---- Y will be recomputed for every solution of X !!! */
% trans_cont(Results,Y, io(V2,Ch,Sp2), Y1),
% print(done(aparY(io(V2,Ch,Sp2)))),nl,
unify_spans(SP1b,Sp2,Span3),
Span = span_info(sharing,Span3)
).
cspm_trans(eaParallel(ECListX,X,ECListY,Y,SrcSpan),AS,eaParallel(ECListX,X,ECListY,Y2,SrcSpan),WF) :-
cspm_trans(Y, AY, Y1,WF), /* To do: try and avoid recomputation of cspm_trans(Y) ?! */
( AY=A, Y2=Y1,
hidden_or_tau(A,ECListY), not_hidden(A,ECListX)
;
AY=tick(_TS), A = tau(AY), Y2=omega
),
shift_span_for_right_branch(SrcSpan,RSpan),
merge_span_into_event(A,RSpan,AS).
cspm_trans(val_of(X,Span),A,NewExpr,WF) :- (symbol(RenamedX,X,_,_) -> cspm_trans(agent_call(Span,RenamedX,[]),A,NewExpr,WF);
cspm_trans(X,A,NewExpr,WF)).
cspm_trans(agent_call(Span,F,Par),NA,NNewExpr,WF) :-
unfold_function_call_once(F,Par,Value,Span),
cspm_trans(Value,A,NewExpr,WF),
full_normalise_csp_process(NewExpr,NNewExpr),
% print(merge_agcall(A,Span)),nl,
merge_span_into_event(A,Span,NA).
cspm_trans(agent_call_curry(F,Par),NA,NNewExpr,WF) :-
Span=no_loc_info_available,
unfold_function_call_curry_once(F,Par,Value,Span),
cspm_trans(Value,A,NewExpr,WF),
full_normalise_csp_process(NewExpr,NNewExpr),
% print(merge_agcall(A,Span)),nl,
merge_span_into_event(A,Span,NA).
cspm_trans(builtin_call(X),Action,NewExpr,WF) :- % builtin_call is normally removed by precompilation; but can remain, e.g., for assertions
cspm_trans(X,Action,NewExpr,WF).
cspm_trans(head(X),Action,NewExpr,WF) :- force_evaluate_argument(X,EX),head_list(EX,Result),
cspm_trans(Result,Action,NewExpr,WF).
cspm_trans('\\'(Expr,CList,Span), A, Res ,WF) :-
evaluate_argument(CList,EvCList),
expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available),
% print(ehide(Expr,ECList,Span)),nl,
cspm_trans(ehide(Expr,ECList,Span),A,Res,WF).
cspm_trans(ehide(Expr,CList,Span), A, Res ,WF) :-
% (nonvar(A) -> ((A=io(_,_,_);A=tick(_)) -> ActionX=A ; A=tau(hide(ActionX)))
% ; true),
cspm_trans(Expr,ActionX,X,WF),
cspm_hide_action(ActionX,X, CList,Span, A,Res).
cspm_trans(exception(CList,X,Y,Span), A, Res ,WF) :-
evaluate_argument(CList,EvCList),
expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available),
%print(exception(ECList,X,Y)),nl,
cspm_trans(eexception(ECList,X,Y,Span),A,Res,WF).
cspm_trans(eexception(CList,X,Y,Span),A,Res,WF) :- % expanded version of exception
cspm_trans(X, ActionX, X1,WF),
( functor_dif(ActionX,tick), ActionX=A,
Res = eexception(CList,X1,Y,Span),
not_hidden(A,CList)
; merge_span_into_event(ActionX,Span,A),
Res = Y,
hidden(ActionX,CList)
; A=tick(TS), ActionX=tick(TS), Res=omega % is this correct ??
).
cspm_trans('[>'(P,Q,SrcSpan),AS,Res,WF) :- cspm_trans(P,A,P1,WF),
( A=tau(_), Res='[>'(P1,Q,SrcSpan)
;
top_level_dif(A,tau(_)), % a transition which can be removed by the tau below
Res=P1 ),
shift_span_for_left_branch(SrcSpan,LSpan),
merge_span_into_event(A,LSpan,AS).
cspm_trans('[>'(_P,Q,SrcSpan),tau(timeout(SrcSpan)),Q,_WF).
cspm_trans('/\\'(X,Y,Span),NA,Res,WF) :-
cspm_trans(X,A,X1,WF), %%print(interrupt_left(X,A,X1)),nl,
shift_span_for_left_branch(Span,LSpan),
merge_span_into_event(A,LSpan,NA),
( A=tick(_), Res=X1
; functor_dif(A,tick), tl_normalise('/\\'(X1,Y,Span),Res)
).
cspm_trans('/\\'(X,Y,Span),NA,Res,WF) :-
cspm_trans(Y,A,Y1,WF),
shift_span_for_right_branch(Span,RSpan),
merge_span_into_event(A,RSpan,NA),
( top_level_dif(A,tau(_)), Res=Y1
; A=tau(_), tl_normalise('/\\'(X,Y1,Span),Res)
).
cspm_trans(procRenamingComp(X,GeneratorList,RenameList),RA,Res,WF) :-
% print(procCompRenaming(GeneratorList)),nl,
% warning: does not have the rangeEnum wrapper expected
expand_set_comprehension(rangeEnum(RenameList),GeneratorList,setValue(ExpandedRenames)),
%print(exp(ExpandedRenames)),nl,
cspm_trans(procRenaming(ExpandedRenames,X,no_loc_info_available),RA,Res,WF).
cspm_trans(procRenaming(RenameList,X,Span),RA,Res,WF) :- %print(procRename(RenameList)),nl,
evaluate_rename_list(RenameList,ERenameList),
cspm_trans(eprocRenaming(ERenameList,X,Span),RA,Res,WF).
cspm_trans(eprocRenaming(RenameList,X,Span),RAS,Res,WF) :-
%print('RENAME: '), translate:print_cspm_state(X),nl,
cspm_trans(X,A,X2,WF),
tl_normalise(eprocRenaming(RenameList,X2,Span),Res),
%print(try_rename(A,RenameList,RA,Span)),nl,
% it's still possible that A is non-ground term, i.e. there are a non-ground variables (c?x?y) in the sub-process,
% which have to be unified before applying renaming on them.
(ground(A) -> true; enumerate_action(A)),
rename_action(A,RenameList,RA),
%%% print(done_rename_action(A,RenameList,RA)),nl,
merge_span_into_event(RA,Span,RAS).
cspm_trans(ifte(Test,Then,Else,S1,S2,S3),A,X1,WF) :-
%nl,print(checking_if_test(Test,Then,Else)),nl,
evaluate_boolean_expression(Test,Res),
% print(if_evaluated_boolean_expression(Test,Res)),nl,nl,
cspm_if_trans(Res,Then,Else,A,X1,S1,S2,S3,WF).
cspm_trans('&'(Test,Then),A,X1,WF) :- S=no_loc_info_available,
cspm_trans(ifte(Test,Then,stop(S),S,S,S),A,X1,WF).
cspm_trans(repChoice(GeneratorList,Body,Span), Action,X1,WF) :-
%% nl,print(repChoice(GeneratorList,Body)),nl,
replicate_expand_set_comprehension([Body],GeneratorList,setValue(Bodies)),
%% print(bodies(Bodies)),nl,
convert_into_choice(Bodies,Span,CHOICE),
%% print(choice(CHOICE)),nl,
cspm_trans(CHOICE,Action,X1,WF).
cspm_trans(repInternalChoice(GeneratorList,Body,Span), tau(rep_int_choice(Span)),Res,_WF) :-
% print(repInternalChoice(GeneratorList,Span)),nl,
replicate_expand_set_comprehension([Body],GeneratorList,Bodies),
% print(bodies(Bodies)),nl,nl,
(is_empty_set(Bodies,true)
-> add_error(cspm_trans,'Empty set for replicated internal choice: ',Bodies,Span),fail
; is_member_set(Res,Bodies)).
cspm_trans(repInterleave(GeneratorList,Body,Span), A, X,WF) :-
%% tools:print_bt_message(repInterleave(GeneratorList)),
% multiplicity is relevant for |||, so add variables to Body below in case Variables are not used
extract_variables_from_generator_list(GeneratorList,Variables),
replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)),
convert_into_interleave(Bodies,Span,INTLV),
%% tools:print_bt_message(intlv(INTLV)),
cspm_trans(INTLV,A,X,WF). %, tools:print_bt_message(sol(A,X)).
cspm_trans(repSequence(GeneratorList,Body,Span),A,X,WF) :-
% print(repSequence(GeneratorList)),nl,
expand_listcomprehension(rangeEnum([Body]),GeneratorList,list(Bodies)),
% print(bodies(Bodies)),nl,
convert_into_seqcomp(Bodies,Span,SEQ), %print(sequential(SEQ)),nl,
cspm_trans(SEQ,A,X,WF).
cspm_trans(procRepAParallel(GeneratorList,pair(SyncSet,Body),Span), A, X,WF) :-
% multiplicity is relevant for sharing (it makes a difference if 1 or 2 copies are present), so add variables to Body below in case Variables are not used
extract_variables_from_generator_list(GeneratorList,Variables),
replicate_expand_set_comprehension([list([SyncSet,Body,Variables])],GeneratorList,setValue(Bodies)),
convert_into_eaParallel(Bodies,Span,APAR,_ALPH),
cspm_trans(APAR,A,X,WF).
cspm_trans(procRepLinkParallel(SyncSet,GeneratorList,Body,Span), A, X,WF) :-
expand_listcomprehension(rangeEnum([Body]),GeneratorList,list(Bodies)),
convert_into_linkParallel(Bodies,SyncSet,Span,APAR,Body),
%when((ground(APAR)),
cspm_trans(APAR,A,X,WF).
cspm_trans(procRepSharing(SyncSet,GeneratorList,Body,Span), A, X,WF) :-
% print(procRepSharing(GeneratorList)),nl,
% multiplicity is relevant for sharing, so add variables to Body below in case Variables are not used
extract_variables_from_generator_list(GeneratorList,Variables),
replicate_expand_set_comprehension([na_tuple([Body|Variables])],GeneratorList,setValue(Bodies)),
% print(bodies(Bodies)),nl,
convert_into_Sharing(Bodies,SyncSet,Span,APAR), %print(repshare(APAR)),nl,
cspm_trans(APAR,A,X,WF).