How to restrict a grammar

In the past week Jan implemented a syntax checker for Acumen models intended to run with the enclosure interpreter. The checker validates that the model conforms to the subset of Acumen syntax used for the shallow embedding of a hybrid automaton. Jan has been working on a formalization of the Acumen subset in BNF form, but has found the formalism too limited to elegantly express certain aspects of the grammar. As an example consider the way events, i.e. transitions in the automaton, are expressed. This is done as follows: the underlying graph of the automaton is expressed by a single switch statement, with cases representing the hybrid modes. Events are specified by if statements, with an assignment to the mode variable indicating the target mode of the transition. Jan would like to constrain the grammar to require that there is precisely one assignment to the mode variable in each if statement, but has not found a way of doing this in plain BNF. As a quick fix he is considering adding this and similar constraints in natural language comments accompanying the grammar, but he is also looking at generalizations of BNF that would allow him to express this property within the grammar itself.