equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 open Network; |
11 open Network; |
12 |
12 |
13 val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = |
13 val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = |
14 goalw thy [stable_def] |
14 Goalw [stable_def] |
15 "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \ |
15 "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \ |
16 \ !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \ |
16 \ !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \ |
17 \ !! m proc. stable Acts {s. m <= s(proc,Sent)}; \ |
17 \ !! m proc. stable Acts {s. m <= s(proc,Sent)}; \ |
18 \ !! n proc. stable Acts {s. n <= s(proc,Rcvd)}; \ |
18 \ !! n proc. stable Acts {s. n <= s(proc,Rcvd)}; \ |
19 \ !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \ |
19 \ !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \ |