equal
deleted
inserted
replaced
14 text\<open>From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.\<close> |
14 text\<open>From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.\<close> |
15 |
15 |
16 subsection\<open>Definitions\<close> |
16 subsection\<open>Definitions\<close> |
17 |
17 |
18 datatype pstate = Hungry | Eating | Thinking |
18 datatype pstate = Hungry | Eating | Thinking |
19 \<comment>\<open>process states\<close> |
19 \<comment> \<open>process states\<close> |
20 |
20 |
21 record state = |
21 record state = |
22 token :: "nat" |
22 token :: "nat" |
23 proc :: "nat => pstate" |
23 proc :: "nat => pstate" |
24 |
24 |