equal
deleted
inserted
replaced
201 "is_init_udp_sock s \<equiv> (case (init_inum_of_socket s) of |
201 "is_init_udp_sock s \<equiv> (case (init_inum_of_socket s) of |
202 Some i \<Rightarrow> (case (init_itag_of_inum i) of |
202 Some i \<Rightarrow> (case (init_itag_of_inum i) of |
203 Some Tag_UDP_SOCK \<Rightarrow> True |
203 Some Tag_UDP_SOCK \<Rightarrow> True |
204 | _ \<Rightarrow> False) |
204 | _ \<Rightarrow> False) |
205 | _ \<Rightarrow> False)" |
205 | _ \<Rightarrow> False)" |
|
206 |
|
207 definition init_same_inode_files :: "t_file \<Rightarrow> t_file set" |
|
208 where |
|
209 "init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}" |
206 |
210 |
207 fun init_alive :: "t_object \<Rightarrow> bool" |
211 fun init_alive :: "t_object \<Rightarrow> bool" |
208 where |
212 where |
209 "init_alive (O_proc p) = (p \<in> init_procs)" |
213 "init_alive (O_proc p) = (p \<in> init_procs)" |
210 | "init_alive (O_file f) = (is_init_file f)" |
214 | "init_alive (O_file f) = (is_init_file f)" |
472 "current_sock_inums \<tau> = {im. \<exists> s. inum_of_socket \<tau> s = Some im}" |
476 "current_sock_inums \<tau> = {im. \<exists> s. inum_of_socket \<tau> s = Some im}" |
473 |
477 |
474 definition current_inode_nums :: "t_state \<Rightarrow> nat set" |
478 definition current_inode_nums :: "t_state \<Rightarrow> nat set" |
475 where |
479 where |
476 "current_inode_nums \<tau> = current_file_inums \<tau> \<union> current_sock_inums \<tau>" |
480 "current_inode_nums \<tau> = current_file_inums \<tau> \<union> current_sock_inums \<tau>" |
|
481 |
|
482 definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set" |
|
483 where |
|
484 "same_inode_files s f \<equiv> {f'. inum_of_file s f = inum_of_file s f'}" |
477 |
485 |
478 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option" |
486 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option" |
479 where |
487 where |
480 "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd" |
488 "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd" |
481 | "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = |
489 | "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = |