search

p-org / PSharp

A framework for rapid development of reliable asynchronous software.
MIT License
390 stars 37 forks source link

Question regarding /coverage:activity #470

Closed ankushdesai closed 5 years ago

ankushdesai commented 5 years ago

A tuple (M, S, E) is said to be covered by a test run if state S of machine M actually dequeues an event of type E during an execution.

Questions: Is receive (implemented using PSharp await) covered as well ?

pdeligia commented 5 years ago

If I am not wrong, we do not include receive statements in the activity coverage today. Is that correct, @akashlal?

akashlal commented 5 years ago

Receive does count against the activity coverage. See references of the method ReportActivityCoverageOfReceivedEvent. It is called both on dequeue as well as on Receive.

ankushdesai commented 5 years ago

Great, thanks!

On Wed, Sep 4, 2019, 12:02 AM Akash Lal notifications@github.com wrote:

Receive does count against the activity coverage. See references of the method ReportActivityCoverageOfReceivedEvent. It is called both on dequeue as well as on Receive.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/p-org/PSharp/issues/470?email_source=notifications&email_token=ADAQV7GA6KTAHOPGKVQKUG3QH5MPHA5CNFSM4ITKYE2KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD52SKVA#issuecomment-527770964, or mute the thread https://github.com/notifications/unsubscribe-auth/ADAQV7EOY5ZXA6TKOYKUZXTQH5MPHANCNFSM4ITKYE2A .