equal
deleted
inserted
replaced
49 | "all_inums (Mkdir p f i # s) = (all_inums s \<union> {i})" |
49 | "all_inums (Mkdir p f i # s) = (all_inums s \<union> {i})" |
50 | "all_inums (CreateSock p af st fd i # s) = (all_inums s \<union> {i})" |
50 | "all_inums (CreateSock p af st fd i # s) = (all_inums s \<union> {i})" |
51 | "all_inums (Accept p fd addr lport fd' i # s) = (all_inums s \<union> {i})" |
51 | "all_inums (Accept p fd addr lport fd' i # s) = (all_inums s \<union> {i})" |
52 | "all_inums (_ # s) = all_inums s" |
52 | "all_inums (_ # s) = all_inums s" |
53 |
53 |
54 fun all_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set" |
|
55 where |
|
56 "all_fds [] = init_fds_of_proc" |
|
57 | "all_fds (Open p f flags fd ipt # s) = (all_fds s) (p := all_fds s p \<union> {fd})" |
|
58 | "all_fds (CreateSock p sf st fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})" |
|
59 | "all_fds (Accept p fd' raddr port fd i # s) = (all_fds s) (p := all_fds s p \<union> {fd})" |
|
60 | "all_fds (Clone p p' fds # s) = (all_fds s) (p' := fds)" |
|
61 | "all_fds (_ # s) = all_fds s" |
|
62 |
54 |
63 fun all_msgqs:: "t_state \<Rightarrow> t_msgq set" |
55 fun all_msgqs:: "t_state \<Rightarrow> t_msgq set" |
64 where |
56 where |
65 "all_msgqs [] = {}" |
57 "all_msgqs [] = {}" |
66 | "all_msgqs (CreateMsgq p q # s) = all_msgqs s \<union> {q}" |
58 | "all_msgqs (CreateMsgq p q # s) = all_msgqs s \<union> {q}" |