Recursive Markov Chain s

We can see an example Recursive Markov Chain in the Fig. 1.

Figure 1: Source code of an example Recursive Markov Chain and its underlying transition graph

The PReMo syntax for defining RMCs is as follows: first we declare all components (procedures), using two numbers as parameters which denote the number of entries and exits; for instance in the example showed on fig. 1 B(1,2); declares ``Component $B$ has 1 entry and 2 exits''. Next, we define the components. Each component definition starts with a declaration of all the boxes contained in the component, together with the component it maps to, e.g., L2(B); declares a box named L2 that is mapped to component B. Next for all entries, internal nodes, and exits of the boxes, we specify a list of transitions available from that control state. A single transition is a probability followed by a goto, call or return instruction separated by a colon. We use goto instruction when the transition leads to an internal node of this component. An instruction call name_of_the_box(entry_number) is used when we want to call the component that is mapped to the box labeled name_of_the_box with a parameter entry_number. Finally we use return value; when we want to exit this component and return value value.

A formal grammar of the input language for RMCs is specified in 4.1.