UMLR — Need BNF for Protocol State Machines Transitions

There is no BNF for the transition syntax of Protocol State Machines. The standard BNF for behavior State Machines is not sufficient as it allows for actions and doesn't allow for post-conditions.

It is not clear currently, for example, whether a post-condition is required, and if it's not there, does the transition string require a trailing / (as shown in the examples)?
My guess is that the missing BNF should be something like:

['['<pre-condition>']'][<trigger>[‘,’ <trigger>]*]  ['/' ['['post-condition']']] 

To not invalidate any existing diagrams, the trailing "/" is allowed even without a following post condition. It also allows multiple triggers, but only one pre and only one post condition as per the abstract syntax.

Since I based this on the pre-existing transistion trigger, it will allow all triggers, including change events, time events, and ALL.
Whatever the syntax is decided on should be included in the spec.