equal
deleted
inserted
replaced
64 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)" |
64 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)" |
65 |
65 |
66 primrec hotel :: "event list \<Rightarrow> bool" |
66 primrec hotel :: "event list \<Rightarrow> bool" |
67 where |
67 where |
68 "hotel [] = True" |
68 "hotel [] = True" |
69 | "hotel (e # s) = (hotel s & (case e of |
69 | "hotel (e # s) = (hotel s \<and> (case e of |
70 Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s | |
70 Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s | |
71 Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) | |
71 Enter g r (k,k') \<Rightarrow> (k,k') \<in> cards s g \<and> (roomk s r \<in> {k, k'}) | |
72 Exit g r \<Rightarrow> g : isin s r))" |
72 Exit g r \<Rightarrow> g \<in> isin s r))" |
73 |
73 |
74 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*) |
74 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*) |
75 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)" |
75 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)" |
76 |
76 |
77 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool" |
77 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool" |