61 caller_def: "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))" |
61 caller_def: "caller ch == \<lambda>s p. (cbit (ch s p), arg (ch s p))" |
62 rtrner_def: "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))" |
62 rtrner_def: "rtrner ch == \<lambda>s p. (rbit (ch s p), res (ch s p))" |
63 |
63 |
64 Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >" |
64 Calling_def: "Calling ch p == PRED cbit< ch!p > \<noteq> rbit< ch!p >" |
65 Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p |
65 Call_def: "(ACT Call ch p v) == ACT \<not> $Calling ch p |
66 & (cbit<ch!p>$ \<noteq> $rbit<ch!p>) |
66 \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>) |
67 & (arg<ch!p>$ = $v)" |
67 \<and> (arg<ch!p>$ = $v)" |
68 Return_def: "(ACT Return ch p v) == ACT $Calling ch p |
68 Return_def: "(ACT Return ch p v) == ACT $Calling ch p |
69 & (rbit<ch!p>$ = $cbit<ch!p>) |
69 \<and> (rbit<ch!p>$ = $cbit<ch!p>) |
70 & (res<ch!p>$ = $v)" |
70 \<and> (res<ch!p>$ = $v)" |
71 PLegalCaller_def: "PLegalCaller ch p == TEMP |
71 PLegalCaller_def: "PLegalCaller ch p == TEMP |
72 Init(\<not> Calling ch p) |
72 Init(\<not> Calling ch p) |
73 & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)" |
73 \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)" |
74 LegalCaller_def: "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)" |
74 LegalCaller_def: "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)" |
75 PLegalReturner_def: "PLegalReturner ch p == TEMP |
75 PLegalReturner_def: "PLegalReturner ch p == TEMP |
76 \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)" |
76 \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)" |
77 LegalReturner_def: "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)" |
77 LegalReturner_def: "LegalReturner ch == TEMP (\<forall>p. PLegalReturner ch p)" |
78 |
78 |