Index: papers/FDL2012/exp_results.tex
===================================================================
--- papers/FDL2012/exp_results.tex	(revision 89)
+++ papers/FDL2012/exp_results.tex	(revision 92)
@@ -1,9 +1,9 @@
 We have conducted preliminary experiments to test and compare the performance
-of our strategy with existing abstraction-refinement techniques available in
+of our strategy with existing techniques available in
 VIS. There are several abstraction-refinement techniques implemented in VIS
 accessible via \emph{approximate\_model\_check},
 \emph{iterative\_model\_check}, \emph{check\_invariant} and
-\emph{incremental\_ctl\_model\_check} commands. However, among the available
-techniques, \emph{incremental\_ctl\_model\_check} is the only one that supports CTL formulas and fairness constraints which are necessary in our test platforms. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}.
+\emph{incremental\_ctl\_verification} commands. However, among the available
+techniques, \emph{incremental\_ctl\_verification} is the only one that supports CTL formulas and fairness constraints which are necessary in our test platforms. It is an automatic abstraction refinement algorithm which generates an initial conservative abstraction principally by reducing the size of the latches by a constant factor. If the initial abstraction is not conclusive, a \emph{goal set} will then be computed in order to guide the refinement process \cite{PardoHachtel98incremCTLMC} \cite{PardoHachtel97autoAbsMC}.
 
 
@@ -18,5 +18,5 @@
 \toprule 
 \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)} \\
+\multicolumn{3}{l}{\textbf{Platform}}     &\emph{BDD Variables}   & \emph{Size} & \emph{Reachable States} & \emph{Time (s)} \\
 \midrule
 \midrule
@@ -24,5 +24,5 @@
 			& 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 \\
+			&               & 4 Masters-2 Slaves & 895  & 238990   & 5.708e+15   & 68882.3\footnotemark[1] \\
 \cline{2-7} 
 \cline{2-7}
@@ -36,7 +36,7 @@
 			& 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 
  \midrule
- 			&\multicolumn{2}{c}{Concrete Model}  					 & 822     & 161730      & 3.7354e+07     & 300.12 \\      
+ 			&\multicolumn{2}{c}{Concrete Model}  					     & 822     & 161730      & 3.7354e+07     & 300.12 \\      
 \cline{2-7}
 \cline{2-7}
@@ -45,5 +45,6 @@
  			&\multicolumn{2}{c}{Final Abstract Model for $\phi_4$}  & 425   & 187   &  1.66005e+12       & 0.04 \\
 \bottomrule  
-\bottomrule
+%\bottomrule
+
 \end{tabular}
 
@@ -51,4 +52,5 @@
 \end{table*}
 
+%\footnotetext[1]{Computed on a calculation server.}
 
 
@@ -72,5 +74,5 @@
 				&	          & Standard MC       & -    &    6.13      \\
 \midrule   
-\midrule
+%\midrule
 				& 	          & Prop. Select.   & 1    &    2.0     \\
 VCI-PI: 		& $\phi_1$   & Incremental       & 0    &   20.4        \\
@@ -81,5 +83,5 @@
 				& 	          & Standard MC       & -    &   39.4    \\
 \midrule
-\midrule  
+%\midrule  
 
 				& 	          & Prop. Select.   &  1   &    2.1     \\
@@ -91,5 +93,5 @@
 				&	          & Standard MC       &  -   &   >1 day   \\
 \midrule 
-\midrule
+%\midrule
 
 				&				 & Prop. Select.   & 1   	&  2.2     \\
@@ -101,5 +103,5 @@
 				&            & Standard MC       & -   	&  >1 day\\
 \midrule 
-\midrule
+%\midrule
       		&	          & Prop. Select.   &  0     &  1.02     \\
  				&$\phi_3$    & Incremental       & N/A    &  >1 day   \\
@@ -111,5 +113,5 @@
 
 \bottomrule       
-\bottomrule
+%\bottomrule
 
 \end{tabular}
@@ -117,6 +119,4 @@
 \caption{\label{TabVerif} Verification Results  }
 \end{table}
-
-
 
 
@@ -128,5 +128,5 @@
 $\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
-27 verifed components properties to be selected in VCI-PI plateform.
+26 verifed components properties to be selected in VCI-PI plateform.
 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.  
 
