/* For inclusion by a Tvp program */ /* Depends on flag ID_PRED */ // ********************************************************************** // ********************************************************************** // FUNCTION DEFINITIONS // ********************************************************************** // ********************************************************************** // ********************************************************************** // Miscellaneous // ********************************************************************** %function Identity[](X) %t "Identity" { X } %function check[](X) %t "Check" { begin coerce(X); X end } // ********************************************************************** // Tests // ********************************************************************** %function IsVarNull[xx](X) %t xx + " == null ?" { begin focus( X,{ xx(v) }); let X = transform(X, precondition: !(E(v) xx(v)) ) in begin coerce(X); X end end } %function IsVarNotNull[xx](X) %t xx + " != null ?" { begin focus(X,{ xx(v) }); let X = transform(X, precondition: E(v) xx(v) ) in begin coerce(X); X end end } %function IsNextNull[xx,f](X) %t xx + "->" + f + " == null ?" { begin focus(X,{ E(v_1) xx(v_1) & f[out](v_1, v) }); let X = transform(X, precondition: ! E(v,v_1) xx(v_1) & f[out](v_1, v) ) in begin coerce(X); X end end } %function IsNextNotNull[xx,f](X) %t xx + "->" + f + " != null ?" { begin focus(X,{ E(v_1) xx(v_1) & f[out](v_1, v) }); let X = transform(X, precondition: E(v,v_1) xx(v_1) & f[out](v_1, v) ) in begin coerce(X); X end end } // ********************************************************************** // Setup // ********************************************************************** // ====================================================================== // One variable // ====================================================================== /* This function assumes that only var1 and [out] are correctly set, and copies [out] to [inp], and sets [ext] to 1/2. */ %function Setup_1[var1](X) %t "Setup_1(" + var1 + ")" { begin let Y = transform(X, update:{ foreach (zz in VarAllFPR - { var1 }){ zz(v) = 1/2 } foreach (b in Bools){ b[inp](v) = b[out](v) b[ext](v) = 1/2 } foreach (f in Fields){ f[inp](v_1,v_2) = f[out](v_1,v_2) f[ext](v_1,v_2) = 1/2 } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,out](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,out](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (zz in VarAllFPR - {var1}){ foreach (m in Mode){ foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = 1/2 } foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumFieldVar1){ p[f,inp,var1](v) = p[f,out,var1](v) p[f,ext,var1](v) = 1/2 } foreach (p in InstrumFieldVar2){ p[f,inp,var1](v_1,v_2) = p[f,out,var1](v_1,v_2) p[f,ext,var1](v_1,v_2) = 1/2 } } foreach (p in InstrumMode1){ p[inp](v) = p[out](v) p[ext](v) = 1/2 } foreach (p in InstrumMode2){ p[inp](v_1,v_2) = p[out](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (zz in VarAllFPR - {var1}){ foreach (m in Mode){ foreach (p in InstrumModeVar1){ p[m,zz](v) = 1/2 } foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumModeVar1){ p[inp,var1](v) = p[out,var1](v) p[ext,var1](v) = 1/2 } foreach (p in InstrumModeVar2){ p[inp,var1](v_1,v_2) = p[out,var1](v_1,v_2) p[ext,var1](v_1,v_2) = 1/2 } // Cross-instrumentation foreach (f in Fields){ foreach(p in #ifdef ID_PRED {id_pred,id_succ} #else {id_succ} #endif ){ p[f,inp,out](v) = 1 p[f,out,inp](v) = 1 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField1 - {id_pred,id_succ}){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin coerce(Y); Y end end } // ====================================================================== // Two variables // ====================================================================== /* This function assumes that only var1, var2 and [out] are correctly set, and copies [out] to [inp], and sets [ext] to 1/2. */ %function Setup_2[var1,var2](X) %t "Setup_2(" + var1 + ", " + var2 + ")" { begin let Y = transform(X, update:{ foreach (zz in VarAllFPR - { var1,var2 }){ zz(v) = 1/2 } foreach (b in Bools){ b[inp](v) = b[out](v) b[ext](v) = 1/2 } foreach (f in Fields){ f[inp](v_1,v_2) = f[out](v_1,v_2) f[ext](v_1,v_2) = 1/2 } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,out](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,out](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (zz in VarAllFPR - {var1,var2}){ foreach (m in Mode){ foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = 1/2 } foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumFieldVar1){ p[f,inp,var1](v) = p[f,out,var1](v) p[f,inp,var2](v) = p[f,out,var2](v) p[f,ext,var1](v) = 1/2 p[f,ext,var2](v) = 1/2 } foreach (p in InstrumFieldVar2){ p[f,inp,var1](v_1,v_2) = p[f,out,var1](v_1,v_2) p[f,inp,var2](v_1,v_2) = p[f,out,var2](v_1,v_2) p[f,ext,var1](v_1,v_2) = 1/2 p[f,ext,var2](v_1,v_2) = 1/2 } } foreach (p in InstrumMode1){ p[inp](v) = p[out](v) p[ext](v) = 1/2 } foreach (p in InstrumMode2){ p[inp](v_1,v_2) = p[out](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (zz in VarAllFPR - {var1,var2}){ foreach (m in Mode){ foreach (p in InstrumModeVar1){ p[m,zz](v) = 1/2 } foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumModeVar1){ p[inp,var1](v) = p[out,var1](v) p[inp,var2](v) = p[out,var2](v) p[ext,var1](v) = 1/2 p[ext,var2](v) = 1/2 } foreach (p in InstrumModeVar2){ p[inp,var1](v_1,v_2) = p[out,var1](v_1,v_2) p[inp,var2](v_1,v_2) = p[out,var2](v_1,v_2) p[ext,var1](v_1,v_2) = 1/2 p[ext,var2](v_1,v_2) = 1/2 } // Cross-instrumentation foreach (f in Fields){ foreach(p in #ifdef ID_PRED {id_pred,id_succ} #else {id_succ} #endif ){ p[f,inp,out](v) = 1 p[f,out,inp](v) = 1 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField1 - {id_pred,id_succ}){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin coerce(Y); Y end end } // ********************************************************************** // Procedure calls and returns // ********************************************************************** // ====================================================================== // Summarizing at the end of a procedure function // ====================================================================== // ---------------------------------------------------------------------- // Summarizing in case of one input and one output parameter // ---------------------------------------------------------------------- /* Summarizing a function with one input and one output parameter name = name of the function (for display only) actfp1 = formal parameter actfr1 = formal return parameter In the summary, we use the special variables "fp1" and "fr1" */ %function summary_1_1[name, actfp1, actfr1](X) %t "Summary of " + name + "(" + actfp1 + ") : " + actfr1 { begin let Y = transform(X, update:{ fp1(v) = actfp1(v) fr1(v) = actfr1(v) foreach (zz in VarAll){ zz(v)=1/2 } foreach (b in Bools){ b[inp](v) = 1/2 b[out](v) = b[inp](v) b[ext](v) = b[out](v) } foreach (f in Fields){ f[inp](v_1,v_2) = 1/2 f[out](v_1,v_2) = f[inp](v_1,v_2) f[ext](v_1,v_2) = f[out](v_1,v_2) } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = 1/2 p[f,out](v) = p[f,inp](v) p[f,ext](v) = p[f,out](v) } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = 1/2 p[f,out](v_1,v_2) = p[f,inp](v_1,v_2) p[f,ext](v_1,v_2) = p[f,out](v_1,v_2) } foreach (p in InstrumFieldVar1){ foreach (zz in VarAllFPR - {fp1,fr1}) { p[f,inp,zz](v) = 1/2 p[f,out,zz](v) = 1/2 p[f,ext,zz](v) = 1/2 } p[f,out,fp1](v) = p[f,inp,actfp1](v) p[f,out,fr1](v) = p[f,inp,actfr1](v) p[f,ext,fp1](v) = p[f,out,actfp1](v) p[f,ext,fr1](v) = p[f,out,actfr1](v) } foreach (p in InstrumFieldVar2){ foreach (zz in VarAllFPR - {fp1,fr1}) { p[f,inp,zz](v_1,v_2) = 1/2 p[f,out,zz](v_1,v_2) = 1/2 p[f,ext,zz](v_1,v_2) = 1/2 } p[f,out,fp1](v_1,v_2) = p[f,inp,actfp1](v_1,v_2) p[f,out,fr1](v_1,v_2) = p[f,inp,actfr1](v_1,v_2) p[f,ext,fp1](v_1,v_2) = p[f,out,actfp1](v_1,v_2) p[f,ext,fr1](v_1,v_2) = p[f,out,actfr1](v_1,v_2) } } foreach (p in InstrumMode1){ p[inp](v) = 1/2 p[out](v) = p[inp](v) p[ext](v) = p[out](v) } foreach(p in InstrumMode2){ p[inp](v_1,v_2) = 1/2 p[out](v_1,v_2) = p[inp](v_1,v_2) p[ext](v_1,v_2) = p[out](v_1,v_2) } foreach(p in InstrumModeVar1){ foreach (zz in VarAllFPR - {fp1,fr1}) { p[inp,zz](v) = 1/2 p[out,zz](v) = 1/2 p[ext,zz](v) = 1/2 } p[out,fp1](v) = p[inp,actfp1](v) p[out,fr1](v) = p[inp,actfr1](v) p[ext,fp1](v) = p[out,actfp1](v) p[ext,fr1](v) = p[out,actfr1](v) } foreach(p in InstrumModeVar2){ foreach (zz in VarAllFPR - {fp1,fr1}) { p[inp,zz](v_1,v_2) = 1/2 p[out,zz](v_1,v_2) = 1/2 p[ext,zz](v_1,v_2) = 1/2 } p[out,fp1](v_1,v_2) = p[inp,actfp1](v_1,v_2) p[out,fr1](v_1,v_2) = p[inp,actfr1](v_1,v_2) p[ext,fp1](v_1,v_2) = p[out,actfp1](v_1,v_2) p[ext,fr1](v_1,v_2) = p[out,actfr1](v_1,v_2) } // Cross-instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = p[f,inp,out](v) p[f,ext,out](v) = p[f,out,inp](v) } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = p[f,inp,out](v_1,v_2) p[f,ext,out](v_1,v_2) = p[f,out,inp](v_1,v_2) } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = p[inp,out](v) p[ext,out](v) = p[out,inp](v) } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = p[inp,out](v_1,v_2) p[ext,out](v_1,v_2) = p[out,inp](v_1,v_2) } }) in begin blur(Y); Y end end } // ---------------------------------------------------------------------- // Summarizing in case of one input and two output parameters // ---------------------------------------------------------------------- /* Summarizing a function with one input and one output parameter name = name of the function (for display only) actfp1 = formal parameter actfr1 = formal return parameter actfr2 = formal return parameter In the summary, we use the special variables "fp1" and "fr1" and "fr2" */ %function summary_1_2[name, actfp1, actfr1, actfr2](X) %t "Summary of " + name + "(" + actfp1 + ") : (" + actfr1 + ", " + actfr2 + ")" { begin let Y = transform(X, update:{ fp1(v) = actfp1(v) fr1(v) = actfr1(v) fr2(v) = actfr2(v) foreach (zz in VarAll){ zz(v)=1/2 } foreach (b in Bools){ b[inp](v) = 1/2 b[out](v) = b[inp](v) b[ext](v) = b[out](v) } foreach (f in Fields){ f[inp](v_1,v_2) = 1/2 f[out](v_1,v_2) = f[inp](v_1,v_2) f[ext](v_1,v_2) = f[out](v_1,v_2) } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = 1/2 p[f,out](v) = p[f,inp](v) p[f,ext](v) = p[f,out](v) } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = 1/2 p[f,out](v_1,v_2) = p[f,inp](v_1,v_2) p[f,ext](v_1,v_2) = p[f,out](v_1,v_2) } foreach (p in InstrumFieldVar1){ foreach (zz in VarAllFPR - {fp1,fr1,fr2}){ p[f,inp,zz](v) = 1/2 p[f,out,zz](v) = 1/2 p[f,ext,zz](v) = 1/2 } p[f,out,fp1](v) = p[f,inp,actfp1](v) p[f,out,fr1](v) = p[f,inp,actfr1](v) p[f,out,fr2](v) = p[f,inp,actfr2](v) p[f,ext,fp1](v) = p[f,out,actfp1](v) p[f,ext,fr1](v) = p[f,out,actfr1](v) p[f,ext,fr2](v) = p[f,out,actfr2](v) } foreach (p in InstrumFieldVar2){ foreach (zz in VarAllFPR - {fp1,fr1,fr2}){ p[f,inp,zz](v_1,v_2) = 1/2 p[f,out,zz](v_1,v_2) = 1/2 p[f,ext,zz](v_1,v_2) = 1/2 } p[f,out,fp1](v_1,v_2) = p[f,inp,actfp1](v_1,v_2) p[f,out,fr1](v_1,v_2) = p[f,inp,actfr1](v_1,v_2) p[f,out,fr2](v_1,v_2) = p[f,inp,actfr2](v_1,v_2) p[f,ext,fp1](v_1,v_2) = p[f,out,actfp1](v_1,v_2) p[f,ext,fr1](v_1,v_2) = p[f,out,actfr1](v_1,v_2) p[f,ext,fr2](v_1,v_2) = p[f,out,actfr2](v_1,v_2) } } foreach (p in InstrumMode1){ p[inp](v) = 1/2 p[out](v) = p[inp](v) p[ext](v) = p[out](v) } foreach(p in InstrumMode2){ p[inp](v_1,v_2) = 1/2 p[out](v_1,v_2) = p[inp](v_1,v_2) p[ext](v_1,v_2) = p[out](v_1,v_2) } foreach(p in InstrumModeVar1){ foreach (zz in VarAllFPR - {fp1,fr1,fr2}){ p[inp,zz](v) = 1/2 p[out,zz](v) = 1/2 p[ext,zz](v) = 1/2 } p[out,fp1](v) = p[inp,actfp1](v) p[out,fr1](v) = p[inp,actfr1](v) p[out,fr2](v) = p[inp,actfr2](v) p[ext,fp1](v) = p[out,actfp1](v) p[ext,fr1](v) = p[out,actfr1](v) p[ext,fr2](v) = p[out,actfr2](v) } foreach(p in InstrumModeVar2){ foreach (zz in VarAllFPR - {fp1,fr1,fr2}){ p[inp,zz](v_1,v_2) = 1/2 p[out,zz](v_1,v_2) = 1/2 p[ext,zz](v_1,v_2) = 1/2 } p[out,fp1](v_1,v_2) = p[inp,actfp1](v_1,v_2) p[out,fr1](v_1,v_2) = p[inp,actfr1](v_1,v_2) p[out,fr2](v_1,v_2) = p[inp,actfr2](v_1,v_2) p[ext,fp1](v_1,v_2) = p[out,actfp1](v_1,v_2) p[ext,fr1](v_1,v_2) = p[out,actfr1](v_1,v_2) p[ext,fr2](v_1,v_2) = p[out,actfr2](v_1,v_2) } // Cross-instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = p[f,inp,out](v) p[f,ext,out](v) = p[f,out,inp](v) } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = p[f,inp,out](v_1,v_2) p[f,ext,out](v_1,v_2) = p[f,out,inp](v_1,v_2) } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = p[inp,out](v) p[ext,out](v) = p[out,inp](v) } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = p[inp,out](v_1,v_2) p[ext,out](v_1,v_2) = p[out,inp](v_1,v_2) } }) in begin blur(Y); Y end end } // ---------------------------------------------------------------------- // Summarizing in case of one input and zero output parameter // ---------------------------------------------------------------------- /* Summarizing a function with one input and zero output parameter name = name of the function (for display only) actfp1 = formal parameter In the summary, we use the special variables "fp1" */ %function summary_1_0[name, actfp1](X) %t "Summary of " + name + "(" + actfp1 + ") : ()" { begin let Y = transform(X, update:{ fp1(v) = actfp1(v) foreach (zz in VarAll){ zz(v)=1/2 } foreach (b in Bools){ b[inp](v) = 1/2 b[out](v) = b[inp](v) b[ext](v) = b[out](v) } foreach (f in Fields){ f[inp](v_1,v_2) = 1/2 f[out](v_1,v_2) = f[inp](v_1,v_2) f[ext](v_1,v_2) = f[out](v_1,v_2) } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = 1/2 p[f,out](v) = p[f,inp](v) p[f,ext](v) = p[f,out](v) } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = 1/2 p[f,out](v_1,v_2) = p[f,inp](v_1,v_2) p[f,ext](v_1,v_2) = p[f,out](v_1,v_2) } foreach (p in InstrumFieldVar1){ foreach (zz in VarAllFPR - {fp1}) { p[f,inp,zz](v) = 1/2 p[f,out,zz](v) = 1/2 p[f,ext,zz](v) = 1/2 } p[f,out,fp1](v) = p[f,inp,actfp1](v) p[f,ext,fp1](v) = p[f,out,actfp1](v) } foreach (p in InstrumFieldVar2){ foreach (zz in VarAllFPR - {fp1}) { p[f,inp,zz](v_1,v_2) = 1/2 p[f,out,zz](v_1,v_2) = 1/2 p[f,ext,zz](v_1,v_2) = 1/2 } p[f,out,fp1](v_1,v_2) = p[f,inp,actfp1](v_1,v_2) p[f,ext,fp1](v_1,v_2) = p[f,out,actfp1](v_1,v_2) } } foreach (p in InstrumMode1){ p[inp](v) = 1/2 p[out](v) = p[inp](v) p[ext](v) = p[out](v) } foreach(p in InstrumMode2){ p[inp](v_1,v_2) = 1/2 p[out](v_1,v_2) = p[inp](v_1,v_2) p[ext](v_1,v_2) = p[out](v_1,v_2) } foreach(p in InstrumModeVar1){ foreach (zz in VarAllFPR - {fp1}) { p[inp,zz](v) = 1/2 p[out,zz](v) = 1/2 p[ext,zz](v) = 1/2 } p[out,fp1](v) = p[inp,actfp1](v) p[ext,fp1](v) = p[out,actfp1](v) } foreach(p in InstrumModeVar2){ foreach (zz in VarAllFPR - {fp1}) { p[inp,zz](v_1,v_2) = 1/2 p[out,zz](v_1,v_2) = 1/2 p[ext,zz](v_1,v_2) = 1/2 } p[out,fp1](v_1,v_2) = p[inp,actfp1](v_1,v_2) p[ext,fp1](v_1,v_2) = p[out,actfp1](v_1,v_2) } // Cross-instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = p[f,inp,out](v) p[f,ext,out](v) = p[f,out,inp](v) } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = p[f,inp,out](v_1,v_2) p[f,ext,out](v_1,v_2) = p[f,out,inp](v_1,v_2) } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = p[inp,out](v) p[ext,out](v) = p[out,inp](v) } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = p[inp,out](v_1,v_2) p[ext,out](v_1,v_2) = p[out,inp](v_1,v_2) } }) in begin blur(Y); Y end end } // ---------------------------------------------------------------------- // Summarizing in case of two input and one output parameters // ---------------------------------------------------------------------- /* Summarizing a function with two input and one output parameter name = name of the function (for display only) actfp1,actfp2 = formal parameter actfr1 = formal return parameter In the summary, we use the special variables "fp1", "fp2" and "fr1" */ %function summary_2_1[name, actfp1, actfp2, actfr1](X) %t "Summary of " + name + "(" + actfp1 + ", " + actfp2+ ") : " + actfr1 { begin let Y = transform(X, update:{ fp1(v) = actfp1(v) fp2(v) = actfp2(v) fr1(v) = actfr1(v) foreach (zz in VarAll){ zz(v)=1/2 } foreach (b in Bools){ b[inp](v) = 1/2 b[out](v) = b[inp](v) b[ext](v) = b[out](v) } foreach (f in Fields){ f[inp](v_1,v_2) = 1/2 f[out](v_1,v_2) = f[inp](v_1,v_2) f[ext](v_1,v_2) = f[out](v_1,v_2) } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = 1/2 p[f,out](v) = p[f,inp](v) p[f,ext](v) = p[f,out](v) } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = 1/2 p[f,out](v_1,v_2) = p[f,inp](v_1,v_2) p[f,ext](v_1,v_2) = p[f,out](v_1,v_2) } foreach (p in InstrumFieldVar1){ foreach (zz in VarAllFPR - {fp1,fp2,fr1}) { p[f,inp,zz](v) = 1/2 p[f,out,zz](v) = 1/2 p[f,ext,zz](v) = 1/2 } p[f,out,fp1](v) = p[f,inp,actfp1](v) p[f,out,fp2](v) = p[f,inp,actfp2](v) p[f,out,fr1](v) = p[f,inp,actfr1](v) p[f,ext,fp1](v) = p[f,out,actfp1](v) p[f,ext,fp2](v) = p[f,out,actfp2](v) p[f,ext,fr1](v) = p[f,out,actfr1](v) } foreach (p in InstrumFieldVar2){ foreach (zz in VarAllFPR - {fp1,fp2,fr1}) { p[f,inp,zz](v_1,v_2) = 1/2 p[f,out,zz](v_1,v_2) = 1/2 p[f,ext,zz](v_1,v_2) = 1/2 } p[f,out,fp1](v_1,v_2) = p[f,inp,actfp1](v_1,v_2) p[f,out,fp2](v_1,v_2) = p[f,inp,actfp2](v_1,v_2) p[f,out,fr1](v_1,v_2) = p[f,inp,actfr1](v_1,v_2) p[f,ext,fp1](v_1,v_2) = p[f,out,actfp1](v_1,v_2) p[f,ext,fp2](v_1,v_2) = p[f,out,actfp2](v_1,v_2) p[f,ext,fr1](v_1,v_2) = p[f,out,actfr1](v_1,v_2) } } foreach (p in InstrumMode1){ p[inp](v) = 1/2 p[out](v) = p[inp](v) p[ext](v) = p[out](v) } foreach(p in InstrumMode2){ p[inp](v_1,v_2) = 1/2 p[out](v_1,v_2) = p[inp](v_1,v_2) p[ext](v_1,v_2) = p[out](v_1,v_2) } foreach(p in InstrumModeVar1){ foreach (zz in VarAllFPR - {fp1,fp2,fr1}) { p[inp,zz](v) = 1/2 p[out,zz](v) = 1/2 p[ext,zz](v) = 1/2 } p[out,fp1](v) = p[inp,actfp1](v) p[out,fp2](v) = p[inp,actfp2](v) p[out,fr1](v) = p[inp,actfr1](v) p[ext,fp1](v) = p[out,actfp1](v) p[ext,fp2](v) = p[out,actfp2](v) p[ext,fr1](v) = p[out,actfr1](v) } foreach(p in InstrumModeVar2){ foreach (zz in VarAllFPR - {fp1,fp2,fr1}) { p[inp,zz](v_1,v_2) = 1/2 p[out,zz](v_1,v_2) = 1/2 p[ext,zz](v_1,v_2) = 1/2 } p[out,fp1](v_1,v_2) = p[inp,actfp1](v_1,v_2) p[out,fp2](v_1,v_2) = p[inp,actfp2](v_1,v_2) p[out,fr1](v_1,v_2) = p[inp,actfr1](v_1,v_2) p[ext,fp1](v_1,v_2) = p[out,actfp1](v_1,v_2) p[ext,fp2](v_1,v_2) = p[out,actfp2](v_1,v_2) p[ext,fr1](v_1,v_2) = p[out,actfr1](v_1,v_2) } // Cross-instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = p[f,inp,out](v) p[f,ext,out](v) = p[f,out,inp](v) } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = p[f,inp,out](v_1,v_2) p[f,ext,out](v_1,v_2) = p[f,out,inp](v_1,v_2) } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = p[inp,out](v) p[ext,out](v) = p[out,inp](v) } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = p[inp,out](v_1,v_2) p[ext,out](v_1,v_2) = p[out,inp](v_1,v_2) } }) in begin blur(Y); Y end end } // ---------------------------------------------------------------------- // Summarizing in case of two input and two output parameters // ---------------------------------------------------------------------- /* Summarizing a function with two input and one output parameter name = name of the function (for display only) actfp1,actfp2 = formal parameter actfr1,actfr2 = formal return parameter In the summary, we use the special variables "fp1", "fp2" and "fr1" and "fr2" */ %function summary_2_2[name, actfp1, actfp2, actfr1, actfr2](X) %t "Summary of " + name + "(" + actfp1 + ", " + actfp2 + ") : (" + actfr1 + ", " + actfr2 + ")" { begin let Y = transform(X, update:{ fp1(v) = actfp1(v) fp2(v) = actfp2(v) fr1(v) = actfr1(v) fr2(v) = actfr2(v) foreach (zz in VarAll){ zz(v)=1/2 } foreach (b in Bools){ b[inp](v) = 1/2 b[out](v) = b[inp](v) b[ext](v) = b[out](v) } foreach (f in Fields){ f[inp](v_1,v_2) = 1/2 f[out](v_1,v_2) = f[inp](v_1,v_2) f[ext](v_1,v_2) = f[out](v_1,v_2) } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = 1/2 p[f,out](v) = p[f,inp](v) p[f,ext](v) = p[f,out](v) } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = 1/2 p[f,out](v_1,v_2) = p[f,inp](v_1,v_2) p[f,ext](v_1,v_2) = p[f,out](v_1,v_2) } foreach (p in InstrumFieldVar1){ foreach (zz in VarAllFPR - {fp1,fp2,fr1,fr2}) { p[f,inp,zz](v) = 1/2 p[f,out,zz](v) = 1/2 p[f,ext,zz](v) = 1/2 } p[f,out,fp1](v) = p[f,inp,actfp1](v) p[f,out,fp2](v) = p[f,inp,actfp2](v) p[f,out,fr1](v) = p[f,inp,actfr1](v) p[f,out,fr2](v) = p[f,inp,actfr2](v) p[f,ext,fp1](v) = p[f,out,actfp1](v) p[f,ext,fp2](v) = p[f,out,actfp2](v) p[f,ext,fr1](v) = p[f,out,actfr1](v) p[f,ext,fr2](v) = p[f,out,actfr2](v) } foreach (p in InstrumFieldVar2){ foreach (zz in VarAllFPR - {fp1,fp2,fr1,fr2}) { p[f,inp,zz](v_1,v_2) = 1/2 p[f,out,zz](v_1,v_2) = 1/2 p[f,ext,zz](v_1,v_2) = 1/2 } p[f,out,fp1](v_1,v_2) = p[f,inp,actfp1](v_1,v_2) p[f,out,fp2](v_1,v_2) = p[f,inp,actfp2](v_1,v_2) p[f,out,fr1](v_1,v_2) = p[f,inp,actfr1](v_1,v_2) p[f,out,fr2](v_1,v_2) = p[f,inp,actfr2](v_1,v_2) p[f,ext,fp1](v_1,v_2) = p[f,out,actfp1](v_1,v_2) p[f,ext,fp2](v_1,v_2) = p[f,out,actfp2](v_1,v_2) p[f,ext,fr1](v_1,v_2) = p[f,out,actfr1](v_1,v_2) p[f,ext,fr2](v_1,v_2) = p[f,out,actfr2](v_1,v_2) } } foreach (p in InstrumMode1){ p[inp](v) = 1/2 p[out](v) = p[inp](v) p[ext](v) = p[out](v) } foreach(p in InstrumMode2){ p[inp](v_1,v_2) = 1/2 p[out](v_1,v_2) = p[inp](v_1,v_2) p[ext](v_1,v_2) = p[out](v_1,v_2) } foreach(p in InstrumModeVar1){ foreach (zz in VarAllFPR - {fp1,fp2,fr1,fr2}) { p[inp,zz](v) = 1/2 p[out,zz](v) = 1/2 p[ext,zz](v) = 1/2 } p[out,fp1](v) = p[inp,actfp1](v) p[out,fp2](v) = p[inp,actfp2](v) p[out,fr1](v) = p[inp,actfr1](v) p[out,fr2](v) = p[inp,actfr2](v) p[ext,fp1](v) = p[out,actfp1](v) p[ext,fp2](v) = p[out,actfp2](v) p[ext,fr1](v) = p[out,actfr1](v) p[ext,fr2](v) = p[out,actfr2](v) } foreach(p in InstrumModeVar2){ foreach (zz in VarAllFPR - {fp1,fp2,fr1,fr2}) { p[inp,zz](v_1,v_2) = 1/2 p[out,zz](v_1,v_2) = 1/2 p[ext,zz](v_1,v_2) = 1/2 } p[out,fp1](v_1,v_2) = p[inp,actfp1](v_1,v_2) p[out,fp2](v_1,v_2) = p[inp,actfp2](v_1,v_2) p[out,fr1](v_1,v_2) = p[inp,actfr1](v_1,v_2) p[out,fr2](v_1,v_2) = p[inp,actfr2](v_1,v_2) p[ext,fp1](v_1,v_2) = p[out,actfp1](v_1,v_2) p[ext,fp2](v_1,v_2) = p[out,actfp2](v_1,v_2) p[ext,fr1](v_1,v_2) = p[out,actfr1](v_1,v_2) p[ext,fr2](v_1,v_2) = p[out,actfr2](v_1,v_2) } // Cross-instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = p[f,inp,out](v) p[f,ext,out](v) = p[f,out,inp](v) } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = p[f,inp,out](v_1,v_2) p[f,ext,out](v_1,v_2) = p[f,out,inp](v_1,v_2) } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = p[inp,out](v) p[ext,out](v) = p[out,inp](v) } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = p[inp,out](v_1,v_2) p[ext,out](v_1,v_2) = p[out,inp](v_1,v_2) } }) in begin blur(Y); Y end end } // ====================================================================== // Calls // ====================================================================== /* Here we map the relevant part of the environment of the caller to the input (and standard) environment of the callee. */ // ---------------------------------------------------------------------- // Call in case of one input parameter // ---------------------------------------------------------------------- /* name = name of the function (for display only) act1 = actual parameter actfp1 = formal parameter */ %function call_X_1[name, act1, actfp1](X) %t "Call_X_1 " + name + "(" + act1 + ")" { begin let Y = transform(X, update:{ // Binding formal to actual actfp1(v) = act1(v) // Forgetting all from the caller foreach (zz in VarAllFPR - { actfp1 }){ zz(v) = 1/2 } // Copying [out] to [inp] (+ special stuff for fp1(v)=act1(v)) foreach (b in Bools){ b[inp](v) = b[out](v) b[ext](v) = 1/2 } foreach (f in Fields){ f[inp](v_1,v_2) = f[out](v_1,v_2) f[ext](v_1,v_2) = 1/2 } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,out](v) p[f,out](v) = p[f,out](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,out](v_1,v_2) p[f,out](v_1,v_2) = p[f,out](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (p in InstrumFieldVar1){ p[f,inp,actfp1](v) = p[f,out,act1](v) p[f,out,actfp1](v) = p[f,out,act1](v) p[f,ext,actfp1](v) = 1/2 foreach(zz in VarAllFPR-{actfp1}){ p[f,inp,zz](v) = 1/2 p[f,out,zz](v) = 1/2 p[f,ext,zz](v) = 1/2 } } foreach (p in InstrumFieldVar2){ p[f,inp,actfp1](v_1,v_2) = p[f,out,act1](v_1,v_2) p[f,out,actfp1](v_1,v_2) = p[f,out,act1](v_1,v_2) p[f,ext,actfp1](v_1,v_2) = 1/2 foreach(zz in VarAllFPR-{actfp1}){ p[f,inp,zz](v_1,v_2) = 1/2 p[f,out,zz](v_1,v_2) = 1/2 p[f,ext,zz](v_1,v_2) = 1/2 } } } foreach(p in InstrumMode1){ p[inp](v) = p[out](v) p[out](v) = p[out](v) p[ext](v) = 1/2 } foreach(p in InstrumMode2){ p[inp](v_1,v_2) = p[out](v_1,v_2) p[out](v_1,v_2) = p[out](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (p in InstrumModeVar1){ p[inp,actfp1](v) = p[out,act1](v) p[out,actfp1](v) = p[out,act1](v) p[ext,actfp1](v) = 1/2 foreach(zz in VarAllFPR-{actfp1}){ p[inp,zz](v) = 1/2 p[out,zz](v) = 1/2 p[ext,zz](v) = 1/2 } } foreach (p in InstrumModeVar2){ p[inp,actfp1](v_1,v_2) = p[out,act1](v_1,v_2) p[out,actfp1](v_1,v_2) = p[out,act1](v_1,v_2) p[ext,actfp1](v_1,v_2) = 1/2 foreach(zz in VarAllFPR-{actfp1}){ p[inp,zz](v_1,v_2) = 1/2 p[out,zz](v_1,v_2) = 1/2 p[ext,zz](v_1,v_2) = 1/2 } } // Cross Instrumentation foreach (f in Fields){ foreach(p in #ifdef ID_PRED {id_pred,id_succ} #else {id_succ} #endif ) { p[f,inp,out](v) = 1 p[f,out,inp](v) = 1 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } } foreach (f in Fields){ foreach(p in CrossInstrumField1-{id_pred,id_succ}){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin blur(Y); coerce(Y); Y end end } // ---------------------------------------------------------------------- // Call in case of two input parameters // ---------------------------------------------------------------------- /* name = name of the function (for display only) act1,act2 = actual parameters actfp1,actfp2 = formal parameter */ %function call_X_2[name, act1, act2, actfp1, actfp2](X) %t "Call_X_2 " + name + "(" + act1 + "," + act2 + ")" { begin let Y = transform(X, update:{ // Binding formal to actual actfp1(v) = act1(v) actfp2(v) = act2(v) // Forgetting all from the caller foreach (zz in VarAllFPR - { actfp1,actfp2 }){ zz(v) = 1/2 } // Copying [out] to [inp] (+ special stuff for fp1(v)=act1(v)) foreach (b in Bools){ b[inp](v) = b[out](v) b[ext](v) = 1/2 } foreach (f in Fields){ f[inp](v_1,v_2) = f[out](v_1,v_2) f[ext](v_1,v_2) = 1/2 } // Instrumentation foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,out](v) p[f,out](v) = p[f,out](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,out](v_1,v_2) p[f,out](v_1,v_2) = p[f,out](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (p in InstrumFieldVar1){ p[f,inp,actfp1](v) = p[f,out,act1](v) p[f,out,actfp1](v) = p[f,out,act1](v) p[f,ext,actfp1](v) = 1/2 p[f,inp,actfp2](v) = p[f,out,act2](v) p[f,out,actfp2](v) = p[f,out,act2](v) p[f,ext,actfp2](v) = 1/2 foreach(zz in VarAllFPR-{actfp1,actfp2}){ p[f,inp,zz](v) = 1/2 p[f,out,zz](v) = 1/2 p[f,ext,zz](v) = 1/2 } } foreach (p in InstrumFieldVar2){ p[f,inp,actfp1](v_1,v_2) = p[f,out,act1](v_1,v_2) p[f,out,actfp1](v_1,v_2) = p[f,out,act1](v_1,v_2) p[f,ext,actfp1](v_1,v_2) = 1/2 p[f,inp,actfp2](v_1,v_2) = p[f,out,act2](v_1,v_2) p[f,out,actfp2](v_1,v_2) = p[f,out,act2](v_1,v_2) p[f,ext,actfp2](v_1,v_2) = 1/2 foreach(zz in VarAllFPR-{actfp1,actfp2}){ p[f,inp,zz](v_1,v_2) = 1/2 p[f,out,zz](v_1,v_2) = 1/2 p[f,ext,zz](v_1,v_2) = 1/2 } } } foreach(p in InstrumMode1){ p[inp](v) = p[out](v) p[out](v) = p[out](v) p[ext](v) = 1/2 } foreach(p in InstrumMode2){ p[inp](v_1,v_2) = p[out](v_1,v_2) p[out](v_1,v_2) = p[out](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (p in InstrumModeVar1){ p[inp,actfp1](v) = p[out,act1](v) p[out,actfp1](v) = p[out,act1](v) p[ext,actfp1](v) = 1/2 p[inp,actfp2](v) = p[out,act2](v) p[out,actfp2](v) = p[out,act2](v) p[ext,actfp2](v) = 1/2 foreach(zz in VarAllFPR-{actfp1,actfp2}){ p[inp,zz](v) = 1/2 p[out,zz](v) = 1/2 p[ext,zz](v) = 1/2 } } foreach (p in InstrumModeVar2){ p[inp,actfp1](v_1,v_2) = p[out,act1](v_1,v_2) p[out,actfp1](v_1,v_2) = p[out,act1](v_1,v_2) p[ext,actfp1](v_1,v_2) = 1/2 p[inp,actfp2](v_1,v_2) = p[out,act2](v_1,v_2) p[out,actfp2](v_1,v_2) = p[out,act2](v_1,v_2) p[ext,actfp2](v_1,v_2) = 1/2 foreach(zz in VarAllFPR-{actfp1,actfp2}){ p[inp,zz](v_1,v_2) = 1/2 p[out,zz](v_1,v_2) = 1/2 p[ext,zz](v_1,v_2) = 1/2 } } // Cross Instrumentation foreach (f in Fields){ foreach(p in #ifdef ID_PRED {id_pred,id_succ} #else {id_succ} #endif ) { p[f,inp,out](v) = 1 p[f,out,inp](v) = 1 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } } foreach (f in Fields){ foreach(p in CrossInstrumField1-{id_pred,id_succ}){ p[f,inp,out](v) = 1/2 p[f,out,inp](v) = 1/2 p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = 1/2 p[f,out,inp](v_1,v_2) = 1/2 p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = 1/2 p[out,inp](v) = 1/2 p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = 1/2 p[out,inp](v_1,v_2) = 1/2 p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin blur(Y); coerce(Y); Y end end } // ====================================================================== // Returns // ====================================================================== /* Here we implement the function "combine" which unify envirnmenment of the caller with the environment of the callee. // ---------------------------------------------------------------------- // Return in case of one input and one output parameter // ---------------------------------------------------------------------- /* name = name of the function (for dispaly only) act1 = name of the actual parameter, ret1 = name of the returning actual parameter */ %function ret_1_1[ret1, name, act1](Xcaller,Xcallee) %t "Ret_1_1 " + ret1 + " := " + name + "(" + act1 + ")" { begin // Conversion to constraints toconstraints(Xcallee); // We put [ext] fields to 1/2 and equate fp1 to act1 in Xcaller let Xcaller = transform(Xcaller, update: { // We put [ext] fields to 1/2 foreach (f in Bools){ f[ext](v) = 1/2 } foreach (f in Fields){ f[ext](v_1,v_2) = 1/2 } // We make fr1 non determinated fr1(v) = 1/2 // We equate fp1 to act1 in Xcaller fp1(v) = act1(v) foreach (f in Fields){ foreach (p in InstrumFieldVar1){ p[f,out,fp1](v) = p[f,out,act1](v) } foreach (p in InstrumFieldVar2){ p[f,out,fp1](v_1,v_2) = p[f,out,act1](v_1,v_2) } } foreach (p in InstrumModeVar1){ p[out,fp1](v) = p[out,act1](v) } foreach (p in InstrumModeVar2){ p[out,fp1](v_1,v_2) = p[out,act1](v_1,v_2) } #ifdef COMPLETE // Input, Output left identical foreach (m in {inp,out}){ // Arity 1&2 foreach (f in Fields){ foreach (p in InstrumField1){ p[f,m](v) = p[f,m](v) } foreach (p in InstrumField2){ p[f,m](v_1,v_2) = p[f,m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fr1}){ foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = p[f,m,zz](v) } foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = p[f,m,zz](v_1,v_2) } } } foreach (p in InstrumMode1){ p[m](v) = p[m](v) } foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fr1}){ foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) } foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) } } } // Cross Instrumentation left identical foreach (m1 in Mode-{ext}){ foreach (m2 in Mode-{m1,ext}){ foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) } foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) } foreach (f in Fields){ foreach (p in CrossInstrumField1){ p[f,m1,m2](v) = p[f,m1,m2](v) } foreach (p in CrossInstrumField2){ p[f,m1,m2](v_1,v_2) = p[f,m1,m2](v_1,v_2) } } } } #endif }) in begin push(Xcaller,Xcallee); // We add them to Xcaller focus(Xcaller, { fr1(v) }); // We make f1(v) appear in Xmain // Coerce is applied after focus (we suppose the right option is turned on) pop(Xcaller); // We go back to the standard set of constraints /* We do several things the same time here. Semantically, 1. we perform the assignement ret1 := fr1 2. we get rid of predicates related to the callee (fp1 and fr1, and related instrumentation) 3. we eliminate predicates with 'out' mode 4. we perform the shift 'ext' -> 'out' Practically, we do it in one step. In the same time - we get rid of predicates related to the callee - we eliminate predicates with 'ext' mode - we assign 'out' to 'ext' The assignement is performed together with the shift */ let Y = transform(Xcaller, update:{ ret1(v) = fr1(v) fp1(v) = 1/2 fr1(v) = 1/2 foreach (f in Bools){ f[out](v) = f[ext](v) f[ext](v) = 1/2 } foreach (f in Fields){ f[out](v_1,v_2) = f[ext](v_1,v_2) f[ext](v_1,v_2) = 1/2 } foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,inp](v) p[f,out](v) = p[f,ext](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,inp](v_1,v_2) p[f,out](v_1,v_2) = p[f,ext](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (p in InstrumFieldVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v) = 1/2 } } p[f,inp,ret1](v) = p[f,inp,fr1](v) p[f,out,ret1](v) = p[f,ext,fr1](v) p[f,ext,ret1](v) = 1/2 foreach (zz in VarAll-{ret1}){ p[f,inp,zz](v) = p[f,inp,zz](v) p[f,out,zz](v) = p[f,ext,zz](v) p[f,ext,zz](v) = 1/2 } } foreach (p in InstrumFieldVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v_1,v_2) = 1/2 } } p[f,inp,ret1](v_1,v_2) = p[f,inp,fr1](v_1,v_2) p[f,out,ret1](v_1,v_2) = p[f,ext,fr1](v_1,v_2) p[f,ext,ret1](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1}){ p[f,inp,zz](v_1,v_2) = p[f,inp,zz](v_1,v_2) p[f,out,zz](v_1,v_2) = p[f,ext,zz](v_1,v_2) p[f,ext,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumMode1){ p[inp](v) = p[inp](v) p[out](v) = p[ext](v) p[ext](v) = 1/2 } foreach (p in InstrumMode2){ p[inp](v_1,v_2) = p[inp](v_1,v_2) p[out](v_1,v_2) = p[ext](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (p in InstrumModeVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v) = 1/2 } } p[inp,ret1](v) = p[inp,fr1](v) p[out,ret1](v) = p[ext,fr1](v) p[ext,ret1](v) = 1/2 foreach (zz in VarAll-{ret1}){ p[inp,zz](v) = p[inp,zz](v) p[out,zz](v) = p[ext,zz](v) p[ext,zz](v) = 1/2 } } foreach (p in InstrumModeVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v_1,v_2) = 1/2 } } p[inp,ret1](v_1,v_2) = p[inp,fr1](v_1,v_2) p[out,ret1](v_1,v_2) = p[ext,fr1](v_1,v_2) p[ext,ret1](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1}){ p[inp,zz](v_1,v_2) = p[inp,zz](v_1,v_2) p[out,zz](v_1,v_2) = p[ext,zz](v_1,v_2) p[ext,zz](v_1,v_2) = 1/2 } } // Cross Instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = p[f,inp,ext](v) p[f,out,inp](v) = p[f,ext,inp](v) p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = p[f,inp,ext](v_1,v_2) p[f,out,inp](v_1,v_2) = p[f,ext,inp](v_1,v_2) p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = p[inp,ext](v) p[out,inp](v) = p[ext,inp](v) p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = p[inp,ext](v_1,v_2) p[out,inp](v_1,v_2) = p[ext,inp](v_1,v_2) p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin blur(Y); coerce(Y); Y end end end } // ---------------------------------------------------------------------- // Return in case of one input and zero output parameter // ---------------------------------------------------------------------- /* name = name of the function (for dispaly only) act1 = name of the actual parameter, */ %function ret_0_1[name, act1](Xcaller,Xcallee) %t "Ret_0_1 " + name + "(" + act1 + ")" { begin // Conversion to constraints toconstraints(Xcallee); // We put [ext] fields to 1/2 and equate fp1 to act1 in Xcaller let Xcaller = transform(Xcaller, update: { // We put [ext] fields to 1/2 foreach (f in Bools){ f[ext](v) = 1/2 } foreach (f in Fields){ f[ext](v_1,v_2) = 1/2 } // We equate fp1 to act1 in Xcaller fp1(v) = act1(v) foreach (f in Fields){ foreach (p in InstrumFieldVar1){ p[f,out,fp1](v) = p[f,out,act1](v) } foreach (p in InstrumFieldVar2){ p[f,out,fp1](v_1,v_2) = p[f,out,act1](v_1,v_2) } } foreach (p in InstrumModeVar1){ p[out,fp1](v) = p[out,act1](v) } foreach (p in InstrumModeVar2){ p[out,fp1](v_1,v_2) = p[out,act1](v_1,v_2) } #ifdef COMPLETE // Input, Output left identical foreach (m in {inp,out}){ // Arity 1&2 foreach (f in Fields){ foreach (p in InstrumField1){ p[f,m](v) = p[f,m](v) } foreach (p in InstrumField2){ p[f,m](v_1,v_2) = p[f,m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1}){ foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = p[f,m,zz](v) } foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = p[f,m,zz](v_1,v_2) } } } foreach (p in InstrumMode1){ p[m](v) = p[m](v) } foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1}){ foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) } foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) } } } // Cross Instrumentation left identical foreach (m1 in Mode-{ext}){ foreach (m2 in Mode-{m1,ext}){ foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) } foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) } foreach (f in Fields){ foreach (p in CrossInstrumField1){ p[f,m1,m2](v) = p[f,m1,m2](v) } foreach (p in CrossInstrumField2){ p[f,m1,m2](v_1,v_2) = p[f,m1,m2](v_1,v_2) } } } } #endif }) in begin push(Xcaller,Xcallee); // We add them to Xcaller coerce(Xcaller); // Coerce is applied pop(Xcaller); // We go back to the standard set of constraints /* We do several things the same time here. Semantically, 1. we perform the assignement ret1 := fr1 2. we get rid of predicates related to the callee (fp1 and fr1, and related instrumentation) 3. we eliminate predicates with 'out' mode 4. we perform the shift 'ext' -> 'out' Practically, we do it in one step. In the same time - we get rid of predicates related to the callee - we eliminate predicates with 'ext' mode - we assign 'out' to 'ext' The assignement is performed together with the shift */ let Y = transform(Xcaller, update:{ fp1(v) = 1/2 foreach (f in Bools){ f[out](v) = f[ext](v) f[ext](v) = 1/2 } foreach (f in Fields){ f[out](v_1,v_2) = f[ext](v_1,v_2) f[ext](v_1,v_2) = 1/2 } foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,inp](v) p[f,out](v) = p[f,ext](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,inp](v_1,v_2) p[f,out](v_1,v_2) = p[f,ext](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (p in InstrumFieldVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v) = 1/2 } } foreach (zz in VarAll){ p[f,inp,zz](v) = p[f,inp,zz](v) p[f,out,zz](v) = p[f,ext,zz](v) p[f,ext,zz](v) = 1/2 } } foreach (p in InstrumFieldVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v_1,v_2) = 1/2 } } foreach (zz in VarAll){ p[f,inp,zz](v_1,v_2) = p[f,inp,zz](v_1,v_2) p[f,out,zz](v_1,v_2) = p[f,ext,zz](v_1,v_2) p[f,ext,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumMode1){ p[inp](v) = p[inp](v) p[out](v) = p[ext](v) p[ext](v) = 1/2 } foreach (p in InstrumMode2){ p[inp](v_1,v_2) = p[inp](v_1,v_2) p[out](v_1,v_2) = p[ext](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (p in InstrumModeVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v) = 1/2 } } foreach (zz in VarAll){ p[inp,zz](v) = p[inp,zz](v) p[out,zz](v) = p[ext,zz](v) p[ext,zz](v) = 1/2 } } foreach (p in InstrumModeVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v_1,v_2) = 1/2 } } foreach (zz in VarAll){ p[inp,zz](v_1,v_2) = p[inp,zz](v_1,v_2) p[out,zz](v_1,v_2) = p[ext,zz](v_1,v_2) p[ext,zz](v_1,v_2) = 1/2 } } // Cross Instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = p[f,inp,ext](v) p[f,out,inp](v) = p[f,ext,inp](v) p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = p[f,inp,ext](v_1,v_2) p[f,out,inp](v_1,v_2) = p[f,ext,inp](v_1,v_2) p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = p[inp,ext](v) p[out,inp](v) = p[ext,inp](v) p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = p[inp,ext](v_1,v_2) p[out,inp](v_1,v_2) = p[ext,inp](v_1,v_2) p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin blur(Y); coerce(Y); Y end end end } // ---------------------------------------------------------------------- // Return in case of two input and one output parameter // ---------------------------------------------------------------------- /* name = name of the function (for dispaly only) act1,act2 = name of the actual parameters, ret1 = name of the returning actual parameter */ %function ret_1_2[ret1, name, act1, act2](Xcaller,Xcallee) %t "Ret_1_2 " + ret1 + " := " + name + "(" + act1 + ", " + act2 + ")" { begin // Conversion to constraints toconstraints(Xcallee); // We put [ext] fields to 1/2 and equate fp1 to act1 in Xcaller let Xcaller = transform(Xcaller, update: { // We put [ext] fields to 1/2 foreach (f in Bools){ f[ext](v) = 1/2 } foreach (f in Fields){ f[ext](v_1,v_2) = 1/2 } // We make fr1 non determinated fr1(v) = 1/2 // We equate fp1 to act1 in Xcaller fp1(v) = act1(v) fp2(v) = act2(v) foreach (f in Fields){ foreach (p in InstrumFieldVar1){ p[f,out,fp1](v) = p[f,out,act1](v) p[f,out,fp2](v) = p[f,out,act2](v) } foreach (p in InstrumFieldVar2){ p[f,out,fp1](v_1,v_2) = p[f,out,act1](v_1,v_2) p[f,out,fp2](v_1,v_2) = p[f,out,act2](v_1,v_2) } } foreach (p in InstrumModeVar1){ p[out,fp1](v) = p[out,act1](v) p[out,fp2](v) = p[out,act2](v) } foreach (p in InstrumModeVar2){ p[out,fp1](v_1,v_2) = p[out,act1](v_1,v_2) p[out,fp2](v_1,v_2) = p[out,act2](v_1,v_2) } #ifdef COMPLETE // Input, Output left identical foreach (m in {inp,out}){ // Arity 1&2 foreach (f in Fields){ foreach (p in InstrumField1){ p[f,m](v) = p[f,m](v) } foreach (p in InstrumField2){ p[f,m](v_1,v_2) = p[f,m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fp2,fr1}){ foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = p[f,m,zz](v) } foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = p[f,m,zz](v_1,v_2) } } } foreach (p in InstrumMode1){ p[m](v) = p[m](v) } foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fp2,fr1}){ foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) } foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) } } } // Cross Instrumentation left identical foreach (m1 in Mode-{ext}){ foreach (m2 in Mode-{m1,ext}){ foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) } foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) } foreach (f in Fields){ foreach (p in CrossInstrumField1){ p[f,m1,m2](v) = p[f,m1,m2](v) } foreach (p in CrossInstrumField2){ p[f,m1,m2](v_1,v_2) = p[f,m1,m2](v_1,v_2) } } } } #endif }) in begin push(Xcaller,Xcallee); // We add them to Xcaller focus(Xcaller, { fr1(v) }); // We make f1(v) appear in Xmain // Coerce is applied after focus (we suppose the right option is turned on) pop(Xcaller); // We go back to the standard set of constraints /* We do several things the same time here. Semantically, 1. we perform the assignement ret1 := fr1 2. we get rid of predicates related to the callee (fp1 and fr1, and related instrumentation) 3. we eliminate predicates with 'out' mode 4. we perform the shift 'ext' -> 'out' Practically, we do it in one step. In the same time - we get rid of predicates related to the callee - we eliminate predicates with 'ext' mode - we assign 'out' to 'ext' The assignement is performed together with the shift */ let Y = transform(Xcaller, update:{ ret1(v) = fr1(v) fp1(v) = 1/2 fp2(v) = 1/2 fr1(v) = 1/2 foreach (f in Bools){ f[out](v) = f[ext](v) f[ext](v) = 1/2 } foreach (f in Fields){ f[out](v_1,v_2) = f[ext](v_1,v_2) f[ext](v_1,v_2) = 1/2 } foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,inp](v) p[f,out](v) = p[f,ext](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,inp](v_1,v_2) p[f,out](v_1,v_2) = p[f,ext](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (p in InstrumFieldVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v) = 1/2 } } p[f,inp,ret1](v) = p[f,inp,fr1](v) p[f,out,ret1](v) = p[f,ext,fr1](v) p[f,ext,ret1](v) = 1/2 foreach (zz in VarAll-{ret1}){ p[f,inp,zz](v) = p[f,inp,zz](v) p[f,out,zz](v) = p[f,ext,zz](v) p[f,ext,zz](v) = 1/2 } } foreach (p in InstrumFieldVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v_1,v_2) = 1/2 } } p[f,inp,ret1](v_1,v_2) = p[f,inp,fr1](v_1,v_2) p[f,out,ret1](v_1,v_2) = p[f,ext,fr1](v_1,v_2) p[f,ext,ret1](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1}){ p[f,inp,zz](v_1,v_2) = p[f,inp,zz](v_1,v_2) p[f,out,zz](v_1,v_2) = p[f,ext,zz](v_1,v_2) p[f,ext,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumMode1){ p[inp](v) = p[inp](v) p[out](v) = p[ext](v) p[ext](v) = 1/2 } foreach (p in InstrumMode2){ p[inp](v_1,v_2) = p[inp](v_1,v_2) p[out](v_1,v_2) = p[ext](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (p in InstrumModeVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v) = 1/2 } } p[inp,ret1](v) = p[inp,fr1](v) p[out,ret1](v) = p[ext,fr1](v) p[ext,ret1](v) = 1/2 foreach (zz in VarAll-{ret1}){ p[inp,zz](v) = p[inp,zz](v) p[out,zz](v) = p[ext,zz](v) p[ext,zz](v) = 1/2 } } foreach (p in InstrumModeVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v_1,v_2) = 1/2 } } p[inp,ret1](v_1,v_2) = p[inp,fr1](v_1,v_2) p[out,ret1](v_1,v_2) = p[ext,fr1](v_1,v_2) p[ext,ret1](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1}){ p[inp,zz](v_1,v_2) = p[inp,zz](v_1,v_2) p[out,zz](v_1,v_2) = p[ext,zz](v_1,v_2) p[ext,zz](v_1,v_2) = 1/2 } } // Cross Instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = p[f,inp,ext](v) p[f,out,inp](v) = p[f,ext,inp](v) p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = p[f,inp,ext](v_1,v_2) p[f,out,inp](v_1,v_2) = p[f,ext,inp](v_1,v_2) p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = p[inp,ext](v) p[out,inp](v) = p[ext,inp](v) p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = p[inp,ext](v_1,v_2) p[out,inp](v_1,v_2) = p[ext,inp](v_1,v_2) p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin blur(Y); coerce(Y); Y end end end } // ---------------------------------------------------------------------- // Return in case of one input and two output parameter // ---------------------------------------------------------------------- /* name = name of the function (for dispaly only) act1 = name of the actual parameter ret1,ret2 = name of the returning actual parameter */ %function ret_2_1[ret1, ret2, name, act1](Xcaller,Xcallee) %t "Ret_2_2 (" + ret1 + ", " + ret2 + ") := " + name + "(" + act1 + ")" { begin // Conversion to constraints toconstraints(Xcallee); // We put [ext] fields to 1/2 and equate fp1 to act1 in Xcaller let Xcaller = transform(Xcaller, update: { // We put [ext] fields to 1/2 foreach (f in Bools){ f[ext](v) = 1/2 } foreach (f in Fields){ f[ext](v_1,v_2) = 1/2 } // We make fr1 non determinated fr1(v) = 1/2 fr2(v) = 1/2 // We equate fp1 to act1 in Xcaller fp1(v) = act1(v) foreach (f in Fields){ foreach (p in InstrumFieldVar1){ p[f,out,fp1](v) = p[f,out,act1](v) p[f,out,fp2](v) = p[f,out,act2](v) } foreach (p in InstrumFieldVar2){ p[f,out,fp1](v_1,v_2) = p[f,out,act1](v_1,v_2) p[f,out,fp2](v_1,v_2) = p[f,out,act2](v_1,v_2) } } foreach (p in InstrumModeVar1){ p[out,fp1](v) = p[out,act1](v) p[out,fp2](v) = p[out,act2](v) } foreach (p in InstrumModeVar2){ p[out,fp1](v_1,v_2) = p[out,act1](v_1,v_2) p[out,fp2](v_1,v_2) = p[out,act2](v_1,v_2) } #ifdef COMPLETE // Input, Output left identical foreach (m in {inp,out}){ // Arity 1&2 foreach (f in Fields){ foreach (p in InstrumField1){ p[f,m](v) = p[f,m](v) } foreach (p in InstrumField2){ p[f,m](v_1,v_2) = p[f,m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fr1,fr2}){ foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = p[f,m,zz](v) } foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = p[f,m,zz](v_1,v_2) } } } foreach (p in InstrumMode1){ p[m](v) = p[m](v) } foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fr1,fr2}){ foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) } foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) } } } // Cross Instrumentation left identical foreach (m1 in Mode-{ext}){ foreach (m2 in Mode-{m1,ext}){ foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) } foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) } foreach (f in Fields){ foreach (p in CrossInstrumField1){ p[f,m1,m2](v) = p[f,m1,m2](v) } foreach (p in CrossInstrumField2){ p[f,m1,m2](v_1,v_2) = p[f,m1,m2](v_1,v_2) } } } } #endif }) in begin push(Xcaller,Xcallee); // We add them to Xcaller focus(Xcaller, { fr1(v), fr2(v) }); // We make f1(v) appear in Xmain // Coerce is applied after focus (we suppose the right option is turned on) pop(Xcaller); // We go back to the standard set of constraints /* We do several things the same time here. Semantically, 1. we perform the assignement ret1 := fr1 2. we get rid of predicates related to the callee (fp1 and fr1, and related instrumentation) 3. we eliminate predicates with 'out' mode 4. we perform the shift 'ext' -> 'out' Practically, we do it in one step. In the same time - we get rid of predicates related to the callee - we eliminate predicates with 'ext' mode - we assign 'out' to 'ext' The assignement is performed together with the shift */ let Y = transform(Xcaller, update:{ ret1(v) = fr1(v) ret2(v) = fr2(v) fp1(v) = 1/2 fr1(v) = 1/2 fr2(v) = 1/2 foreach (f in Bools){ f[out](v) = f[ext](v) f[ext](v) = 1/2 } foreach (f in Fields){ f[out](v_1,v_2) = f[ext](v_1,v_2) f[ext](v_1,v_2) = 1/2 } foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,inp](v) p[f,out](v) = p[f,ext](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,inp](v_1,v_2) p[f,out](v_1,v_2) = p[f,ext](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (p in InstrumFieldVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v) = 1/2 } } p[f,inp,ret1](v) = p[f,inp,fr1](v) p[f,out,ret1](v) = p[f,ext,fr1](v) p[f,ext,ret1](v) = 1/2 p[f,inp,ret2](v) = p[f,inp,fr2](v) p[f,out,ret2](v) = p[f,ext,fr2](v) p[f,ext,ret2](v) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[f,inp,zz](v) = p[f,inp,zz](v) p[f,out,zz](v) = p[f,ext,zz](v) p[f,ext,zz](v) = 1/2 } } foreach (p in InstrumFieldVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v_1,v_2) = 1/2 } } p[f,inp,ret1](v_1,v_2) = p[f,inp,fr1](v_1,v_2) p[f,out,ret1](v_1,v_2) = p[f,ext,fr1](v_1,v_2) p[f,ext,ret1](v_1,v_2) = 1/2 p[f,inp,ret2](v_1,v_2) = p[f,inp,fr2](v_1,v_2) p[f,out,ret2](v_1,v_2) = p[f,ext,fr2](v_1,v_2) p[f,ext,ret2](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[f,inp,zz](v_1,v_2) = p[f,inp,zz](v_1,v_2) p[f,out,zz](v_1,v_2) = p[f,ext,zz](v_1,v_2) p[f,ext,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumMode1){ p[inp](v) = p[inp](v) p[out](v) = p[ext](v) p[ext](v) = 1/2 } foreach (p in InstrumMode2){ p[inp](v_1,v_2) = p[inp](v_1,v_2) p[out](v_1,v_2) = p[ext](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (p in InstrumModeVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v) = 1/2 } } p[inp,ret1](v) = p[inp,fr1](v) p[out,ret1](v) = p[ext,fr1](v) p[ext,ret1](v) = 1/2 p[inp,ret2](v) = p[inp,fr2](v) p[out,ret2](v) = p[ext,fr2](v) p[ext,ret2](v) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[inp,zz](v) = p[inp,zz](v) p[out,zz](v) = p[ext,zz](v) p[ext,zz](v) = 1/2 } } foreach (p in InstrumModeVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v_1,v_2) = 1/2 } } p[inp,ret1](v_1,v_2) = p[inp,fr1](v_1,v_2) p[out,ret1](v_1,v_2) = p[ext,fr1](v_1,v_2) p[ext,ret1](v_1,v_2) = 1/2 p[inp,ret2](v_1,v_2) = p[inp,fr2](v_1,v_2) p[out,ret2](v_1,v_2) = p[ext,fr2](v_1,v_2) p[ext,ret2](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[inp,zz](v_1,v_2) = p[inp,zz](v_1,v_2) p[out,zz](v_1,v_2) = p[ext,zz](v_1,v_2) p[ext,zz](v_1,v_2) = 1/2 } } // Cross Instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = p[f,inp,ext](v) p[f,out,inp](v) = p[f,ext,inp](v) p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = p[f,inp,ext](v_1,v_2) p[f,out,inp](v_1,v_2) = p[f,ext,inp](v_1,v_2) p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = p[inp,ext](v) p[out,inp](v) = p[ext,inp](v) p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = p[inp,ext](v_1,v_2) p[out,inp](v_1,v_2) = p[ext,inp](v_1,v_2) p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin blur(Y); coerce(Y); Y end end end } // ---------------------------------------------------------------------- // Return in case of two input and two output parameter // ---------------------------------------------------------------------- /* name = name of the function (for dispaly only) act1,act2 = name of the actual parameters, ret1,ret2 = name of the returning actual parameter */ %function ret_2_2[ret1, ret2, name, act1, act2](Xcaller,Xcallee) %t "Ret_2_2 (" + ret1 + ", " + ret2 + ") := " + name + "(" + act1 + ", " + act2 + ")" { begin // Conversion to constraints toconstraints(Xcallee); // We put [ext] fields to 1/2 and equate fp1 to act1 in Xcaller let Xcaller = transform(Xcaller, update: { // We put [ext] fields to 1/2 foreach (f in Bools){ f[ext](v) = 1/2 } foreach (f in Fields){ f[ext](v_1,v_2) = 1/2 } // We make fr1 non determinated fr1(v) = 1/2 fr2(v) = 1/2 // We equate fp1 to act1 in Xcaller fp1(v) = act1(v) fp2(v) = act2(v) foreach (f in Fields){ foreach (p in InstrumFieldVar1){ p[f,out,fp1](v) = p[f,out,act1](v) p[f,out,fp2](v) = p[f,out,act2](v) } foreach (p in InstrumFieldVar2){ p[f,out,fp1](v_1,v_2) = p[f,out,act1](v_1,v_2) p[f,out,fp2](v_1,v_2) = p[f,out,act2](v_1,v_2) } } foreach (p in InstrumModeVar1){ p[out,fp1](v) = p[out,act1](v) p[out,fp2](v) = p[out,act2](v) } foreach (p in InstrumModeVar2){ p[out,fp1](v_1,v_2) = p[out,act1](v_1,v_2) p[out,fp2](v_1,v_2) = p[out,act2](v_1,v_2) } #ifdef COMPLETE // Input, Output left identical foreach (m in {inp,out}){ // Arity 1&2 foreach (f in Fields){ foreach (p in InstrumField1){ p[f,m](v) = p[f,m](v) } foreach (p in InstrumField2){ p[f,m](v_1,v_2) = p[f,m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fp2,fr1,fr2}){ foreach (p in InstrumFieldVar1){ p[f,m,zz](v) = p[f,m,zz](v) } foreach (p in InstrumFieldVar2){ p[f,m,zz](v_1,v_2) = p[f,m,zz](v_1,v_2) } } } foreach (p in InstrumMode1){ p[m](v) = p[m](v) } foreach (p in InstrumMode2){ p[m](v_1,v_2) = p[m](v_1,v_2) } foreach (zz in VarAllFPR - {fp1,fp2,fr1,fr2}){ foreach (p in InstrumModeVar1){ p[m,zz](v) = p[m,zz](v) } foreach (p in InstrumModeVar2){ p[m,zz](v_1,v_2) = p[m,zz](v_1,v_2) } } } // Cross Instrumentation left identical foreach (m1 in Mode-{ext}){ foreach (m2 in Mode-{m1,ext}){ foreach (p in CrossInstrum1){ p[m1,m2](v) = p[m1,m2](v) } foreach (p in CrossInstrum2){ p[m1,m2](v_1,v_2) = p[m1,m2](v_1,v_2) } foreach (f in Fields){ foreach (p in CrossInstrumField1){ p[f,m1,m2](v) = p[f,m1,m2](v) } foreach (p in CrossInstrumField2){ p[f,m1,m2](v_1,v_2) = p[f,m1,m2](v_1,v_2) } } } } #endif }) in begin push(Xcaller,Xcallee); // We add them to Xcaller focus(Xcaller, { fr1(v), fr2(v) }); // We make f1(v) appear in Xmain // Coerce is applied after focus (we suppose the right option is turned on) pop(Xcaller); // We go back to the standard set of constraints /* We do several things the same time here. Semantically, 1. we perform the assignement ret1 := fr1 2. we get rid of predicates related to the callee (fp1 and fr1, and related instrumentation) 3. we eliminate predicates with 'out' mode 4. we perform the shift 'ext' -> 'out' Practically, we do it in one step. In the same time - we get rid of predicates related to the callee - we eliminate predicates with 'ext' mode - we assign 'out' to 'ext' The assignement is performed together with the shift */ let Y = transform(Xcaller, update:{ ret1(v) = fr1(v) ret2(v) = fr2(v) fp1(v) = 1/2 fp2(v) = 1/2 fr1(v) = 1/2 fr2(v) = 1/2 foreach (f in Bools){ f[out](v) = f[ext](v) f[ext](v) = 1/2 } foreach (f in Fields){ f[out](v_1,v_2) = f[ext](v_1,v_2) f[ext](v_1,v_2) = 1/2 } foreach (f in Fields){ foreach (p in InstrumField1){ p[f,inp](v) = p[f,inp](v) p[f,out](v) = p[f,ext](v) p[f,ext](v) = 1/2 } foreach (p in InstrumField2){ p[f,inp](v_1,v_2) = p[f,inp](v_1,v_2) p[f,out](v_1,v_2) = p[f,ext](v_1,v_2) p[f,ext](v_1,v_2) = 1/2 } foreach (p in InstrumFieldVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v) = 1/2 } } p[f,inp,ret1](v) = p[f,inp,fr1](v) p[f,out,ret1](v) = p[f,ext,fr1](v) p[f,ext,ret1](v) = 1/2 p[f,inp,ret2](v) = p[f,inp,fr2](v) p[f,out,ret2](v) = p[f,ext,fr2](v) p[f,ext,ret2](v) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[f,inp,zz](v) = p[f,inp,zz](v) p[f,out,zz](v) = p[f,ext,zz](v) p[f,ext,zz](v) = 1/2 } } foreach (p in InstrumFieldVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[f,m,zz](v_1,v_2) = 1/2 } } p[f,inp,ret1](v_1,v_2) = p[f,inp,fr1](v_1,v_2) p[f,out,ret1](v_1,v_2) = p[f,ext,fr1](v_1,v_2) p[f,ext,ret1](v_1,v_2) = 1/2 p[f,inp,ret2](v_1,v_2) = p[f,inp,fr2](v_1,v_2) p[f,out,ret2](v_1,v_2) = p[f,ext,fr2](v_1,v_2) p[f,ext,ret2](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[f,inp,zz](v_1,v_2) = p[f,inp,zz](v_1,v_2) p[f,out,zz](v_1,v_2) = p[f,ext,zz](v_1,v_2) p[f,ext,zz](v_1,v_2) = 1/2 } } } foreach (p in InstrumMode1){ p[inp](v) = p[inp](v) p[out](v) = p[ext](v) p[ext](v) = 1/2 } foreach (p in InstrumMode2){ p[inp](v_1,v_2) = p[inp](v_1,v_2) p[out](v_1,v_2) = p[ext](v_1,v_2) p[ext](v_1,v_2) = 1/2 } foreach (p in InstrumModeVar1){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v) = 1/2 } } p[inp,ret1](v) = p[inp,fr1](v) p[out,ret1](v) = p[ext,fr1](v) p[ext,ret1](v) = 1/2 p[inp,ret2](v) = p[inp,fr2](v) p[out,ret2](v) = p[ext,fr2](v) p[ext,ret2](v) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[inp,zz](v) = p[inp,zz](v) p[out,zz](v) = p[ext,zz](v) p[ext,zz](v) = 1/2 } } foreach (p in InstrumModeVar2){ foreach (zz in FP+FR){ foreach (m in Mode){ p[m,zz](v_1,v_2) = 1/2 } } p[inp,ret1](v_1,v_2) = p[inp,fr1](v_1,v_2) p[out,ret1](v_1,v_2) = p[ext,fr1](v_1,v_2) p[ext,ret1](v_1,v_2) = 1/2 p[inp,ret2](v_1,v_2) = p[inp,fr2](v_1,v_2) p[out,ret2](v_1,v_2) = p[ext,fr2](v_1,v_2) p[ext,ret2](v_1,v_2) = 1/2 foreach (zz in VarAll-{ret1,ret2}){ p[inp,zz](v_1,v_2) = p[inp,zz](v_1,v_2) p[out,zz](v_1,v_2) = p[ext,zz](v_1,v_2) p[ext,zz](v_1,v_2) = 1/2 } } // Cross Instrumentation foreach (f in Fields){ foreach(p in CrossInstrumField1){ p[f,inp,out](v) = p[f,inp,ext](v) p[f,out,inp](v) = p[f,ext,inp](v) p[f,inp,ext](v) = 1/2 p[f,ext,inp](v) = 1/2 p[f,out,ext](v) = 1/2 p[f,ext,out](v) = 1/2 } foreach(p in CrossInstrumField2){ p[f,inp,out](v_1,v_2) = p[f,inp,ext](v_1,v_2) p[f,out,inp](v_1,v_2) = p[f,ext,inp](v_1,v_2) p[f,inp,ext](v_1,v_2) = 1/2 p[f,ext,inp](v_1,v_2) = 1/2 p[f,out,ext](v_1,v_2) = 1/2 p[f,ext,out](v_1,v_2) = 1/2 } } foreach(p in CrossInstrum1){ p[inp,out](v) = p[inp,ext](v) p[out,inp](v) = p[ext,inp](v) p[inp,ext](v) = 1/2 p[ext,inp](v) = 1/2 p[out,ext](v) = 1/2 p[ext,out](v) = 1/2 } foreach(p in CrossInstrum2){ p[inp,out](v_1,v_2) = p[inp,ext](v_1,v_2) p[out,inp](v_1,v_2) = p[ext,inp](v_1,v_2) p[inp,ext](v_1,v_2) = 1/2 p[ext,inp](v_1,v_2) = 1/2 p[out,ext](v_1,v_2) = 1/2 p[ext,out](v_1,v_2) = 1/2 } }) in begin blur(Y); coerce(Y); Y end end end }