channel C_CustomerAOff_In {
	out customerA_off(c:String, setOff(x)) = x
	out customerA_off(c, e) = c
}

channel C_CustomerBOff_In {
	out customerB_off(c:String, setOff(x)) = x
	out customerB_off(c, e) = c
}

channel C_CompanyC1Add_In {
	out companyC1_add(a:String, setAdd(y)) = y
	out companyC1_add(a, e) = a
}

channel C_CompanyC2Add_In {
	out companyC2_add(a:String, setAdd(y)) = y
	out companyC2_add(a, e) = a
}

channel CA {
	in customerA_off(c, sync(z, u, v)) = z
	in companyC1_add(a1, sync(z, u, v)) = u
	in companyC2_add(a2, sync(z, u, v)) = v
	out customerA_add(a3:String, sync(z, u, v)) = if(z == C1, u, if(z == C2, v, null))
}

channel CB {
	in customerB_off(c, sync(z, u, v)) = z
	in companyC1_add(a1, sync(z, u, v)) = u
	in companyC2_add(a2, sync(z, u, v)) = v
	out customerB_add(a3:String, sync(z, u, v)) = if(z == C1, u, if(z == C2, v, null))
}