loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
12 stars 5 forks source link

Initially keyword not relevant in synchronous analysis #93

Open kfhoech opened 2 years ago

kfhoech commented 2 years ago

In the case where a component implementation has synchronous behavior, the initially keyword is ignored and any behavior specified under it is silently ignored. This is appropriate as the initially keyword is relevant in component type specifications only when composed as a subcomponent into a component implementation applying the synchrony keyword such that the subcomponent is non-synchronous.

In this case it is likely that we wish the validator to issue a warning that the initially statement has not effect.