Changeset 92 for papers/FDL2012/ordering_filter_properties.tex

Timestamp:

Apr 6, 2012, 10:37:41 PM (12 years ago)

Author:

syed

Message:

/papers/FDL2012/

File:

• papers/FDL2012/ordering_filter_properties.tex (modified) (5 diffs)

papers/FDL2012/ordering_filter_properties.tex

@@ -27 +27 @@
 whereas variables which do not interfere with a primary variable are weighted 0. 
 Here is how we proceed:
+\vspace*{-5mm}
 \begin{enumerate}
+\itemsep -0.3em
 \item Build the structural dependency graph for all primary variables.
 \item Compute the depth of all variables 
@@ -157 +159 @@
 In order to reach this objective, a Abstract Kripke structure of the counterexample $\sigma$, $K(\sigma)$
 is generated. $K(\sigma)$ is a succession of states corresponding to the counterexample path which dissatisfies 
-the global property~$\Phi$ 
+the global property~$\Phi$. 
 %as show in figure \ref{AKSNegCex}. 
 %In case where the spurious counter-example exhibits a bounded path, we add a last
@@ -181 +183 @@
 R_{\sigma},F_{\sigma})$
 such that:
-
+\vspace*{-2mm}
 \begin{itemize}
+%\parsep=2pt
+%\topsep 0pt
+\itemsep -0.3em
 \item $AP_{\sigma} = \widehat{AP}_i$ : a finite set of atomic propositions which corresponds to the variables in the abstract model     
 \item $S_{\sigma} = \{s_{i}|s_i\in \sigma\}\cup\{s_T\}$
@@ -252 +257 @@
 
 \begin{property}{Counterexample eviction}
+\vspace*{-2mm}
 \begin{enumerate}
+\itemsep -0.3em
 \item If {\textbf{$K(\sigma) \vDash \varphi  \Rightarrow AKS(\varphi) $ will
 not eliminate $\sigma$}}.
@@ -272 +279 @@
 \end{proof}
 
+\vspace*{-2mm}
 The proposed approach ensures that the refinement excludes the counterexample
 and  respects the definition \ref{def:goodrefinement}.