--- a/no_shm_selinux/Static.thy	Wed Jan 08 18:40:38 2014 +0800
+++ b/no_shm_selinux/Static.thy	Thu Jan 09 14:39:00 2014 +0800
@@ -99,38 +99,30 @@
      | _ \<Rightarrow> None)"
 *)
 
-fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
+fun init_obj2sobj :: "t_dobject \<Rightarrow> t_sobject option"
 where
-  "init_obj2sobj (O_proc p) = 
+  "init_obj2sobj (D_proc p) = 
      (case (init_cp2sproc p) of 
        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
      | _ \<Rightarrow> None)"
-| "init_obj2sobj (O_file f) = 
+| "init_obj2sobj (D_file f) = 
      Some (S_file (init_cf2sfiles f) 
                   (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
-| "init_obj2sobj (O_dir f) = 
+| "init_obj2sobj (D_dir f) = 
      (case (init_cf2sfile f) of
            Some sf \<Rightarrow> Some (S_dir sf) 
          | _ \<Rightarrow> None)"
-| "init_obj2sobj (O_msgq q) = None"
-
-(*
-     (case (init_cq2smsgq q) of
-       Some sq \<Rightarrow> Some (S_msgq sq)
-     | _ \<Rightarrow> None)"
+| "init_obj2sobj (D_msgq q) = None"
 
-| "init_obj2sobj (O_shm h) = 
-     (case (init_ch2sshm h) of 
-       Some sh \<Rightarrow> Some (S_shm sh)
-     | _       \<Rightarrow> None)"  
-| "init_obj2sobj (O_msg q m) = 
-     (case (init_cq2smsgq q, init_cm2smsg q m) of 
-        (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
-      | _                  \<Rightarrow> None)" *)
-| "init_obj2sobj _ = None"
+fun init_dalive :: "t_dobject \<Rightarrow> bool"
+where
+  "init_dalive (D_proc p) = (p \<in> init_procs)"
+| "init_dalive (D_file f) = (is_init_file f)"
+| "init_dalive (D_dir  f) = (is_init_dir  f)"
+| "init_dalive (D_msgq q) = False"
 
 definition  
-  "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
+  "init_static_state \<equiv> {sobj. \<exists> obj. init_dalive obj \<and> init_obj2sobj obj = Some sobj}"
 
 (**************** translation from dynamic to static *******************)
 
@@ -227,39 +219,33 @@
                      (Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms)
                    | _ \<Rightarrow> None)"
 
-fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
+fun co2sobj :: "t_state \<Rightarrow> t_dobject \<Rightarrow> t_sobject option"
 where
-  "co2sobj s (O_proc p) = 
+  "co2sobj s (D_proc p) = 
      (case (cp2sproc s p) of 
         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
       | _       \<Rightarrow> None)"
-| "co2sobj s (O_file f) = 
+| "co2sobj s (D_file f) = 
      Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
-| "co2sobj s (O_dir f) = 
+| "co2sobj s (D_dir f) = 
      (case (cf2sfile s f) of
         Some sf  \<Rightarrow> Some (S_dir sf)
       | _ \<Rightarrow> None)"
-| "co2sobj s (O_msgq q) = 
+| "co2sobj s (D_msgq q) = 
      (case (cq2smsgq s q) of
         Some sq \<Rightarrow> Some (S_msgq sq)
       | _ \<Rightarrow> None)"
-(*
-| "co2sobj s (O_shm h) = 
-     (case (ch2sshm s h) of 
-        Some sh \<Rightarrow> Some (S_shm sh)
-      | _ \<Rightarrow> None)"
 
-| "co2sobj s (O_msg q m) = 
-     (case (cq2smsgq s q, cm2smsg s q m) of 
-       (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
-     | _ \<Rightarrow> None)"
-*)
-| "co2sobj s _ = None"
-
+fun dalive :: "t_state \<Rightarrow> t_dobject \<Rightarrow> bool"
+where
+  "dalive s (D_proc p) = (p \<in> current_procs s)"
+| "dalive s (D_file f) = (is_file s f)"
+| "dalive s (D_dir  f) = (is_dir  s f)"
+| "dalive s (D_msgq q) = (q \<in> current_msgqs s)"
 
 definition s2ss :: "t_state \<Rightarrow> t_static_state"
 where
-  "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
+  "s2ss s \<equiv> {sobj. \<exists> obj. dalive s obj \<and> co2sobj s obj = Some sobj}"
 
 
 (* ******************************************************** *)