equal
deleted
inserted
replaced
36 Exit thread | -- {* Thread @{text "thread"} finishing its execution. *} |
36 Exit thread | -- {* Thread @{text "thread"} finishing its execution. *} |
37 P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *} |
37 P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *} |
38 V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} |
38 V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} |
39 Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} |
39 Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} |
40 |
40 |
41 fun actor :: "event \<Rightarrow> thread" where |
41 fun actor where |
42 "actor (Create th pty) = th" | |
|
43 "actor (Exit th) = th" | |
42 "actor (Exit th) = th" | |
44 "actor (P th cs) = th" | |
43 "actor (P th cs) = th" | |
45 "actor (V th cs) = th" | |
44 "actor (V th cs) = th" | |
46 "actor (Set th pty) = th" |
45 "actor (Set th pty) = th" | |
|
46 "actor (Create th prio) = th" |
|
47 |
|
48 definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s" |
47 |
49 |
48 fun isCreate :: "event \<Rightarrow> bool" where |
50 fun isCreate :: "event \<Rightarrow> bool" where |
49 "isCreate (Create th pty) = True" | |
51 "isCreate (Create th pty) = True" | |
50 "isCreate _ = False" |
52 "isCreate _ = False" |
51 |
53 |