Index: papers/FDL2012/exp_results.tex
===================================================================
--- papers/FDL2012/exp_results.tex	(revision 83)
+++ papers/FDL2012/exp_results.tex	(revision 88)
@@ -2,63 +2,46 @@
 
 
-We have executed and compared the execution time and the number of refinement iterations for two examples: VCI-PI platform consisting of Virtual Component Interface (VCI), a PI-Bus and VCI-PI protocol converter and a simplified version of a CAN bus platform consisting of 3 nodes on a CAN bus. Table \ref{StatsVCI_PI} and Table \ref{StatsCAN_Bus} give the size and the statistics concerning the VCI-PI platform and CAN bus platform respectively. All the values are obtained using the \emph{compute\_reach} command with option \emph{-v 1} in VIS except the number of BDD variables, computed using the \emph{print\_bdd\_stats} command. The experiments have been executed on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory. 
-
-
-\begin{table*} [ht]
-\hspace*{17mm}
-\begin{tabular}{clcccc}
-
-\toprule 
-\multicolumn{2}{c}{\textbf{VCI-PI}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
-\multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
-\midrule
-\midrule
-               & 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
- Final         & 1 Master-1 Slave   & 197  &  76   &  5.03316e+07  & 0.01 \\
- Abstract      & 2 Masters-1 Slave  & 301  &  99   &  4.12317e+11  & 0.02 \\
- Model         & 4 Masters-1 Slave  & 501  & 147   &  3.45876e+18  & 0.03\\
- for $\phi_1$  & 4 Masters-2 Slaves & 589  & 167   &  7.08355e+21  & 0.04 \\
-\midrule 
- Final         & 1 Master-1 Slave   & 194  & 50    &  2.62144e+07  & 0 \\
- Abstract      & 2 Masters-1 Slave  & 298  & 73    &  2.14748e+11  & 0.01 \\
- Model         & 4 Masters-1 Slave  & 498  & 121   &  1.80144e+18  & 0.02 \\
- for $\phi_2$  & 4 Masters-2 Slaves & 586  & 141   &  3.68935e+21  & 0.02 \\ 
-\bottomrule  
-\bottomrule
-\end{tabular}
- 
-\caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform}
-\end{table*}
-%\medskip
-
+We have executed and compared the execution time and the number of refinement iterations for two examples: VCI-PI platform consisting of Virtual Component Interface (VCI), a PI-Bus and VCI-PI protocol converter and a simplified version of a CAN bus platform consisting of 3 nodes on a CAN bus. Table \ref{StatsPlatform} gives the size and the statistics concerning the VCI-PI platform and CAN bus platform verified. All the values are obtained using the \emph{compute\_reach} command with option \emph{-v 1} in VIS except the number of BDD variables, computed using the \emph{print\_bdd\_stats} command. The experiments have been executed on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory. 
 
 
 \begin{table*} [ht]
 \hspace*{15mm}
-\begin{tabular}{ccccc}
+\small
+\begin{tabular}{cclcccc}
 
 \toprule 
-\textbf{CAN Bus}      & \emph{Number of}       & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
-\textbf{Platform}     &\emph{BDD Variables}    & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
+\multicolumn{3}{l}{\textbf{Experiment}}   & \emph{Number of}      & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
+\multicolumn{3}{l}{\textbf{Platform}} &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
 \midrule
 \midrule
- Concrete Model                     & 822     & 161730      & 3.7354e+07     & 300.12 \\      
+			&               & 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 \\
+\cline{2-7} 
+\cline{2-7}
+			& Final         & 1 Master-1 Slave   & 197  &  76   &  5.03316e+07  & 0.01 \\
+VCI-PI	& Abstract      & 2 Masters-1 Slave  & 301  &  99   &  4.12317e+11  & 0.02 \\
+			& Model         & 4 Masters-1 Slave  & 501  & 147   &  3.45876e+18  & 0.03\\
+			& for $\phi_1$  & 4 Masters-2 Slaves & 589  & 167   &  7.08355e+21  & 0.04 \\
+\cline{2-7}
+			& Final         & 1 Master-1 Slave   & 194  & 50    &  2.62144e+07  & 0 \\
+			& Abstract      & 2 Masters-1 Slave  & 298  & 73    &  2.14748e+11  & 0.01 \\
+			& Model         & 4 Masters-1 Slave  & 498  & 121   &  1.80144e+18  & 0.02 \\
+			& for $\phi_2$  & 4 Masters-2 Slaves & 586  & 141   &  3.68935e+21  & 0.02 \\ 
  \midrule 
  \midrule
- Final Abstract Model for $\phi_1$  & 425   & 187   &  1.66005e+12       & 0.03 \\
-\midrule 
- Final Abstract Model for $\phi_2$  & 425   & 187   &  1.66005e+12       & 0.04 \\
+ 			&\multicolumn{2}{c}{Concrete Model}  					 & 822     & 161730      & 3.7354e+07     & 300.12 \\      
+\cline{2-7}
+\cline{2-7}
+CAN Bus  &\multicolumn{2}{c}{Final Abstract Model for $\phi_3$}  & 425   & 187   &  1.66005e+12       & 0.03 \\
+\cline{2-7}
+ 			&\multicolumn{2}{c}{Final Abstract Model for $\phi_4$}  & 425   & 187   &  1.66005e+12       & 0.04 \\
 \bottomrule  
 \bottomrule
 \end{tabular}
- 
-\caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform}
+
+\caption{\label{StatsPlatform} Statistics on the VCI-PI and CAN Bus platform}
 \end{table*}
-
 
 
@@ -66,86 +49,71 @@
 \begin{table} [h]
 %\hspace*{-8mm}
-\begin{tabular}{cccc}
-
+\small
+\addtolength{\tabcolsep}{-1pt}
+\begin{tabular}{ccccc}
 \toprule 
-\emph{Global}   &\emph{Verification} & \emph{Refinement}  & \emph{Verif.}  \\
-\emph{Property} & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}      \\ 
+\emph{Experim.}     &\emph{Global}   &\emph{Verification} & \emph{Refine.}  & \emph{Verif.}  \\
+\emph{Platform}		&\emph{Property} & \emph{Technique}  & \emph{Iter.}  & \emph{Time (s)}      \\ 
 \midrule
 \midrule
-\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
- 	         & Prop. Selection   & 1    &    2.2     \\
- $\phi_1$   & Incremental       & 0    &    6.3        \\
-            & Standard MC       & -    &    6.06     \\
-\midrule
-	         & Prop. Selection   & 0    &     1.0     \\
- $\phi_2$   & Incremental       & 562  &   200.9         \\
-	         & Standard MC       & -    &    6.13      \\
+%\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
+				& 	          & Prop. Select.   & 1    &    2.2     \\
+VCI-PI:  	& $\phi_1$   & Incremental       & 0    &    6.3        \\
+1 Master		&            & Standard MC       & -    &    6.06     \\
+\cline{2-5}
+-				&	          & Prop. Select.   & 0    &     1.0     \\
+1 Slave		& $\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    &   20.4        \\
-            & Standard MC       & -    &   37.9     \\
-\midrule
- 	         & Prop. Selection   & 0    &    1.0    \\
- $\phi_2$   & Incremental       & 74   &  786.3        \\
- 	         & Standard MC       & -    &   39.4    \\
+				& 	          & Prop. Select.   & 1    &    2.0     \\
+VCI-PI: 		& $\phi_1$   & Incremental       & 0    &   20.4        \\
+2 Masters	&            & Standard MC       & -    &   37.9     \\
+\cline{2-5}
+- 				& 	          & Prop. Select.   & 0    &    1.0    \\
+1 Slave		& $\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       &  0   &  261.6      \\
-            & Standard MC       &  -   &  >1 day     \\
-\midrule
- 	         & Prop. Selection   &  0   &   1.0    \\
- $\phi_2$   & Incremental       &  0   &   263.5     \\
-	         & Standard MC       &  -   &   >1 day   \\
+
+				& 	          & Prop. Select.   &  1   &    2.1     \\
+VCI-PI:  	& $\phi_1$   & Incremental       &  0   &  261.6      \\
+4 Masters	&            & Standard MC       &  -   &  >1 day     \\
+\cline{2-5}
+-  		   & 	          & Prop. Select.   &  0   &   1.0    \\
+1 Slave		& $\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 &  >1 day    \\
-            & Standard MC       & -   &  >1 day   \\
+
+				&				 & Prop. Select.   & 1   	&  2.2     \\
+VCI-PI:     & $\phi_1$   & Incremental       & N/A 	&  >1 day    \\
+4 Masters	&            & Standard MC       & -   	&  >1 day   \\
+\cline{2-5}
+  - 		   &            & Prop. Select.   & 0   	&  1.1\\
+2 Slaves		& $\phi_2$   & Incremental       & N/A 	&  >1 day    \\
+				&            & Standard MC       & -   	&  >1 day\\
+\midrule 
 \midrule
-            & Prop. Selection   & 0   &  1.1\\
- $\phi_2$   & Incremental       & N/A &  >1 day    \\
-            & Standard MC       & -   &  >1 day\\
+      		&	          & Prop. Select.   &  0     &  1.02     \\
+ 				&$\phi_3$    & Incremental       & N/A    &  >1 day   \\
+CAN 			&	          & Standard MC       & -   	&  2645.4    \\
+\cline{2-5}
+Bus  			&	          & Prop. Select.   &  0     &   1.01     \\
+ 				&$\phi_4$    & Incremental       & N/A    &  >1 day    \\
+ 				&	          & Standard MC       & -      &   1678.1    \\    
+
 \bottomrule       
 \bottomrule
 
 \end{tabular}
- 
-\caption{\label{TabVCI_PI} Results on the VCI-PI platform }
-\end{table}
 
-%\medskip
-
-
-\begin{table} [h]
-%\hspace*{-8mm}
-\begin{tabular}{lcccc}
-
-\toprule 
-\emph{Global}  & \emph{Verification} & \emph{Refinement} & \emph{Verif.}   \\ 
-\emph{Property}  & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}       \\
-\midrule
-\midrule
- 	         & Prop. Selection  &  0          &  1.02     \\
- $\phi_3$   & Incremental      & N/A   		&  >1 day   \\
- 	         & Standard MC      & -   			&  2645.4    \\
-\midrule
- 	         & Prop. Selection   &  0         &   1.01     \\
- $\phi_4$   & Incremental       & N/A        &  >1 day    \\
- 	         & Standard MC       & -          &   1678.1    \\
-\bottomrule
-
-\end{tabular}
- 
-\caption{\label{TabCANBus} Results on the CAN Bus platform }
+\caption{\label{TabVerif} Verification Results  }
 \end{table}
 
 
 
-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 Table \ref{TabVerif}, we compare the execution time between our technique (Prop. Select.), \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.  
 
 
