The definition of Input_Time must be revised in 8.3.2
(18) _The InputTime property can be used to explicitly specify an input time for ports. This can be done for all ports by specifying the property value for the thread, or it can be specified separately for each port.
-> is impossible, Input_Time only applies to ports
(19) -> some cases are not handled
Dispatch: what if a non zero value?
Completion: In the case of Input_Time, would a negative value mean relative to a future completion? And a positive value relative to the previous completion?
Start: similar question to Completion case
(20) In this case it indicates that input is frozen multiple times for the execution of a dispatch. If a thread has multiple input times specified, then the content of an incoming port is frozen multiple times during a single dispatch.
-> For Start/Completion, this can be done implicitly by the user code, what if Receive_Input is called outside of the offset specified? should be a bounded error
-> For Dispatch/NoIo, should we allow this?
The definition of Input_Time must be revised in 8.3.2
(18) _The InputTime property can be used to explicitly specify an input time for ports. This can be done for all ports by specifying the property value for the thread, or it can be specified separately for each port.
-> is impossible, Input_Time only applies to ports
(19) -> some cases are not handled
(20) In this case it indicates that input is frozen multiple times for the execution of a dispatch. If a thread has multiple input times specified, then the content of an incoming port is frozen multiple times during a single dispatch. -> For Start/Completion, this can be done implicitly by the user code, what if Receive_Input is called outside of the offset specified? should be a bounded error -> For Dispatch/NoIo, should we allow this?
Similar issues for Output_Time