Index: papers/FDL2012/exp_results.tex
===================================================================
--- papers/FDL2012/exp_results.tex	(revision 66)
+++ papers/FDL2012/exp_results.tex	(revision 71)
@@ -1,9 +1,62 @@
 We have conducted preliminary experiments to tests and compare the performance of our strategy with existing abstraction-refinement technique available in VIS. As our abstraction representation requires fairness constraints, we have chosen the \emph{incremental\_ctl\_verification} abstraction refinement technique as it supports CTL formulas and fairness constraints \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}. 
-
 
 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 and a CAN bus. The results have been obtained on a PC with an AMD Athlon dual-core processor 4450e and 1.8GB of RAM memory.
 
 
-\medskip
+\begin{table*} [ht]
+\hspace*{10mm}
+\begin{tabular}{clccccc}
+
+\toprule 
+\multicolumn{2}{c}{\textbf{VCI-PI}}   & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
+\multicolumn{2}{c}{\textbf{Platform}} &\emph{BDD Variables}  & \emph{Depth}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
+\midrule
+\midrule
+               & 1 Master-1 Slave   & 308 & 599 & 33 442   & 3.64116e+06 & 41.49 \\
+ Concrete      & 2 Masters-1 Slave  & 439 & 186 & 75 210   & 73282       & 14.36 \\
+  Model        & 4 Masters-1 Slave  & 709 & 408 & 156 657  & 2.15076e+07 & 414.38 \\
+               & 4 Masters-2 Slaves & 883 & 597 & 217 797  & 3.22215e+10 & 4064.09 \\
+ \midrule 
+ \midrule
+ Final         & 1 Master-1 Slave   & 197 & 2   &  76   &  5.03316e+07  & 0.01 \\
+ Abstract      & 2 Masters-1 Slave  & 301 & 2   &  99   &  4.12317e+11  & 0.02 \\
+ Model         & 4 Masters-1 Slave  & 501 & 2   & 147   &  3.45876e+18  & 0.03\\
+ for $\phi_1$  & 4 Masters-2 Slaves & xx  & 2   & xxx   &  xxx          & xxxx \\
+\midrule 
+ Final         & 1 Master-1 Slave   & 194 & 1   & 50    &  2.62144e+07  & 0 \\
+ Abstract      & 2 Masters-1 Slave  & 298 & 1   & 73    &  2.14748e+11  & 0.01 \\
+ Model         & 4 Masters-1 Slave  & 498 & 1   & 121   &  1.80144e+18  & 0.02 \\
+ for $\phi_2$  & 4 Masters-2 Slaves & xxx & x   & xxx   &  xxx          & xxx \\ 
+\bottomrule  
+\bottomrule
+\end{tabular}
+ 
+\caption{\label{StatsVCI_PI} Statistics on the VCI-PI platform}
+\end{table*}
+%\medskip
+
+
+\begin{table*} [ht]
+\hspace*{12mm}
+\begin{tabular}{cccccc}
+
+\toprule 
+\textbf{CAN Bus}      & \emph{Number of}      & \emph{FSM}    & \emph{BDD}  & \emph{Number of }       & \emph{Analysis}\\ 
+\textbf{Platform}     &\emph{BDD Variables}  & \emph{Depth}  & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
+\midrule
+\midrule
+ Concrete Model   & 838     & 182     & 212550    & 2.87296e+08      & 167.9 \\      
+ \midrule 
+ \midrule
+ Final Abstract Model for $\phi_1$  & xx  & 2   & xxx   &  xxx       & xxxx \\
+\midrule 
+ Final Abstract Model for $\phi_2$  & xx  & 2   & xxx   &  xxx       & xxxx \\
+\bottomrule  
+\bottomrule
+\end{tabular}
+ 
+\caption{\label{StatsCAN_Bus} Statistics on the CAN Bus platform}
+\end{table*}
+
 
 \begin{table} [h]
@@ -12,20 +65,52 @@
 
 \toprule 
-\textbf{VCI} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\ 
- \textbf{-PI}& \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
+\emph{Global}   &\emph{Verification} & \emph{Refinement}  & \emph{Verif.}  \\
+\emph{Property} & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}      \\ 
 \midrule
 \midrule
- 	     & Prop. Selection &    2.2    & 1 \\
- $\phi_1$   & Incremental      &  18.1    & 0    \\
- 	     & Standard MC    &  14.9    & - \\
+\multicolumn{4}{l}{\textbf{\underline{1 Master - 1 Slave :}}} \\
+ 	         & Prop. Selection   & 1    &    2.2     \\
+ $\phi_1$   & Incremental       & 0    &   18.1        \\
+            & Standard MC       & -    &   14.9     \\
 \midrule
- 	     & Prop\_Selection &     1.0    & 0 \\
- $\phi_2$   & Incremental      & 168.0    & 467    \\
- 	     & Standard MC    &   14.9    & - \\
+	         & Prop. Selection   & 0    &     1.0     \\
+ $\phi_2$   & Incremental       & 467  &   168.0         \\
+	         & Standard MC       & -    &    14.9      \\
+\midrule   
+\midrule
+\multicolumn{4}{l}{\textbf{\underline{2 Masters - 1 Slave :}}}   \\   
+ 	         & Prop. Selection   & 1    &    2.0     \\
+ $\phi_1$   & Incremental       & 0    &    1.3        \\
+            & Standard MC       & -    &    1.5     \\
+\midrule
+ 	         & Prop. Selection   & 0    &    1.0    \\
+ $\phi_2$   & Incremental       & 0    &   15.3       \\
+ 	         & Standard MC       & -    &   14.6    \\
+\midrule
+\midrule  
+\multicolumn{4}{l}{\textbf{\underline{4 Masters - 1 Slave :}}}   \\ 
+ 	         & Prop. Selection   & 1    &    2.1     \\
+ $\phi_1$   & Incremental       & 0    &    6.8        \\
+            & Standard MC       & -    &  175.5     \\
+\midrule
+ 	         & Prop. Selection   &  0    &   1.0 \\
+ $\phi_2$   & Incremental       &  0    &   7.5    \\
+	         & Standard MC       &  -    & 195.1 \\
+\midrule 
+\midrule
+\multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\ 
+				& Prop. Selection   & 1   &  xxx     \\
+ $\phi_1$   & Incremental       & xxx &  xxx         \\
+            & Standard MC       & -   &  2231.3    \\
+\midrule
+            & Prop. Selection   & 0   &  xxx\\
+ $\phi_2$   & Incremental       & N/A &  >1 day    \\
+            & Standard MC       & -   &  12814.1 \\
+\bottomrule       
 \bottomrule
 
 \end{tabular}
  
-\caption{\label{TabVCI_PI} Results on VCI-PI platform }
+\caption{\label{TabVCI_PI} Results on the VCI-PI platform }
 \end{table}
 
@@ -34,23 +119,23 @@
 \begin{table} [h]
 %\hspace*{-8mm}
-\begin{tabular}{cccc}
+\begin{tabular}{lcccc}
 
 \toprule 
-\textbf{CAN} & \emph{Verification} & \emph{Verification}  & \emph{Refinement} \\ 
-\textbf{Bus}  & \emph{Technique}  & \emph{Time (s)}       & \emph{Iteration} \\
+\emph{Global}  & \emph{Verification} & \emph{Refinement} & \emph{Verif.}   \\ 
+\emph{Property}  & \emph{Technique}  & \emph{Iteration}  & \emph{Time (s)}       \\
 \midrule
 \midrule
- 	      & Prop. Selection  &             &       \\
- $\phi_1$   & Incremental       &  >1 day  & 0    \\
- 	      & Standard MC     &  51.9    & - \\
+ 	         & Prop. Selection  &  xxx        &  xxx     \\
+ $\phi_3$   & Incremental      & N/A   		&  >1 day \\
+ 	         & Standard MC      & -   			&  51.9    \\
 \midrule
- 	     & Prop\_Selection &              &   \\
- $\phi_2$   & Incremental      &   57.3    & 0   \\
- 	     & Standard MC     &     2.2    & - \\
+ 	         & Prop. Selection   &  xxx       &  xxx \\
+ $\phi_4$   & Incremental       & 0          &   57.3     \\
+ 	         & Standard MC       & -          &    2.2    \\
 \bottomrule
 
 \end{tabular}
  
-\caption{\label{TabCANBus} Results on CAN Bus platform }
+\caption{\label{TabCANBus} Results on the CAN Bus platform }
 \end{table}
 
