equal
deleted
inserted
replaced
56 | _ \<Rightarrow> None)" |
56 | _ \<Rightarrow> None)" |
57 |
57 |
58 definition init_cph2spshs |
58 definition init_cph2spshs |
59 :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set" |
59 :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set" |
60 where |
60 where |
61 "init_cph2spshs p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> init_procs_of_shm h \<and> |
61 "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> |
62 init_ch2sshm h = Some sh}" |
62 init_ch2sshm h = Some sh}" |
63 |
63 |
64 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option" |
64 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option" |
65 where |
65 where |
66 "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of |
66 "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of |
721 Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec) |
721 Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec) |
722 | _ \<Rightarrow> None)" |
722 | _ \<Rightarrow> None)" |
723 |
723 |
724 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set" |
724 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set" |
725 where |
725 where |
726 "cph2spshs s p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}" |
726 "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}" |
727 |
727 |
728 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option" |
728 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option" |
729 where |
729 where |
730 "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of |
730 "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of |
731 Some sec \<Rightarrow> |
731 Some sec \<Rightarrow> |