35 Exit thread | -- {* Thread @{text "thread"} finishing its execution. *} |
35 Exit thread | -- {* Thread @{text "thread"} finishing its execution. *} |
36 P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *} |
36 P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *} |
37 V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} |
37 V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} |
38 Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} |
38 Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} |
39 |
39 |
|
40 fun actor :: "event \<Rightarrow> thread" where |
|
41 "actor (Create th pty) = th" | |
|
42 "actor (Exit th) = th" | |
|
43 "actor (P th cs) = th" | |
|
44 "actor (V th cs) = th" | |
|
45 "actor (Set th pty) = th" |
|
46 |
|
47 fun isCreate :: "event \<Rightarrow> bool" where |
|
48 "isCreate (Create th pty) = True" | |
|
49 "isCreate _ = False" |
|
50 |
|
51 fun isP :: "event \<Rightarrow> bool" where |
|
52 "isP (P th cs) = True" | |
|
53 "isP _ = False" |
|
54 |
|
55 fun isV :: "event \<Rightarrow> bool" where |
|
56 "isV (V th cs) = True" | |
|
57 "isV _ = False" |
40 |
58 |
41 text {* |
59 text {* |
42 As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events, |
60 As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events, |
43 which is defined by the following type @{text "state"}: |
61 which is defined by the following type @{text "state"}: |
44 *} |
62 *} |