By: |
![]() ![]() (GenConclAtAddr [2;1;2] THEN Fold `w-Msg` -2 THEN Unfold `w-Msg` -1) THEN Unfold `fair-fifo` 3 THEN Analyze 3 THEN Analyze 4 THEN Analyze 5 THEN Analyze 0 THEN Unfold `w-match` -1 THEN RW assert_pushdownC -1 |
1 |
![]() ![]() ![]() ![]() ![]() ![]() 4. ![]() ![]() 4. isnull(a(i;t)) 4. ![]() ![]() 4. ( ![]() ![]() ![]() 5. ![]() ![]() 5. isrcv(l;a(i;t)) 5. ![]() ![]() 5. destination(l) = i & ||queue(l;t)|| ![]() ![]() 6. ![]() ![]() 6. ![]() ![]() ![]() ![]() ![]() 7. isrcv(kind(e)) 8. ![]() ![]() 9. t : ![]() 10. l : IdLnk 11. ||onlnk(l;m(source(l);t))|| ![]() ![]() 12. ||snds(l;t)|| ![]() 13. ||rcvs(l;time(e))||<||snds(l;t)||+||onlnk(l;m(source(l);t))|| ![]() ![]() ![]() | 2 steps |
About:
![]() | ![]() | ![]() | ![]() | ![]() |