Information Technology Reference
In-Depth Information
conf
e, en : e ∈ s.evt ∧¬ ( en ∈ s.evt ) do
newevt ( en, s );
newgrd ( en, e.guard )
newact ( en, e.action );
conf g : g ∈ PRED ∧ FV ( g ) ⊆ s.var
do newgrd ( e, g ) newgrd ( en, ¬g ) end
end
The pattern configuration requires three parameters. Parameter e refers to the event to
be refined from the input model s , en is some fresh event name, and g is a predicate on
the model variables.
The pattern is applicable to models with at least one event. The result is a model with
an additional event and a constrained guard of the original event. As an input model for
this model we use the model from the previous example.
MACHINE m 1
VARIABLES x
INVARIANT x
Z
INITIALISATION x := 0
EVENTS
count = WHEN x mod 2 = 0 THEN x := x +1 END
inc = WHEN
¬ ( x mod 2 = 0) THEN x := x +1 END
Here, the pattern parameters are instantiated as follows: e as count , en as inc ,and x as
x mod 2 = 0 .
4
Pattern Composition
In the previous section we defined the notion of a basic transformation rule as a combi-
nation of the applicability conditions, transformation (effect) function, and refinement
proof obligations. Moreover, In Figure 1, we also introduced various composition con-
structs for creating complex transformation rules. In this section we will show how
we can inductively define the applicability conditions, effect, and proof obligations for
composed rules.
4.1
Rule Applicability Conditions
For a basic rule, the rule applicability condition is defined in its context clause. For
more complex rules constructed using the proposed language of transformation rules,
rule applicability is derived inductively according to the following definition:
app ( basic )( c, s ) = context ( basic )( c, s )
app ( p ; q )( c, s ) = app ( p )( c, s ) app ( q )( c, eff ( p )( c, s ))
app ( pq )( c, s ) = app ( p )( c, s ) app ( q )( c, s )
inter ( scope ( p ) , scope ( q )) =
app ( if G ( c, s ) then p end )( c, s ) = G ( c, s ) app ( p )( c, s )
app ( conf i : Q ( i, c, s ) do p ( i ) end )( c, s )= ∀ i · Q ( i, c, s ) app ( p ( i ))( c, s )
app ( par i : Q ( i, c, s ) do p ( i ) end )( c, s )= app ( conf i : Q ( i, c, s ) do p ( i ) end )( c, s )
∀ i, j · Q ( i, c, s ) ∧ Q ( j, c, s ) ∧ i = j ⇒
inter ( scope ( p ( i )) , scope ( p ( j ))) =
Search WWH ::




Custom Search