For now, we are triggering a warning if self loops exist in the protocol. This is because we are not handling them in the proper way.
We can fix this problem in the following way:
If the self loop is a default transition, then it is pointless
If the self loop is a transition with predicate and time constraint, we can add a new urgent state.
For example: A - [b,t<4] -> A can be transformed to:
For now, we are triggering a warning if self loops exist in the protocol. This is because we are not handling them in the proper way. We can fix this problem in the following way:
For example:
A - [b,t<4] -> A
can be transformed to: