diff --git a/examples/case_study/CaseStudy.nc b/examples/case_study/CaseStudy.nc
index d67c5d49b20f350abc2f526b0ced4b63946a31ff..78d8277be19d042054965c0efebff03b769c4231 100644
--- a/examples/case_study/CaseStudy.nc
+++ b/examples/case_study/CaseStudy.nc
@@ -15,119 +15,175 @@ TenPow5:= 100000
 ##    Frame/Burst size: 1000 bytes = 8000 bits
 ##    Throughput: 20Mb/s = 20Kb/ms
 
-f1:= bucket(20000, 8000)
-f2:= f1
-f3:= f1
-f4:= f1
-f5:= f1
+alpha1:= bucket(20000, 8000)
+alpha2:= alpha1
+alpha3:= alpha1
+alpha4:= alpha1
+alpha5:= alpha1
+
+##################################
+## Servers Rate
+##    Rate : 100Mb/s
+
+beta1:= affine(TenPow5,0)
+beta2:= beta1
+beta3:= beta1
+beta4:= beta1
+beta5:= beta1
 
 ###################################
 ## First server : S1
 ##    Throughput: 100Mb/s = 100Kb/ms
 ##    Input: f1, f2, f3
 
+alpha_S1:= alpha1 + alpha2
+alpha_S1:= alpha_S1 + alpha3
+  
+beta_S1_delay:= hdev(alpha_S1, beta1)
 
-capacity:= affine(TenPow5,0)
-S1_input:= f1 + f2
-S1_input:= S1_input + f3
+beta_S1:= delay( beta_S1_delay )
 
-S1_FIFO_delay:= hdev(S1_input, capacity)
-S1_FIFO_delay
-S1_FIFO_service:= delay( S1_FIFO_delay )
-plot( S1_FIFO_service, S1_input, capacity, xlim=[0,1], ylim=[0,50000], main="Server S1: total input, capacity and delay")
+alpha1_S1':= alpha1 / beta_S1
+alpha2_S1':= alpha2 / beta_S1
+alpha3_S1':= alpha3 / beta_S1
 
-f1_S1:= ( f1 / S1_FIFO_service )
-f2_S1:= ( f2 / S1_FIFO_service )
-f3_S1:= ( f3 / S1_FIFO_service )
+alpha1_S1:= alpha1_S1' /\ d0
+alpha2_S1:= alpha2_S1' /\ d0
+alpha3_S1:= alpha3_S1' /\ d0
 
+###################################
+## Second server : S2 1
+
+beta_S2_1_delay:= hdev( alpha1_S1, beta2 )
+
+beta_S2_1:= delay( beta_S2_1_delay )
+
+alpha1_S2' := ( alpha1_S1 / beta_S2_1 )
+
+alpha1_S2 := alpha1_S2' /\ d0
 
 ###################################
-## Second server : S2
-##   Made of 3 output ports called internally
-##  S2_f1, S2_f2, S2_f3
+## Second server : S2_2
 
-S2_f1_FIFO_delay:= hdev( f1_S1, capacity )
-S2_f1_FIFO_service:= delay( S2_f1_FIFO_delay )
-f1_S2:= ( f1_S1 / S2_f1_FIFO_service )
+beta_S2_2_delay:= hdev( alpha2_S1, beta2 )
 
-S2_f2_FIFO_delay:= hdev( f2_S1, capacity )
-S2_f2_FIFO_service:= delay( S2_f2_FIFO_delay )
-f2_S2:= ( f2_S1 / S2_f2_FIFO_service )
+beta_S2_2:= delay( beta_S2_2_delay )
 
-S2_f3_FIFO_delay:= hdev( f3_S1, capacity )
-S2_f3_FIFO_service:= delay( S2_f3_FIFO_delay )
-f3_S2:= ( f3_S1 / S2_f3_FIFO_service )
+alpha2_S2':= ( alpha2_S1 / beta_S2_2 )
+
+alpha2_S2 := alpha2_S2' /\ d0
+
+###################################
+## Second server : S2 3
+
+beta_S2_3_delay:= hdev( alpha3_S1, beta2 )
+
+beta_S2_3:= delay( beta_S2_3_delay )
+
+alpha3_S2':= ( alpha3_S1 / beta_S2_3 )
+
+alpha3_S2 := alpha3_S2' /\ d0
 
 ###################################
 ## Third server: S3
 ##    Throughput: 100Mb/s = 100Kb/ms
 ##    Input: f1, f4
 
-S3_input:= f1_S2 + f4
-S3_FIFO_delay:= hdev(S3_input, capacity)
-S3_FIFO_service:= delay( S3_FIFO_delay )
-plot( S3_FIFO_service, S3_input, capacity, xlim=[0,1], ylim=[0,50000], main="Server S3: total input, capacity and delay")
-f1_S3:= ( f1_S2 / S3_FIFO_service )
-f4_S3:= ( f4    / S3_FIFO_service )
+alpha_S3:= alpha1_S2 + alpha4
+
+beta_S3_delay:= hdev(alpha_S3, beta3)
+
+beta_S3 := delay( beta_S3_delay )
+
+alpha1_S3':= (alpha1_S2 / beta_S3 )
+alpha4_S3':= (alpha4    / beta_S3 )
+
+alpha1_S3 := alpha1_S3'	 /\ d0
+alpha4_S3 := alpha4_S3'	 /\ d0
 
 ###################################
 ## Fourth server: S4
 ##    Throughput: 100Mb/s = 100Kb/ms
 ##    Input: f3, f5
 
-S4_input:= f3_S2 + f5
-S4_FIFO_delay:= hdev(S4_input, capacity)
-S4_FIFO_service:= delay( S4_FIFO_delay )
-f3_S4:= ( f3_S2 / S4_FIFO_service )
-f5_S4:= ( f5    / S4_FIFO_service )
+alpha_S4 := alpha3_S2 + alpha5
+
+beta_S4_delay := hdev(alpha_S4, beta4)
+
+beta_S4 := delay( beta_S4_delay )
+
+alpha3_S4':= ( alpha3_S2 / beta_S4 )
+alpha5_S4':= ( alpha5    / beta_S4 )
+
+alpha3_S4:= alpha3_S4' /\ d0
+alpha5_S4:=  alpha5_S4' /\ d0
 
 ###################################
-## Fifth server/ first port: S5
+## Fifth server/ first port: S5_1
 ##    Throughput: 100Mb/s = 100Kb/ms
 ##    Input: f1,f2,f3
 
-S5_input:= f1_S3 + f2_S2
-S5_input:= S5_input + f3_S4
-S5_FIFO_delay:= hdev(S5_input, capacity)
-S5_FIFO_service:= delay( S5_FIFO_delay )
+alpha_S5_1:= alpha1_S3 + alpha2_S2
+alpha_S5_1:= alpha_S5_1 + alpha3_S4
+
+beta_S5_1_delay := hdev(alpha_S5_1, beta5)
+
+beta_S5_1 := delay( beta_S5_1_delay )
 
 ###################################
-## Fifth server/ second port: S6
+## Fifth server/ second port: S5_2
 ##    Throughput: 100Mb/s = 100Kb/ms
 ##    Input: f4,f5
 
-S6_input:= f4_S3 + f5_S4
-S6_FIFO_delay:= hdev(S6_input, capacity)
-S6_FIFO_service:= delay( S6_FIFO_delay )
+alpha_S5_2:= alpha4_S3 + alpha5_S4
+
+beta_S5_2_delay:= hdev(alpha_S5_2, beta5)
+
+beta_S5_2 := delay( beta_S5_2_delay )
 
+###################################
+####   End-to-end delays ##########
 
 ###################################
-## End-to-end delays
+### f1
+
+beta1_E2E:= ( beta_S1 * beta_S2_1 ) * beta_S3
+beta1_E2E:= f1_E2E_service * beta_S5_1
 
-f1_E2E_service:= ( S1_FIFO_service * S3_FIFO_service ) * S5_FIFO_service
-f1_E2E_service:= f1_E2E_service * S2_f1_FIFO_service
-f1_E2E_delay:= hdev(f1, f1_E2E_service)
+f1_E2E_delay:= hdev(alpha1, f1_E2E_service)
 f1_E2E_delay
-# 3612/3125 = 1.15584ms
 
-f2_E2E_service:=  S1_FIFO_service * S5_FIFO_service
-f2_E2E_service:= f2_E2E_service * S2_f2_FIFO_service
-f2_E2E_delay:= hdev(f2, f2_E2E_service)
+###################################
+### f2
+
+f2_E2E_service:=  beta_S1 * beta_S5_1
+f2_E2E_service:= f2_E2E_service * beta_S2_2
+
+f2_E2E_delay:= hdev(alpha2, f2_E2E_service)
 f2_E2E_delay
-# 2882/3125 = 0.92224 ms
 
-f3_E2E_service:= ( S1_FIFO_service * S4_FIFO_service ) * S5_FIFO_service
-f3_E2E_service:= f3_E2E_service * S2_f3_FIFO_service
-f3_E2E_delay:= hdev(f3, f3_E2E_service)
+###################################
+### f3
+
+f3_E2E_service:= ( beta_S1 * beta_S4 ) * beta_S5_1
+f3_E2E_service:= f3_E2E_service * beta_S2_3
+
+f3_E2E_delay:= hdev(alpha3, f3_E2E_service)
 f3_E2E_delay
-# 3612/3125 = 1.15584ms
 
-f4_E2E_service:=  S3_FIFO_service * S6_FIFO_service
-f4_E2E_delay:= hdev(f4, f4_E2E_service)
+###################################
+### f4
+
+f4_E2E_service:=  beta_S3 * beta_S5_1
+f4_E2E_service
+
+f4_E2E_delay:= hdev(alpha4, f4_E2E_service)
 f4_E2E_delay
-# 1522/3125 = 0.48704 ms
 
-f5_E2E_service:=  S4_FIFO_service * S6_FIFO_service
-f5_E2E_delay:= hdev(f5, f5_E2E_service)
+###################################
+### f5
+
+f5_E2E_service:=  beta_S4 * beta_S5_1
+
+f5_E2E_delay:= hdev(alpha5, f5_E2E_service)
 f5_E2E_delay
-# 1522/3125 = 0.48704 ms
diff --git a/examples/case_study/arbitrary_flows.v b/examples/case_study/arbitrary_flows.v
index 4c56bf3e83fd1c50e38c753076d7cc9992d3a3c3..d883c60d099da9cc9cef706ec7fd4c2f6fcf5766 100644
--- a/examples/case_study/arbitrary_flows.v
+++ b/examples/case_study/arbitrary_flows.v
@@ -119,7 +119,7 @@ Hypothesis H_server_S4 :
     (finfun_of_tuple [tuple F3_S2; F5])
     (finfun_of_tuple [tuple F3_S4; F5_S4]).
 
-(** Server 5 ***************************************************)
+(** Server 5 -1 ************************************************)
 Variables F1_S5 F2_S5 F3_S5 : flow_cc.
 
 Hypothesis H_server_S5_1 :
@@ -127,7 +127,7 @@ Hypothesis H_server_S5_1 :
     (finfun_of_tuple [tuple F1_S3; F2_S2; F3_S4])
     (finfun_of_tuple [tuple F1_S5; F2_S5; F3_S5]).
 
-(** Server 6 ***************************************************)
+(** Server 5 -2 ************************************************)
 Variables F4_S5 F5_S5 : flow_cc.
 
 Hypothesis H_server_S5_2 :