equal
deleted
inserted
replaced
5 |
5 |
6 Deadlock examples from section 5.6 of |
6 Deadlock examples from section 5.6 of |
7 Misra, "A Logic for Concurrent Programming", 1994 |
7 Misra, "A Logic for Concurrent Programming", 1994 |
8 *) |
8 *) |
9 |
9 |
10 theory Deadlock = UNITY: |
10 theory Deadlock imports UNITY begin |
11 |
11 |
12 (*Trivial, two-process case*) |
12 (*Trivial, two-process case*) |
13 lemma "[| F \<in> (A \<inter> B) co A; F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> B)" |
13 lemma "[| F \<in> (A \<inter> B) co A; F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> B)" |
14 by (unfold constrains_def stable_def, blast) |
14 by (unfold constrains_def stable_def, blast) |
15 |
15 |