Note: for the sake of a cleaner grammar, we use : instead of | to denote a nondeterministic selection. Can nondeterministic selections contain else-clauses?
Operational Semantics: nondeterministic selection blocks until at least one guard becomes true. While any number of guards may be true, one of the true guards is chosen arbitrarily1 as the path of execution.
Execution: More than one guard is allowed to be true, but only branch is chosen to be executed. Q: Do we use the notion of a time-window before evaluating guards?