# HG changeset patch
# User chunhan
# Date 1384926272 -28800
# Node ID fc7151df7f8e7c52f7702cc0180117fb402d4632
# Parent  742bed61324568ec1ca6ed39a6ba47ce7b2d9eb9
simplifing model, by changing current_proc_fds to proc_file_fds in the Clone & Execve cases of os_grant

diff -r 742bed613245 -r fc7151df7f8e Flask.thy
--- a/Flask.thy	Wed Nov 20 13:43:09 2013 +0800
+++ b/Flask.thy	Wed Nov 20 13:44:32 2013 +0800
@@ -690,7 +690,7 @@
 | "os_grant \<tau> (WriteFile p fd)                = 
     (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> 
      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 
-     (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
+     (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))" 
 | "os_grant \<tau> (Execve p f fds)                = 
     (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> proc_file_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} \<and> fds \<subseteq> current_proc_fds \<tau> p *)
 (*