461 | "rc_grant \<tau> (Kill p p') = ( |
461 | "rc_grant \<tau> (Kill p p') = ( |
462 case (currentrole \<tau> p, type_of_process \<tau> p') of |
462 case (currentrole \<tau> p, type_of_process \<tau> p') of |
463 (Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible |
463 (Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible |
464 | _ \<Rightarrow> False )" |
464 | _ \<Rightarrow> False )" |
465 |
465 |
466 |
|
467 (**** OS' job: checking resources existence & grant new resource ****) |
|
468 |
|
469 definition next_nat :: "nat set \<Rightarrow> nat" |
|
470 where |
|
471 "next_nat ps = (Max ps) + 1" |
|
472 |
|
473 definition new_proc :: "t_state \<Rightarrow> t_process" |
|
474 where |
|
475 "new_proc \<tau> = next_nat (current_procs \<tau>)" |
|
476 |
|
477 definition new_ipc :: "t_state \<Rightarrow> t_ipc" |
|
478 where |
|
479 "new_ipc \<tau> = next_nat (current_ipcs \<tau>)" |
|
480 |
|
481 (* new file pathname is user-defined, so os just check if its unexistence *) |
466 (* new file pathname is user-defined, so os just check if its unexistence *) |
482 fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool" |
467 fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool" |
483 where |
468 where |
484 "os_grant \<tau> (Execute p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
469 "os_grant \<tau> (Execute p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
485 | "os_grant \<tau> (CreateFile p f) = (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> (\<exists> pf. (parent f = Some pf) \<and> pf \<in> current_files \<tau>))" (*cannot create disk, ?? or f = [] ??*) |
470 | "os_grant \<tau> (CreateFile p f) = (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> (\<exists> pf. (parent f = Some pf) \<and> pf \<in> current_files \<tau>))" (*cannot create disk, ?? or f = [] ??*) |
486 | "os_grant \<tau> (ChangeRole p r) = (p \<in> current_procs \<tau>)" |
471 | "os_grant \<tau> (ChangeRole p r) = (p \<in> current_procs \<tau>)" |
487 | "os_grant \<tau> (ReadFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
472 | "os_grant \<tau> (ReadFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
488 | "os_grant \<tau> (WriteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
473 | "os_grant \<tau> (WriteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
489 | "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)" |
474 | "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)" |
490 | "os_grant \<tau> (CreateIPC p i) = (p \<in> current_procs \<tau> \<and> i = new_ipc \<tau>)" |
475 | "os_grant \<tau> (CreateIPC p i) = (p \<in> current_procs \<tau> \<and> i \<notin> current_ipcs \<tau>)" (* i = new_ipc \<tau> *) |
491 | "os_grant \<tau> (Send p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
476 | "os_grant \<tau> (Send p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
492 | "os_grant \<tau> (Recv p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
477 | "os_grant \<tau> (Recv p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
493 | "os_grant \<tau> (Clone p p') = (p \<in> current_procs \<tau> \<and> p' = new_proc \<tau>)" |
478 | "os_grant \<tau> (Clone p p') = (p \<in> current_procs \<tau> \<and> p' \<notin> current_procs \<tau>)" (* p' = new_proc \<tau> *) |
494 | "os_grant \<tau> (Kill p p') = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)" |
479 | "os_grant \<tau> (Kill p p') = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)" |
495 | "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>))" |
480 | "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>))" |
496 | "os_grant \<tau> (DeleteIPC p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
481 | "os_grant \<tau> (DeleteIPC p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
497 |
482 |
498 (**** system valid state ****) |
483 (**** system valid state ****) |
959 fun initp_intact_but :: "t_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
944 fun initp_intact_but :: "t_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
960 where |
945 where |
961 "initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p" |
946 "initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p" |
962 | "initp_intact_but s _ = initp_intact s" |
947 | "initp_intact_but s _ = initp_intact s" |
963 |
948 |
964 (*** how to generating new valid pathname for examples of CreateFile ***) |
949 (*** how to generating new valid pathname for examples of new_proc, new_ipc and new_file as CreateFile ***) |
|
950 |
|
951 definition next_nat :: "nat set \<Rightarrow> nat" |
|
952 where |
|
953 "next_nat ps = (Max ps) + 1" |
|
954 |
|
955 definition new_proc :: "t_state \<Rightarrow> t_process" |
|
956 where |
|
957 "new_proc \<tau> = next_nat (current_procs \<tau>)" |
|
958 |
|
959 definition new_ipc :: "t_state \<Rightarrow> t_ipc" |
|
960 where |
|
961 "new_ipc \<tau> = next_nat (current_ipcs \<tau>)" |
965 |
962 |
966 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set" |
963 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set" |
967 where |
964 where |
968 "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}" |
965 "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}" |
969 |
966 |