# Diferencias

Muestra las diferencias entre dos versiones de la página.

Enlace a la vista de comparación

grupos:avispa:operational_semantics_of_tcc [2009/11/12 19:27]
caolarte
grupos:avispa:operational_semantics_of_tcc [2011/01/24 15:30] (actual)
Línea 1: Línea 1:
+====== Operational Semantics of tcc ======

+The following table summarizes the internal and observable transition relations for tcc.
+
+{{ :grupos:avispa:sos.png |}}
+
+Let us describe  the internal reduction rules:
+
+   * The rule **RTell** says that the process **tell**( c ) adds c to the current store d, via conjunction, and evolves into **skip**.
+   * The rule **RPar** is the standard interleaving rule for parallel composition.
+   * Let Q = **local** (x;c) P  in Rule **RLoc**. The global store is d and the local store is c.   We distinguish between the //external// (corresponding to Q) and the //internal// point of view (corresponding to P).  From the internal point of view, the information about  the variable x, possibly appearing in the global store d , cannot be observed. Thus, before reducing  P we first hide the information about x  that  Q  may have in d  by existentially quantifying  x   in   d. Similarly, from the external point of view, the observable information about x that the reduction of internal agent P may produce (i.e.,  c')  cannot be observed. Thus we hide it by existentially quantifying x in c' before adding it to the global store. Additionally, we  make c' the new private store of the evolution of the internal process.
+  * Since the process P=**unless** c **next** Q executes Q in the next time unit only if  the final store at the current time unit  does not entail c, in the rule **RUnl** P evolves into **skip** if the current store d entails c.
+  *  Rule **RRep**  dictates that the process !P produces a copy of P at the current  time unit, and then persists in the next time unit.
+  *  Rule **RAsk**  describes the behavior of P=**when** c **do** Q. If the current store d entails c, then the process Q is executed.
+  *  Let ≡ be the smallest congruence satisfying:
+    -  P ≡ Q if  P and Q  differ only by a renaming of bound variables (alpha-conversion).
+    -  P || **skip** ≡ P.
+    - P || Q ≡ Q || P.
+    -  P ||  (Q || R) ≡ (P || Q) || R.
+    If P≡Q and c is logically equivalent to d, we say that <P,c>≡<Q,d>. Rule **RStr** says that structurally congruent configurations have the same reductions.
+
+
+The seemingly missing rules for the  processes **next** P and **unless** c **next** P (when c cannot be entailed from the current store)  are given by the rule **RObs**. This rule says that an observable transition from P labeled with  (c,d) is obtained from a terminating sequence of internal transitions of the form <P,c>→ <sup>*</sup><Q,d>. The process R to be executed in the next time interval is equivalent to  F(Q) (the "future" of Q). The process F(Q)  is obtained by removing from Q  any local information that has been stored in Q, and  by
+"unfolding" the sub-terms within **next** and **unless** expressions.  More precisely:
+  - F(**skip**) = **skip**
+  - F(**next** P) = P
+  - F(**unless** c **next** P) = P
+  - F(P1 || P2) = F(P1) || F(P2)
+  - F( (**local** x;c)P ) = (**local** x;true) P