--- a/Static.thy	Tue Oct 08 16:37:39 2013 +0800
+++ b/Static.thy	Thu Oct 10 12:00:49 2013 +0800
@@ -482,7 +482,7 @@
      | _ \<Rightarrow> sobj = sobj')}"
 
 
-(* no del 
+
 (* all reachable static states(sobjects set) *)
 inductive_set static :: "t_static_state set"
 where
@@ -650,15 +650,19 @@
 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')"
 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
+(*
 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')"
+*)
 | "init_obj_related _ _ = False"
 
 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
 where
   "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
+(*
 | "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
      (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"
+*)
 | "tainted_s ss _ = False"
 
 (*