From a3817afc787a37cc1c81cfabddcd9e92cd72cf9f Mon Sep 17 00:00:00 2001
From: Lucien <lucien.rakotomalala@onera.fr>
Date: Mon, 11 Oct 2021 15:55:03 +0200
Subject: [PATCH] Renaming case files
Update name in nc file and update old comment about previous S6 (now S5_2).
---
examples/case_study/CaseStudy.nc | 188 +++++++++++++++++---------
examples/case_study/arbitrary_flows.v | 4 +-
2 files changed, 124 insertions(+), 68 deletions(-)
diff --git a/examples/case_study/CaseStudy.nc b/examples/case_study/CaseStudy.nc
index d67c5d49..78d8277b 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 4c56bf3e..d883c60d 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 :
--
GitLab