equal
deleted
inserted
replaced
508 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
508 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
509 where |
509 where |
510 "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)" |
510 "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)" |
511 *) |
511 *) |
512 |
512 |
513 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
513 fun current_msgqs :: "t_state \<Rightarrow> t_msgq set" |
514 where |
514 where |
515 "current_msgqs [] = init_msgqs" |
515 "current_msgqs [] = init_msgqs" |
516 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |
516 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |
517 | "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}" |
517 | "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}" |
518 | "current_msgqs (_ # \<tau>) = current_msgqs \<tau>" |
518 | "current_msgqs (_ # \<tau>) = current_msgqs \<tau>" |