Testing with concrete (and semi-concrete) schedules in P

[osavaryb]

Hi!
I'm currently using P to model and gain assurance about properties of an existing implementation. To convince myself that the P model corresponds to the implementation (as sanity check), I would like to reproduce the implementation's test suite in P.

I am aware of the ability to call pmc with fixed schedules (.schedule), but these are too detailed for this use, since they contain the schedule for every machine in the model. At the moment, our solution has been to create a P machine (as a test driver) handling scheduling at the granularity we wish to describe it, but this does complicate the model. In particular, we have machines in the system waiting for permission from this reified scheduler to proceed at specific points during their execution.

Is this a common pattern in P modeling, and is there a better way to do this?

[ankushdesai]

Hi,
This is a very interesting use-case for P. For cases where we wanted to know if the model contains certain behaviors, what we have done is, write a spec machine that observes a set of messages and assert's false when a particular sequence of events are seen by the monitor. In other words, in this case a monitor spec machine is being used as a observer that raises an alarm when a specific sequence of messages occur in the system. This is one way we have used in the past where we want to check if we are hitting certain behaviors in our models.

What you have mentioned is another interesting case, it would be great to see how we can feed implementation test cases into P. Are your implementation test cases only controlling inputs or controlling messages as well.

If you would like to chat more, lets get on a call and I can share other details and use cases!

Thanks for the questions!

[osavaryb]

Hi Ankush,
Thank you for the quick answer!
Our test cases control for inputs and scheduling, and are testing some messages/behaviors (i.e. this agent gets to a certain state at a determined point in the schedule) and some view of the final state as output.
I'd love to chat more and share about how we are dealing with it in P at the moment and hear your thoughts about it. I will be sending you an email to schedule a call!