Assert and Assume annotations on Events

[ankushdesai]

I upgraded to the latest version of P# and it seems like Event class does not take the Assert and Assume values as parameters anymore.

Has P# dropped the support for it?

How do I initialize it?

[pdeligia]

Hey @ankushdesai, we removed them from the event class in order to optimize for memory in production (as these two are only used during testing). You can now pass these arguments via the machine and runtime Send APIs using an optional parameter SendOptions (its constructor can set assert and assume). Btw, please note that assume was never really supported by P# (even if you can pass it as a parameter), we left it there for historical reasons (from P) and we might end up either removing it in a future release (have to discuss this with @akashlal). I believe that right now in P# using assume gives the same result as using assert (instead of e.g. not scheduling paths that would generate more events than the assumption).

[ankushdesai]

Thanks, Pantazis. I have updated P to use the latest version of P#. It would be good if we can figure out the PLogger story.

On Wed, Aug 14, 2019 at 12:10 AM Pantazis Deligiannis < notifications@github.com> wrote:

Hey @ankushdesai https://github.com/ankushdesai, we removed them from the event class in order to optimize for memory in production (as these two are only used during testing). You can now pass these arguments via the machine and runtime Send APIs using an optional parameter SendOptions (its constructor can set assert and assume). Btw, please note that assume was never really supported by P# (even if you can pass it as a parameter), we left it there for historical reasons (from P) and we might end up either removing it in a future release (have to discuss this with @akashlal https://github.com/akashlal). I believe that right now in P# using assume gives the same result as using assert (instead of e.g. not scheduling paths that would generate more events than the assumption).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/p-org/PSharp/issues/456?email_source=notifications&email_token=ADAQV7AMA6IQCLHX5IS4JD3QEOVW5A5CNFSM4ILRAHFKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD4H43JI#issuecomment-521129381, or mute the thread https://github.com/notifications/unsubscribe-auth/ADAQV7BIDR7MUEVJ7YZLB7TQEOVW5ANCNFSM4ILRAHFA .

[akashlal]

One of the reasons for this change, in addition to performance optimization, was that we didn't much use of these annotations. If they really are useful, we can consider adding them back in some way, e.g., through annotations on the event class declaration. These annotations would only be interpreted by the testing runtime so there will be no performance implications for production. The current SendOptions methodology works as well, but requires one to annotate each send to get the same effect as a P constraint.

[pdeligia]

Hey Ankush, I am finishing up some tasks this week, and then I will try to add support for adding custom logging during testing, so you can then use again the PLogger. I don't think it will be too hard to support that.

[ankushdesai]

Thanks, please let me know when you are done.

On Wed, Aug 14, 2019 at 1:49 PM Pantazis Deligiannis < notifications@github.com> wrote:

Hey Ankush, I am finishing up some tasks this week, and then I will try to add support for adding custom logging during testing, so you can then use again the PLogger. I don't think it will be too hard to support that.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/p-org/PSharp/issues/456?email_source=notifications&email_token=ADAQV7D7KXA5POQOH3MO66LQERVXDA5CNFSM4ILRAHFKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD4KCE7A#issuecomment-521413244, or mute the thread https://github.com/notifications/unsubscribe-auth/ADAQV7BHX6U6RSIXAO77KGLQERVXDANCNFSM4ILRAHFA .

[pdeligia]

I just added an issue here #459, so we can track it seperately from this question.