PSharp icon indicating copy to clipboard operation
PSharp copied to clipboard

Attributes and syntax extensions for the built-in timers

Open pdeligia opened this issue 7 years ago • 0 comments

Low-priority proposal. It would be nice to have attributes and syntax extensions that simplify using the new built-in timers.

For example, instead of the user having to explicitly handle a TimerElapsedEvent, they could use an attribute such as:

[OnTimeoutDoAction(nameof(HandleTimeoutForPing))]
class SomeState : MachineState { }

instead of:

[OnEventDoAction(typeof(TimerElapsedEvent), nameof(HandleTimeoutForPing))]
class SomeState : MachineState { }

Also, the HandleTimeoutForPing would now receive the TimerInfo as argument (instead of having to access the TimerElapsedEvent which would be internal.

void HandleTimeout(TimerInfo info) {
  ...
}

instead of:

void HandleTimeout() {
  var info = (this.ReceivedEvent as TimerElapsedEvent).Info;
  ...
}

This can be supported in the P# syntax on something like:

on timeout do HandleTimeout;

pdeligia avatar Mar 22 '19 01:03 pdeligia