1 Introduction
2 An introduction to OIL
2.1 Instance variables
this
’ to indicate that these belong to the scope of the modelled component instance.power
, job
, tmp
and sheets
. They can be found in the visualisation prepended with the keyword this
, which indicates that this variable is part of the instance state. Instance variable power
stores whether the component is on using enum values \({'off'}\) and \({'on'}\). Instance variable job
stores whether the component is busy with a print job using enum values \({'idle'}\) and \({'busy'}\). Instance variable tmp
stores the temperature of the component as an integer value. Instance variable sheets
stores how many sheets are left to print as an integer value. The initial instance state maps power
to \({'off'}\), job
to \({'idle'}\), tmp
to 20 and sheets
to 0. For brevity of notation, we denote such an instance state by \(\langle {'off'}, {'idle'}, 20, 0 \rangle \).2.2 Areas
power
and job
and contain states for each value in the domain of these variables. The scope in the middle models that the component may only handle jobs when it is switched on. An alternative way of modelling this restriction would be to make the region that refers to job
a child of state \({'on'}\) in the tree structure. The scope on the bottom models that the temperature should stay below 45.
In case the area is a state: the variable for this state equals the value of this state.

In case the area is a scope: its invariant.
power
is active since it is a root area. The state with value \({'off'}\) is active since its parent area is active and the initial instance state maps power
to \({'off'}\). The bottom scope is active since it is a root area and its invariant is true for the initial instance state. An example of an area update is the one for state \({'off'}\), which consists of only one assignment, namely \(\texttt {this.power} := {'off'}\).2.3 Events and transitions
turn_off
, turn_on
, add_job
, \sheet_printed
, \job_printed
and cool_down
. Only events \sheet_printed
and \job_printed
are proactive, indicated by the backslash that precedes the event name. Event \job_printed
is also silent, indicated by [silent]
in the visualisation. Events add_job
and \sheet_printed
have integer parameters nrsheets
and sheetnr
, respectively.tmp
and sheets
. There are no transitions with asserts in this example. Only the transition with event \sheet_printed
has an argument, which specifies that \(\texttt {sheetnr}\) must be equal to \(\texttt {this.sheets}\).sheet_printed
, the transition precondition is \(\texttt {this.power} = {'on'} \wedge \texttt {this.job} = {'busy'} \wedge \texttt {this.sheets} > 0 \wedge \texttt {sheetnr} = \texttt {this.sheets}\), the transition update is \(\{\texttt {this.job} := {'busy'}, \texttt {this.sheets} := \texttt {this.sheets}  1\}\) and the transition postcondition is \(\texttt {this.power} = {'on'} \wedge \texttt {this.job} = {'busy'}\).2.4 Updating the instance state
turn_on
occurs. This event corresponds to two transitions, identified as turn_on #1
and turn_on #2
. Both transitions fire since both transitions’ preconditions are true. This causes turn_on #1
to update power
to \({'on'}\) and turn_on #2
to update tmp
to \(\texttt {tmp} + 5\), resulting in instance state \(\langle {'on'}, {'idle'}, 25, 0 \rangle \). In this instance state both transitions’ postconditions are true and therefore the event succeeds.turn_on
occurs in instance state \(\langle {'off'},\! {'idle'},\!40, 0 \rangle \), both transitions fire which results in instance state \(\langle {'on'}, {'idle'}, 45, 0 \rangle \). Since in this resulting instance state it does not hold that \(\texttt {tmp} < 45\), transition turn_on #2
(and therefore the event turn_on
) fails. This failure models a crash of the component due to overheating. To make this restriction more explicit to the user of the component, a guard [this.temp
< 40]
can be added to turn_on #2
.2.5 Concerns
power
is referred to by both the region in the top part and the scope in the middle part. Parts can also interact with each other by synchronising on the same event. Synchronisation can occur whenever separate parts of an OIL specification contain transitions with the same event. When these transitions can fire and the corresponding event occurs, the transitions fire simultaneously, causing these separate parts to proceed simultaneously.POWER
, JOB
and HEAT
, shown after the event in the transition label. The two transitions of event turn_on
have different concerns, namely POWER
and HEAT
, which makes event turn_on
only allowed if both transitions can fire. This synchronisation enforces that the temperature increases every time the component is turned on. If we would not have had these concerns, both transitions could have fired independently of each other. A turn_on
event could then occur while the component is already on and only increase the temperature of the component.2.6 Scheduling and communication of events
sheet_printed
and \job_printed
are proactive, no other event is considered while any of these two are possible when the running example is executed with a runtocompletion scheduler. This causes the printer to not listen to the environment whenever it is busy printing a job. If we would not have a runtocompletion scheduler, it would for instance be possible to turn the printer off while it is busy printing. Note that if we would put scopes around the top region and bottom scope with the invariant \(\texttt {job} = {'idle'}\), the behaviour with or without runtocompletion scheduler would be the same.3 Formal preliminaries
3.1 Valuations and updates

for all assignments \(x := f \in U\): \(w(x) = \llbracket f \rrbracket v\),

in case there exists no assignment \(x := f \in U\) for variable x: \(w(x) = v(x)\).
3.2 Transition systems
4 Formal OIL semantics
4.1 Semantics of an OIL component specification

\(\mathbb {X} = \langle X, \mathcal {I} \rangle \) concerns the variables of the OIL specification, where

X is a set of variables. We partition X into a set of instance variables \(X_I\) and a set of parameters \(X_P\).

\(\mathcal {I} \in \mathbb {V}^{X_I}\) associates each instance variable with its initial value.


\(\mathbb {A} = \langle A, \sqsubset , \mathcal {RE}, \mathcal {EXP} \rangle \) concerns the areas of the OIL specification, where

A is a set of areas. We partition A into a set of regions \(A_{Re}\), a set of states \(A_{St}\) and a set of scopes \(A_{Sc}\).

\(\sqsubset \) is a partial order over A such that \(a \sqsubset a'\) iff \(a'\) is the parent area of a or \(a'\) is a super area of a.

\(\mathcal {RE} : A_{St} \rightarrow A_{Re}\) associates each state with the region it belongs to.

\(\mathcal {EXP} : A \rightarrow EXP_{X_I}\) associates each area a with an expression, which is a variable in \(X_I\) in case \(a \in A_{Re}\), a constant in \(EXP\) in case \(a \in A_{St}\) and a boolean expression in \(EXP_{X_I}\) in case \(a \in A_{Sc}\).


\(\mathbb {T} = \langle E, \mathcal {PAR}, T, \textit{CO}, \mathcal {CO} \rangle \) concerns the transitions of the OIL specification, where

E is a set of events. We partition E into a set of reactive events \(E_R\) and a set of proactive events \(E_P\). Additionally, we define \(E_H \subseteq E_P\) as the set of silent events.

\(\mathcal {PAR} : E \rightarrow \mathbb {P}(X_P)\) associates each event with a set of parameters.

\(T \subseteq A \times EXP_X \times E \times (X_P \nrightarrow EXP_{X_I}) \times \mathbb {P}(X_I \times EXP_X) \times A \times EXP_X^{old}\) is the set of transitions, where \(\nrightarrow \) indicates a partial function. For a transition \(\langle so, gu, e, \mathcal {ARG}, AG, ta, ar \rangle \in T\), so is its source area, gu is its boolean guard, e is its event, \(\mathcal {ARG}\) defines its arguments for parameters in \(\mathcal {PAR}(e)\), AG is its collection of assignments (an update), ta is its target area and ar is its boolean assert.

\(\textit{CO}\) is a set of concerns.

\(\mathcal {CO} : T \rightarrow \mathbb {P}(\textit{CO}) \setminus \{\emptyset \}\) associates each transition with a nonempty set of concerns. We define \(\mathcal {CO}\) also on sets of transitions: let \(T' \subseteq T\), then \(\mathcal {CO}(T') = \bigcup \limits _{t \in T'} \mathcal {CO}(t)\).

this.power
and \(\texttt {this.tmp} < 45\), respectively.job_printed
, which equals \(\texttt {this.power} = {'on'} \wedge \texttt {this.job} = {'busy'} \wedge \texttt {this.sheets} = 0\). The transition updates for transitions \(\texttt {turn\_on \#{}1}\) and \(\texttt {turn\_on \#{}2}\) are defined as \(\{\texttt {this.power} := {'on'}\}\) and \(\{\texttt {this.tmp} := \texttt {this.tmp} + 5\}\) respectively. The transition postconditions for transitions \(\texttt {turn\_on \#{}1}\) and \(\texttt {turn\_on \#{}2}\) are defined as \(\texttt {this.power} = {'on'}\) and \(\texttt {this.tmp} < 45\), respectively.turn_on
may only occur if both transitions can fire.
\(S = \mathbb {V}^{X_I}\), ,

\(s_0 = \mathcal {I}\),

\(I = \{e(p)\ \ e \in E_R \wedge p \in \mathbb {V}^{\mathcal {PAR}(e)}\}\), \(O = \{e(p)\ \ e \in E_P \setminus E_H \wedge p \in \mathbb {V}^{\mathcal {PAR}(e)}\}\), \(H = \{e(p)\ \ e \in E_H \wedge p \in \mathbb {V}^{\mathcal {PAR}(e)}\}\), \(L = I \cup O \cup H\),

such that for all \(s, s' \in S\) and \(e(p) \in L\), with \(v = s \cup p\):
fail
to indicate that a failure occurred. An event fails if the update is incompatible (\(\lnot CP(v, \mathcal {U}(T_e^v))\)) or if the transition postconditions are not met (\(\lnot \llbracket \mathcal {POC}(T_e^v) \rrbracket ^{v}_{v[\mathcal {U}(T_e^v)]}\)). Note that this IOLTS is deterministic. This is because all transitions in OIL with the same event that can fire are combined into one transition in the IOLTS.4.2 Execution semantics
5 Validity of OIL specifications
6 Translating OIL to mCRL2
6.1 mCRL2

\(S = \mathbb {V}^{\bar{d}}\),

\(s_0 \in \mathbb {V}^{\bar{d}}\) such that \(s_0(d_j) = \llbracket id_j \rrbracket \) for each \(1 \le j \le n\),

\(\xrightarrow {}\) is the transition relation such that for all \(s \in S\), \(i \in I\) and \(p \in \mathbb {V}^{\bar{e_i}}\) with \(v = s \cup p\):$$\begin{aligned} s \xrightarrow {a_i(\llbracket \bar{f_i} \rrbracket v)} \llbracket \bar{g_i} \rrbracket v \text { iff } \llbracket c_i \rrbracket v \end{aligned}$$
6.2 OIL in mCRL2
ISt
in the mCRL2 data specification, which defines a constructor IS
that accepts a tuple of expressions, representing values for the instance variables. We also add (data) type definitions of (instance) variables where necessary. Along with this structured sort we define projection functions \(\texttt {GET}_x\) to query the value of an instance variable x. We call an expression of type ISt
an instance struct. In mCRL2, an instance state is then represented with a ground instance struct, that is an instance struct without variables.power_type
and job_type
are defined separately. The initial instance state \(\langle {'off'}, {'idle'}, 20, 0 \rangle \) is represented in mCRL2 as the ground instance struct IS(power_off, job_idle, 20, 0)
.
s
, which translates each constant and operator to its mCRL2 counterpart and each \(x \in X_I\) to \(\texttt {GET}_x(\texttt {s})\). In case \(f \in EXP_X^{old}\) we define \(\sigma _\texttt {us}^\texttt {s}(f)\) for instance structs s
and us
, which translates each constant and operator to its mCRL2 counterpart and for each \(x \in X_I\), \(x^{old}\) to \(\texttt {GET}_x(\texttt {s})\) and x to \(\texttt {GET}_x(\texttt {us})\). To translate the evaluation of expressions to the context of mCRL2 too, we need to translate an evaluation over instance variables to a valuation over an instance struct variable. Given a valuation \(s \in \mathbb {V}^{X_I}\) and an instance struct variable s
, we define \(s_\texttt {s}\) as the valuation over \(\texttt {s}\) such that \(\llbracket \texttt {GET}_x(\texttt {s}) \rrbracket s_\texttt {s} = s(x)\) for all \(x \in X_I\).T
is the data type of x. The first parameter of type ISt
is the instance struct to be updated, the second parameter is a boolean expression that indicates whether the change should be applied and the third parameter of type \(\texttt {T}\) is the new value for x. The boolean parameter effectively makes this a conditional assignment. If this boolean parameter evaluates to true, the entry for x in the instance struct is overwritten with the new value, otherwise no changes are made. Why this boolean parameter is useful will be shown later on.s
some instance struct and \(\texttt {f}\) and \(\texttt {g}_1, .., \texttt {g}_n\) some mCRL2 expressions. Then, \(\texttt {SET}_{x_i}\) is defined with the following rewrite rules:power
of the running example, we define rewrite rules of the form: To update an instance struct s
with assignment \(\texttt {tmp} := \texttt {tmp} + 5\) we can use the mCRL2 expression SET_tmp(s, true, GET_tmp(s) + 5)
.
s
in a sequential way by nesting setter applications on the first parameter of the setters. To properly model a simultaneous update, we need to use the original instance struct s
to retrieve the values for instance variables in the righthand sides of assignments. In mCRL2, we generate this nesting as follows:s
be some instance struct, l be a list of pairs (b, u), where b is a boolean expression and u is an assignment to an instance variable. Then, the updated instance struct \(\mathcal {US}(l, \texttt {s})\) that results from applying the conditional assignments in l on s
is an mCRL2 expression constructed as follows:s
. The boolean parameter of the setters are used to make sure that exactly the assignments of transitions that fire are applied.turn_on
define the assignments \(\texttt {power} := {'on'}\) and \(\texttt {tmp} := \texttt {tmp} + 5\). If turn_on
would occur in an instance state s
, the resulting updated instance state, which corresponds to \(\mathcal {US}(\hat{U}(\texttt {turn\_on}), \texttt {s})\), is described in mCRL2 as follows: This update results in the instance struct equal to IS(power_on, GET_job(s), GET_tmp(s) + 5, GET_sheets(s))
. In case s
would be the initial instance struct IS(power_off, job_idle, 20, 0)
, the updated instance struct can be rewritten to IS(power_on, job_idle, 25, 0)
.
s
and us
be two instance structs that represent the state before, respectively, after an update. Then, the transition’s compatibility checks \(\mathcal {CP}(t, \texttt {s}, \texttt {us})\), the transition’s altered postcondition \(\mathcal {POC}(t, \texttt {s}, \texttt {us})\) and their combination \(\mathcal {PCP}(t, \texttt {s}, \texttt {us})\) under the assumption that the transition’s precondition holds are mCRL2 expressions constructed as follows:turn_on
, we add the compatibility checks GET_power(us) == power_off
and GET_tmp(us) == GET_tmp(s) + 5
, where s
and us
are the instance structs before, respectively, after updating.P
with an instance struct parameter to record the instance state and a boolean parameter which is false iff an event has failed. The body of process P
is a nondeterministic choice between a number of summands, one for each event in the OIL specification. Additionally, to model the failure state, we have a summand with a selfloop labelled with action fail
. We define \(\bar{p^e}\) as the vector of variables in \(\mathcal {PAR}(e)\) and \(\tau ^e\) as the data type of this vector for some event e.P
is a process defined with the LPE:lpssumelm
from the mCRL2 toolset can eliminate these auxiliary variables.P
of the running example, showing only the summand for the event turn_on
with auxiliary variables. On line 4 we define auxiliary variables f1
, f2
and us
, which represent the transition preconditions of the transitions turn_on #1
and turn_on #2
and the updated instance state respectively. This is done using the sum
operator to declare the variables, followed by conditions to fix their values (lines 45). The variables f1
and f2
are supplied to the setters so that only the updates of transitions that can fire are applied. The boolean b
and the concern condition are checked on line 6. On line 7 the action turn_on
is done and then the process recurses with the updated instance state and the postconditions. One could expect a compatibility check GET_tmp(us) == GET_tmp(s) + 5
here due to the update SET_tmp(.., f2, GET_tmp(s) + 5)
, but since there is only one assignment to tmp
defined for event turn_on
, this check is not necessary so it is left out.P
(Definition 26) where \(\texttt {P}(\texttt {is}, \texttt {true})\) describes the acceptor semantics of this OIL specification in mCRL2 (Definition 31). Then
.6.2.1 Execution semantics
s
some instance struct. Then the mCRL2 expression encoding the proactive priority condition \(\mathcal {PPC}(e, \texttt {s})\) is constructed as follows:sheet_printed
and \job_printed
are the only proactive events in the running example. Therefore, the proactive priority condition for the running example in some instance struct s
is defined in mCRL2 as:
P
(Definition 26) where \(\texttt {P}(\texttt {is}, \texttt {true})\) describes the execution semantics of this OIL specification in mCRL2 (Definition 33). Then
.6.3 Implementation of the translation to mCRL2
7 Validation of OIL specifications
7.1 Mucalculus
7.2 Checking the validity requirements
7.2.1 Safe lookaheadlessness
fail
. This requirement can be formalised in the mucalculus with the formula \(\phi _{R1} = [L^*][O \cup H][\texttt {fail}]false\).7.2.2 Finite proactivity
7.2.3 Confluent proactivity
7.2.4 Predictable proactivity
7.2.5 Alternative methods of checking confluent and predictable proactivity
8 Experiments
mcrl22lps
(and use txt2lps
instead).8.1 The EPC case
R1  R2  R3  R4  

EPC  0.4  0.4  0.4  0.4 
AGA  13  12  21  22 
8.2 The AGA case

We gave event parameters of reactive events with an infinite domain a fixed value. These parameters represent values received from the environment. In case such a parameter has an infinite domain, there would be an infinite number of transitions possible in the LTS, which causes the generation of the LTS to not terminate. Since the values of these parameters were only used to be passed on to other components, this change does not affect the control flow behaviour of the model.

We removed the assignments to instance variables that are at most only used to pass information on to other components. This keeps these variables at their initial values, which avoids creating multiple branches in the LTS for each value. Note that this effectively abstracts away some event parameters in proactive events, used to pass this information back to the environment. This is not an issue, since these branches are behaviourally the same except for the value for the instance variable and such event parameters and since we are (for now) only concerned with the behaviour of a single component.

We added assignments to reset instance variables to their initial value after their value becomes irrelevant. This makes the branches in the LTS that represent different values for this variable converge earlier.
start
represents the event at the beginning of the loop. Checking this formula on the AGA model results in false, which is due to events in the loop that are deliberately put in the model to model a failure in the system. Removing these events from L and checking the formula again results in true. These formulae can be checked on the reduced LTS within a few seconds.9 Discussion of results
9.1 Process structure
9.2 Automating Preprocessing
lpsparelm
and lpsstategraph
[34]. However, experiments have shown that these tools are not very effective on mCRL2 specifications generated from OIL specifications. This is due to our monolithic representation of the instance state. To make these tools more effective, the structure of the generated mCRL2 will have to be redesigned or the tools have to be improved.