--- a/rc_theory.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/rc_theory.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -463,21 +463,6 @@
        (Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible
      | _                \<Rightarrow> False               )"
 
-
-(**** OS' job: checking resources existence & grant new resource ****)
-
-definition next_nat :: "nat set \<Rightarrow> nat"
-where
-  "next_nat ps = (Max ps) + 1"
-
-definition new_proc :: "t_state \<Rightarrow> t_process"
-where 
-  "new_proc \<tau> = next_nat (current_procs \<tau>)"
-
-definition new_ipc :: "t_state \<Rightarrow> t_ipc"
-where
-  "new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
-
 (* new file pathname is user-defined, so os just check if its unexistence *) 
 fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
 where
@@ -487,10 +472,10 @@
 | "os_grant \<tau> (ReadFile p f)   = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
 | "os_grant \<tau> (WriteFile p f)  = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
 | "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)"
-| "os_grant \<tau> (CreateIPC p i)  = (p \<in> current_procs \<tau> \<and> i = new_ipc \<tau>)"
+| "os_grant \<tau> (CreateIPC p i)  = (p \<in> current_procs \<tau> \<and> i \<notin> current_ipcs \<tau>)" (* i = new_ipc \<tau> *)
 | "os_grant \<tau> (Send p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 
 | "os_grant \<tau> (Recv p i)       = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
-| "os_grant \<tau> (Clone p p')     = (p \<in> current_procs \<tau> \<and> p' = new_proc \<tau>)"
+| "os_grant \<tau> (Clone p p')     = (p \<in> current_procs \<tau> \<and> p' \<notin> current_procs \<tau>)" (* p' = new_proc \<tau> *)
 | "os_grant \<tau> (Kill p p')      = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)" 
 | "os_grant \<tau> (DeleteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> (\<exists>fn. fn # f \<in> current_files \<tau>))"
 | "os_grant \<tau> (DeleteIPC p i)  = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" 
@@ -961,7 +946,19 @@
   "initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p"
 | "initp_intact_but s _                   = initp_intact s"
 
-(*** how to generating new valid pathname for examples of CreateFile ***)
+(*** how to generating new valid pathname for examples of new_proc, new_ipc and new_file as CreateFile ***)
+
+definition next_nat :: "nat set \<Rightarrow> nat"
+where
+  "next_nat ps = (Max ps) + 1"
+
+definition new_proc :: "t_state \<Rightarrow> t_process"
+where 
+  "new_proc \<tau> = next_nat (current_procs \<tau>)"
+
+definition new_ipc :: "t_state \<Rightarrow> t_ipc"
+where
+  "new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
 
 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
 where