Changeset 75 for papers/FDL2012/exp_results.tex

Timestamp:

Mar 27, 2012, 5:24:35 PM (13 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

• papers/FDL2012/exp_results.tex (modified) (4 diffs)

papers/FDL2012/exp_results.tex

@@ -21 +21 @@
  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 \\
+ for $\phi_1$  & 4 Masters-2 Slaves & 589 & 2   & 167   &  7.08355e+21  & 0.04 \\
 \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 \\ 
+ for $\phi_2$  & 4 Masters-2 Slaves & 586 & 1   & 141   &  3.68935e+21  & 0.02 \\ 
 \bottomrule  
 \bottomrule
@@ -99 +99 @@
 \midrule
 \multicolumn{4}{l}{\textbf{\underline{4 Masters - 2 Slaves :}}}  \\ 
-                                & Prop. Selection   & 1   &  xxx     \\
- $\phi_1$   & Incremental       & xxx &  xxx         \\
+                                & Prop. Selection   & 1   &  2.2     \\
+ $\phi_1$   & Incremental       & N/A &  >1 day    \\
             & Standard MC       & -   &  2231.3    \\
 \midrule
-            & Prop. Selection   & 0   &  xxx\\
+            & Prop. Selection   & 0   &  1.1\\
  $\phi_2$   & Incremental       & N/A &  >1 day    \\
             & Standard MC       & -   &  12814.1 \\
@@ -115 +115 @@
 
 %\medskip
-
-
-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))$ whereas for the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)) -> AF((s = 1)*(r = 1))$ and $\phi_4 = AG(((p'=1)*(q'=1)) -> AG(r' = 0))$. 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.
 
 
@@ -143 +140 @@
 \end{table}
 
-\medskip
 
 
+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)))$ whereas for the CAN bus platform, the global property $\phi_3$ is the type $AG(((p'=1)*(q'=1)) -> AF((s = 1)*(r = 1))$ and $\phi_4 = AG(((p'=1)*(q'=1)) -> AG(r' = 0))$. 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.
+
+
+
+%\medskip
+
+