-
In the documentation for the
makes it sound as though a message is delivered to the fifo queue of the new machine. Is this true? Is a scheduling point introduced, or does the entry function of the new machine run inline with the caller of |
Beta Was this translation helpful? Give feedback.
Replies: 2 comments
-
For PChecker, new statement compiled to one of CreateStateMachine methods in ControlledRuntime, there is a scheduled point just before creating a StateMachine: Right after the StateMachine is created, OnEntry action will be called during the first time the newly created StateMachine instance runs its EventHandler: In generated ClientServer.cs, Init State of a StateMachine looks like this and Anon is an anonymous function generated for action onEntry and it will be called during above mentioned initialization.
|
Beta Was this translation helpful? Give feedback.
-
A scheduling point is introduced between the machine being created and it executing the entry function of the start state |
Beta Was this translation helpful? Give feedback.
For PChecker, new statement compiled to one of CreateStateMachine methods in ControlledRuntime, there is a scheduled point just before creating a StateMachine:
[https://github.com/p-org/P/blob/b45194b2fa9e7334bf488e3ac887227ee1c2c2d3/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs#L498](Code url)
Right after the StateMachine is created, OnEntry action will be called during the first time the newly created StateMachine instance runs its EventHandler:
[https://github.com/p-org/P/blob/b45194b2fa9e7334bf488e3ac887227ee1c2c2d3/Src/PChecker/CheckerCore/SystematicTesting/ControlledRuntime.cs#L685](Code url)
In generated ClientServer.cs, Init State of a StateMachine looks like thi…