equal
deleted
inserted
replaced
756 | "deleted obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> (\<exists> m. obj = O_msg q m) \<or> deleted obj s)" |
756 | "deleted obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> (\<exists> m. obj = O_msg q m) \<or> deleted obj s)" |
757 | "deleted obj (DeleteShM p h # s) = (obj = O_shm h \<or> deleted obj s)" |
757 | "deleted obj (DeleteShM p h # s) = (obj = O_shm h \<or> deleted obj s)" |
758 | "deleted obj (RecvMsg p q m # s) = (obj = O_msg q m \<or> deleted obj s)" |
758 | "deleted obj (RecvMsg p q m # s) = (obj = O_msg q m \<or> deleted obj s)" |
759 | "deleted obj (_ # s) = deleted obj s" |
759 | "deleted obj (_ # s) = deleted obj s" |
760 |
760 |
|
761 |
|
762 definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set" |
|
763 where |
|
764 "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}" |
|
765 |
|
766 |
|
767 definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set" |
|
768 "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}" |
761 |
769 |
762 end |
770 end |
763 |
771 |
764 |
772 |
765 |
773 |