Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav07_lecture_18 [2007/05/28 21:33] vasu.singh |
sav07_lecture_18 [2007/05/28 22:22] vasu.singh |
||
---|---|---|---|
Line 27: | Line 27: | ||
This suggests that the two programs above are not equivalent for the purpose of reasoning | This suggests that the two programs above are not equivalent for the purpose of reasoning | ||
in concurrently executing programs. | in concurrently executing programs. | ||
+ | |||
Line 58: | Line 59: | ||
$I(S_1,S_2) = \{S_1^1, S_2^1, \ldots, S_1^n, S_2^n \mid S_1 = S_1^1 S_1^2 \ldots S_1^n$ and $S_2 = S_2^1 S_2^2 \ldots S_2^n \}$. | $I(S_1,S_2) = \{S_1^1, S_2^1, \ldots, S_1^n, S_2^n \mid S_1 = S_1^1 S_1^2 \ldots S_1^n$ and $S_2 = S_2^1 S_2^2 \ldots S_2^n \}$. | ||
- | $[[ C^* ]] = \cup_{n \ge 0} [[C^n]]$ where $[[C^0]] = \emptyset$. | + | $[[ C^* ]] = \cup_{n \ge 0} [[C^n]]$ where $[[C^0]] = \emptyset$ and $[[C^{n+1}]] = [[ C^n ; C]]$. |
- | $[[ \atomic(C) ]] = \eval([[C]])$. | + | $[[ $atomic$(C) ]] = $eval$([[C]])$ where eval is a function $eval: R* \rightarrow R$ such that |
+ | eval$(\{r_1^1 \ldots r_{n1}^1, r_1^2 \ldots r_{n2}^2, \ldots, r_1^k \ldots r_{nk}^k \}) = (r_1^1 \circ r_1^2 \ldots \circ r_{n1}^1) \cup \ldots \cup (r_1^k \circ | ||
+ | r_2^k \ldots \circ r_{nk}^k)$. | ||
==== Global reachability invariants ==== | ==== Global reachability invariants ==== |