time labels (ARRANGE language)

Transitions in express scenarios can be time-labeled in a similar way to mCRL2. Let's start with a scenario that has no time-labels yet.

express status_20140709_slide7 = 
  (a . (b . c)* . b?) 
  | (d . e*);

To specify time constraints as shown in the figure

append time labels to actions denoting them with an @.

express status_20140709_slide7_labeled = 
  (a@t1 . (b . c@(t2 => t2<t1+500))* . b?) 
  | (d@t3 . e @(t3i => t3i>t3+200) @t3 *);

Notice how two time labels have been appended to action e, that is @(t3i=>t3i>t3+200) and @t3.