Skip to content

Does the new statement introduce a scheduling point? #765

Answered by AnDongLi
dotnwat asked this question in Q&A
Discussion options

You must be logged in to vote

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…

Replies: 2 comments

Comment options

You must be logged in to vote
0 replies
Answer selected by ankushdesai
Comment options

You must be logged in to vote
0 replies
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Category
Q&A
Labels
None yet
3 participants