/* 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
}