Changeset 79 for papers/FDL2012/abstraction_refinement.tex

Timestamp:

Mar 30, 2012, 5:02:20 PM (13 years ago)

Author:

cecile

Message:

correction counter-example and its negation representation

File:

• papers/FDL2012/abstraction_refinement.tex (modified) (2 diffs)

papers/FDL2012/abstraction_refinement.tex

@@ -30 +30 @@
 
 The counterexample at a refinement step $i$, $\sigma$, is a path in the
-abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the counterexample given by the model-checker, the variable configuration in each state is boolean.
+abstract model $\widehat{M}_i$ which dissatisfies $\Phi$.  In the
+counterexample given by the model-checker, the variable configuration in each
+state is boolean. We name $\check{L_i}$ this new labeling.
 The spurious counterexample $\sigma$ is defined such that :
 \begin{definition}
 Let $\sigma$ be a \emph{counter-example} in $\widehat{M}_i =\langle \widehat{AP}_i, \widehat{S}_i, \widehat{S}_{0i},
-\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length$|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
+\widehat{L}_i, \widehat{R}_i, \widehat{F}_i \rangle$ of  length $|\sigma| = n$: $ \sigma = s_{0} \rightarrow s_{1} \ldots
 \rightarrow s_{n}$ with $(s_{k}, s_{k+1}) \in \widehat{R}_i$ $\forall k \in [0..n-1]$.
 \begin{itemize}
 \item All its variables are concrete: $\forall s_i$ and $\forall p\in
-\widehat{AP}_i$, $p$ is either true or false
+\widehat{AP}_i$, $p$ is either true or false according to $\check{L_i}$.
 (not {\it unknown}), and $s_0 $ is an initial state of the concrete system: $s_0 \in \mathbf{R}_0$
 \item  $\sigma$ is a counterexample in  $\widehat{M}_i$: $s_0\not\models \Phi$.
@@ -45 +47 @@
 \end{itemize}
 \end{definition}
-
+In the following we denote by 
 The construction of the AKS representing all executions except the one described by the spurious counter-example is done in two steps.
 \subsubsection{step 1 : Build the structure of the AKS.}
-Let us denote $AKS(\overline{\sigma})$ this AKS. $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
-\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}}, \widehat{F}_{\overline{\sigma}} \rangle$.
+
+\begin{definition}
+Let $\sigma$ be a counter-example of  length $|\sigma| = n$, the \emph{ AKS of the
+counter-example negation} $AKS(\overline{\sigma}) = \langle \widehat{AP}_{\overline{\sigma}}, \widehat{S}_{\overline{\sigma}}, \widehat{S}_{0{\overline{\sigma}}},
+\widehat{L}_{\overline{\sigma}}, \widehat{R}_{\overline{\sigma}},
+\widehat{F}_{\overline{\sigma}} \rangle$ is such that :
 \begin{itemize}
-\item The set of atomic propositions coincides with the one of $\sigma$ : $AP_{\overline{\sigma}} = {AP}_i$
-\item Build a state $s_T$, and for each state $s_i$ in $\sigma$, build two states $s'_i$ and $s"_i$.  $s_T \in S_{\overline{\sigma}}$ and forall $i$ in $[0..n-1]$ : $s'_i \in S_{\overline{\sigma}}$ and $s"_i \in S_{\overline{\sigma}}.$
-\item State labeling : $s'_i$ represents the (concrete) configuration of state $s_i$ and state $s"_i$  represents all configurations but the one of $s_i$. This last set may not be representable by the labeling function defined in def \ref{def-aks}. State labeling is treated in the second step.
-\item States $s'_0$ and $s"_0$ are initial states.
-\item Transitions : Forall $i$ in $[1..n-1]$, connect $s'_i$ and $s"_i$ to their predecessor state $s'_{i-1}$: $(s'_{i-1},s'_i) \in R_{\overline{\sigma}}$ and $(s'_{i-1},s"_i) \in R_{\overline{\sigma}}$ and connect all $s"$ states as predecessor of the $s_T$ state : $(s"_i,s_T) \in R_{\overline{\sigma}}$.
-\item \TODO{FAIRNESS}
+\item $AP_{\overline{\sigma}} = {AP}_i$:
+The set of atomic propositions coincides with the one of $\sigma$
+\item $\widehat{S}_{\overline{\sigma}}$: $\{s_T\} \cup \{s_{i}'|\forall i`in
+[0..n-2] \vee s_i\in
+\sigma\}\cup \{\bar{s_{i}}|\forall i in [0..n-1] \vee s_i\in \sigma\}$
+\item $\widehat{L}_{\overline{\sigma}}$ is such that $s_i'$ represents the
+(concrete) configuration of state $s_i$ and state $\bar{s_i}$  represents all
+configurations but the one of $s_i$. This last set may not be representable by
+the labeling function defined in def \ref{def-aks}. State labeling is treated
+in the second step. $s_t$ is a state where all atomic propositions are {\it unknown}.
+
+\item $\widehat{S}_{0{\overline{\sigma}}} = \{ s_0',\bar{s_0}\}$
+\item $\widehat{R}_{\overline{\sigma}} = \{(\bar{s_i},s_T), \forall i\in
+[0..n-1]\} \cup \{(s_i',\bar{s_{i+1}}), \forall i\in[0..n-2]\} \cup
+\{(s_i',s_{i+1}',\forall  i\in[0..n-3]\}$
+
+\item $\widehat{F}_{\overline{\sigma}} = \emptyset$
 \end{itemize}
+\end{definition}
 The size of this structure is linear with the size of the counter-example, however it is not a strict AKS since the representation of the set of configurations in states $s"$ may lead to a union of labels.