equal
deleted
inserted
replaced
540 |
540 |
541 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option" |
541 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option" |
542 where |
542 where |
543 "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd" |
543 "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd" |
544 | "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = |
544 | "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = |
545 (if (p = p' \<and> fd = fd') then Some flags else flags_of_proc_fd \<tau> p' fd')" |
545 (if (p = p' \<and> fd = fd') then Some flags |
|
546 else flags_of_proc_fd \<tau> p' fd')" |
546 | "flags_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = |
547 | "flags_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = |
547 (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')" |
548 (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')" |
548 | "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = |
549 | "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = |
549 (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')" |
550 (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')" |
550 | "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = |
551 | "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = |
664 where |
665 where |
665 "socket_in_recving \<tau> s \<equiv> (socket_state \<tau> s = Some (SS_trans Trans_Recv)) \<or> (socket_state \<tau> s = Some (SS_trans Trans_RS))" |
666 "socket_in_recving \<tau> s \<equiv> (socket_state \<tau> s = Some (SS_trans Trans_Recv)) \<or> (socket_state \<tau> s = Some (SS_trans Trans_RS))" |
666 |
667 |
667 |
668 |
668 (******* admissable check by the OS *******) |
669 (******* admissable check by the OS *******) |
669 fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool" |
670 fun os_grant:: "t_state \<Rightarrow> t_event \<Rightarrow> bool" |
670 where |
671 where |
671 "os_grant \<tau> (Open p f flags fd inumopt) = ( |
672 "os_grant \<tau> (Open p f flags fd inumopt) = ( |
672 case inumopt of |
673 case inumopt of |
673 Some ino \<Rightarrow> |
674 Some ino \<Rightarrow> |
674 (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> |
675 (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> |