644 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
644 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
645 where |
645 where |
646 "init_obj_related (S_proc (pi, sec, fds) tag) (O_proc p') = (pi = Init p')" |
646 "init_obj_related (S_proc (pi, sec, fds) tag) (O_proc p') = (pi = Init p')" |
647 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
647 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
648 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
648 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
649 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')" |
|
650 (* |
649 (* |
651 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
650 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
652 |
651 |
653 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
652 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
654 *) |
653 *) |
656 |
655 |
657 |
656 |
658 |
657 |
659 (***************** for backward proof when Instancing static objects ******************) |
658 (***************** for backward proof when Instancing static objects ******************) |
660 |
659 |
|
660 (* |
661 fun all_procs :: "t_state \<Rightarrow> t_process set" |
661 fun all_procs :: "t_state \<Rightarrow> t_process set" |
662 where |
662 where |
663 "all_procs [] = init_procs" |
663 "all_procs [] = init_procs" |
664 | "all_procs (Clone p p' fds # s) = insert p' (all_procs s)" |
664 | "all_procs (Clone p p' fds # s) = insert p' (all_procs s)" |
665 | "all_procs (e # s) = all_procs s" |
665 | "all_procs (e # s) = all_procs s" |
|
666 *) |
666 |
667 |
667 definition next_nat :: "nat set \<Rightarrow> nat" |
668 definition next_nat :: "nat set \<Rightarrow> nat" |
668 where |
669 where |
669 "next_nat nset = (Max nset) + 1" |
670 "next_nat nset = (Max nset) + 1" |
670 |
671 |
671 definition new_proc :: "t_state \<Rightarrow> t_process" |
672 definition new_proc :: "t_state \<Rightarrow> t_process" |
672 where |
673 where |
673 "new_proc \<tau> = next_nat (current_procs \<tau>)" |
674 "new_proc \<tau> = next_nat (current_procs \<tau>)" |
674 |
675 |
|
676 (* |
675 definition brandnew_proc :: "t_state \<Rightarrow> t_process" |
677 definition brandnew_proc :: "t_state \<Rightarrow> t_process" |
676 where |
678 where |
677 "brandnew_proc s \<equiv> next_nat (all_procs s)" |
679 "brandnew_proc s \<equiv> next_nat (all_procs s)" |
|
680 *) |
|
681 |
678 |
682 |
679 definition new_inode_num :: "t_state \<Rightarrow> nat" |
683 definition new_inode_num :: "t_state \<Rightarrow> nat" |
680 where |
684 where |
681 "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)" |
685 "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)" |
682 |
686 |
696 |
700 |
697 definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd" |
701 definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd" |
698 where |
702 where |
699 "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)" |
703 "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)" |
700 |
704 |
701 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set" |
705 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname set" |
702 where |
706 where |
703 "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}" |
707 "all_fname_under_dir d \<tau> fs = {fn. \<exists> f. fn # d = f \<and> f \<in> (current_files \<tau> \<union> fs)}" |
704 |
708 |
705 fun fname_all_a:: "nat \<Rightarrow> t_fname" |
709 fun fname_all_a:: "nat \<Rightarrow> t_fname" |
706 where |
710 where |
707 "fname_all_a 0 = []" | |
711 "fname_all_a 0 = []" | |
708 "fname_all_a (Suc n) = ''a''@(fname_all_a n)" |
712 "fname_all_a (Suc n) = ''a''@(fname_all_a n)" |
709 |
713 |
710 definition fname_length_set :: "t_fname set \<Rightarrow> nat set" |
714 definition fname_length_set :: "t_fname set \<Rightarrow> nat set" |
711 where |
715 where |
712 "fname_length_set fns = length`fns" |
716 "fname_length_set fns = length`fns" |
713 |
717 |
714 definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname" |
718 definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_fname" |
715 where |
719 where |
716 "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)" |
720 "next_fname pf \<tau> fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau> fs))) + 1)" |
|
721 |
|
722 definition new_childf_general:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file set \<Rightarrow> t_file" |
|
723 where |
|
724 "new_childf_general pf \<tau> fs = next_fname pf \<tau> fs # pf" |
717 |
725 |
718 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file" |
726 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file" |
719 where |
727 where |
720 "new_childf pf \<tau> = next_fname pf \<tau> # pf" |
728 "new_childf pf \<tau> = new_childf_general pf \<tau> {}" |
721 |
729 |
722 end |
730 end |
723 |
731 |
724 end |
732 end |