equal
deleted
inserted
replaced
67 caller_def "caller ch == %s p. (cbit (ch s p), arg (ch s p))" |
67 caller_def "caller ch == %s p. (cbit (ch s p), arg (ch s p))" |
68 rtrner_def "rtrner ch == %s p. (rbit (ch s p), res (ch s p))" |
68 rtrner_def "rtrner ch == %s p. (rbit (ch s p), res (ch s p))" |
69 |
69 |
70 Calling_def "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >" |
70 Calling_def "Calling ch p == PRED cbit< ch!p > ~= rbit< ch!p >" |
71 Call_def "(ACT Call ch p v) == ACT ~ $Calling ch p |
71 Call_def "(ACT Call ch p v) == ACT ~ $Calling ch p |
72 & (cbit<ch!p>` ~= $rbit<ch!p>) |
72 & (cbit<ch!p>$ ~= $rbit<ch!p>) |
73 & (arg<ch!p>` = $v)" |
73 & (arg<ch!p>$ = $v)" |
74 Return_def "(ACT Return ch p v) == ACT $Calling ch p |
74 Return_def "(ACT Return ch p v) == ACT $Calling ch p |
75 & (rbit<ch!p>` = $cbit<ch!p>) |
75 & (rbit<ch!p>$ = $cbit<ch!p>) |
76 & (res<ch!p>` = $v)" |
76 & (res<ch!p>$ = $v)" |
77 PLegalCaller_def "PLegalCaller ch p == TEMP |
77 PLegalCaller_def "PLegalCaller ch p == TEMP |
78 Init(~ Calling ch p) |
78 Init(~ Calling ch p) |
79 & [][ ? a. Call ch p a ]_((caller ch)!p)" |
79 & [][ ? a. Call ch p a ]_((caller ch)!p)" |
80 LegalCaller_def "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" |
80 LegalCaller_def "LegalCaller ch == TEMP (! p. PLegalCaller ch p)" |
81 PLegalReturner_def "PLegalReturner ch p == TEMP |
81 PLegalReturner_def "PLegalReturner ch p == TEMP |