Information Technology Reference
In-Depth Information
(
∀
r:Run
•
equiv(
γ
(r), r,
ρ
))
)
pre dom
ρ
= iovars(iots1)
∧
rng
ρ
= iovars(iots2),
→
iovars : IOTS
Var
-set
≡{
|
∈
∧
∈{
}}
iovars(iots)
v
v:Var
•
v
vars(iots)
mode(v)
IN,OUT
,
For the identity variable mappings
id
we just write
equiv
(
iots
1
,iots
2) rather
than
equiv
(
iots
1
,iots
2
,id
).
7.4
IOTS Transformation Rules
We have developed a collection (see [30]) of transformation rules between IOTS
patterns and proved by hand that any instance of the rules gives rise to a transfor-
mation that preserves I/O behaviour. The RSL formulation of the IOTS concepts
in previous section now makes it possible to make the proofs formal.
l0
l0
<=>
g / x := x+1
g / y := x
l3
l1
y := y+1
l2
x := y
l3
Fig. 5.
A transformation rule
As an example, there is a rule stating that an IOTS
iots
1 can be transformed
into an equivalent IOTS
iots
2 by replacing the transition shown on the left hand
side of Fig. 5 with the three transitions shown on the right hand side of Fig. 5,
or vice versa, provided that (1)
l
1and
l
2 are not locations of
iots
1,
x
and
y
are
local variables, and (2) in any path emanating from location
l
3, the variable
y
is assigned before read. The rule is generic in locations
l
0,
l
1,
l
2,
l
3, variables
x
and
y
, and, guard
g
.
Proving this rule correct, amounts to prove:
∀
iots1, iots2 : IOTS, l0, l1, l2, l3 : Loc, g : Guard, x, y : Var
•
{
x, y
}⊆
vars(iots1)
∧
mode(x) = PROC
∧
mode(y) = PROC
∧
{
l0, l3
}⊆
locs(iots1)
∧
l1
∈
locs(iots1)
∧
l2
∈
locs(iots1)
∧
(l0, g, mk Assign(
(x, mk Sum(mk Var(x), mk Const(1)))
), l3)
∧
vars(iots2) = vars(iots1)
∈
trans(iots1)
∧
initstate(iots2) = initstate(iots1)
∧
locs(iots2) = locs(iots1)
∪{
l1, l2
}∧
Search WWH ::
Custom Search