Index: papers/FDL2012/exp_results.tex
===================================================================
--- papers/FDL2012/exp_results.tex	(revision 80)
+++ papers/FDL2012/exp_results.tex	(revision 83)
@@ -14,8 +14,8 @@
 \midrule
 \midrule
-               & 1 Master-1 Slave   & 308  & 33 442   & 3.64116e+06 & 41.49 \\
- Concrete      & 2 Masters-1 Slave  & 453  & 140297   & 2.42518e+11 & 1922.75 \\
-  Model        & 4 Masters-1 Slave  & 737  & N/A      & N/A         & >3days \\
-               & 4 Masters-2 Slaves & 911  & N/A      & N/A         & >3days \\
+               & 1 Master-1 Slave   & 304  & 7207     & 4.711e+3    & 6.36 \\
+ Concrete      & 2 Masters-1 Slave  & 445  & 24406    & 7.71723e+06 & 35.2 \\
+  Model        & 4 Masters-1 Slave  & 721  & 84118    & 3.17332e+12 & 2818.3 \\
+               & 4 Masters-2 Slaves & 911  & N/A      & N/A         & >1 day \\
  \midrule 
  \midrule
@@ -48,5 +48,5 @@
 \midrule
 \midrule
- Concrete Model                     & 822     & 140586      & 3.7354e+07     & 294.6 \\      
+ Concrete Model                     & 822     & 161730      & 3.7354e+07     & 300.12 \\      
  \midrule 
  \midrule
@@ -75,40 +75,40 @@
 \multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
  	         & Prop. Selection   & 1    &    2.2     \\
- $\phi_1$   & Incremental       & 0    &   18.1        \\
-            & Standard MC       & -    &   14.9     \\
+ $\phi_1$   & Incremental       & 0    &    6.3        \\
+            & Standard MC       & -    &    6.06     \\
 \midrule
 	         & Prop. Selection   & 0    &     1.0     \\
- $\phi_2$   & Incremental       & 467  &   168.0         \\
-	         & Standard MC       & -    &    14.9      \\
+ $\phi_2$   & Incremental       & 562  &   200.9         \\
+	         & Standard MC       & -    &    6.13      \\
 \midrule   
 \midrule
 \multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}}   \\   
  	         & Prop. Selection   & 1    &    2.0     \\
- $\phi_1$   & Incremental       & 0    &  107.7        \\
-            & Standard MC       & -    & 1181.8     \\
+ $\phi_1$   & Incremental       & 0    &   20.4        \\
+            & Standard MC       & -    &   37.9     \\
 \midrule
  	         & Prop. Selection   & 0    &    1.0    \\
- $\phi_2$   & Incremental       & 0    &  108.5       \\
- 	         & Standard MC       & -    & 1103.3   \\
+ $\phi_2$   & Incremental       & 74   &  786.3        \\
+ 	         & Standard MC       & -    &   39.4    \\
 \midrule
 \midrule  
 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}}   \\ 
- 	         & Prop. Selection   & 1    &    2.1     \\
- $\phi_1$   & Incremental       & N/A  & >3 days        \\
-            & Standard MC       & -    & >3 days     \\
+ 	         & Prop. Selection   &  1   &    2.1     \\
+ $\phi_1$   & Incremental       &  0   &  261.6      \\
+            & Standard MC       &  -   &  >1 day     \\
 \midrule
- 	         & Prop. Selection   &  0    &   1.0 \\
- $\phi_2$   & Incremental       &  N/A  &  >3 days   \\
-	         & Standard MC       &  -    & >3 days \\
+ 	         & Prop. Selection   &  0   &   1.0    \\
+ $\phi_2$   & Incremental       &  0   &   263.5     \\
+	         & Standard MC       &  -   &   >1 day   \\
 \midrule 
 \midrule
 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\ 
 				& Prop. Selection   & 1   &  2.2     \\
- $\phi_1$   & Incremental       & N/A &  >3 days    \\
-            & Standard MC       & -   &  >3 days   \\
+ $\phi_1$   & Incremental       & N/A &  >1 day    \\
+            & Standard MC       & -   &  >1 day   \\
 \midrule
             & Prop. Selection   & 0   &  1.1\\
- $\phi_2$   & Incremental       & N/A &  >3 days    \\
-            & Standard MC       & -   &  >3 days\\
+ $\phi_2$   & Incremental       & N/A &  >1 day    \\
+            & Standard MC       & -   &  >1 day\\
 \bottomrule       
 \bottomrule
@@ -132,10 +132,10 @@
 \midrule
  	         & Prop. Selection  &  0          &  1.02     \\
- $\phi_3$   & Incremental      & N/A   		&  N/A \\
- 	         & Standard MC      & -   			&  N/A    \\
+ $\phi_3$   & Incremental      & N/A   		&  >1 day   \\
+ 	         & Standard MC      & -   			&  2645.4    \\
 \midrule
- 	         & Prop. Selection   &  0         &   1.01\\
- $\phi_4$   & Incremental       & N/A        &   N/A     \\
- 	         & Standard MC       & -          &   N/A    \\
+ 	         & Prop. Selection   &  0         &   1.01     \\
+ $\phi_4$   & Incremental       & N/A        &  >1 day    \\
+ 	         & Standard MC       & -          &   1678.1    \\
 \bottomrule
 
@@ -147,8 +147,8 @@
 
 
-In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), incremental\_ctl\_verification (Incremental) and the standard model checking (Standard MC) computed using the \emph{model\_check} command in VIS (Note: Dynamic variable ordering has been enabled with sift method). For the VCI-PI platform, the global property $\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of 42 verifed components properties to be selected in VCI-PI plateform and for the verification of $\phi_1$ we have restrained the selectable properties only to those without AG prefix. In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations.  
+In the following tables: Table \ref{TabVCI_PI} and Table \ref{TabCANBus}, we compare the execution time between our technique (Prop. Selection), \emph{incremental\_ctl\_verification} (Incremental) and the standard model checking (Standard MC) computed using the \emph{model\_check} command in VIS (Note: Dynamic variable ordering has been enabled with sift method). For the VCI-PI platform, the global property $\phi_1$ is the type $AF((p=1)*AF(q=1))$ and $\phi_2$ is actually a stronger version of the same formula with $AG(AF((p=1)*AF(q=1)))$. We have a total of 42 verifed components properties to be selected in VCI-PI plateform and for the verification of $\phi_1$ we have restrained the selectable properties only to those without AG prefix. In comparison to $\phi_2$, we can see that, a better set of properties available will result in a better abstraction and less refinement iterations.  
 
 
-In the case of the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)*AF(r_1=1)) -> AF((s_1=1)*AF(t_1=1)))$ and $\phi_4 = AG(((p'=1)*(q'=1)*AG(r_2=0)) -> AG((s_2=0)*(t_2=0)))$. We have at our disposal 103 verified component properties and after the selection process, 3 selected component properties were sufficient to verify both global properties.
+In the case of the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)*AF(r_1=1)) \rightarrow AF((s_1=1)*AF(t_1=1)))$ and $\phi_4 = AG(((p'=1)*(q'=1)*AG(r_2=0)) \rightarrow AG((s_2=0)*(t_2=0)))$. We have at our disposal 103 verified component properties and after the selection process, 3 selected component properties were sufficient to verify both global properties.
 
 Globally, we can see that our technique systematically computes faster than the other two methods and interestingly in the case where the size of the platform increases by adding the more connected components, in contrary to the other two methods, our computation time remains stable.
