Information Technology Reference
In-Depth Information
An
I/O restriction
of a run is the restriction of the run to pairs where the lo-
cation is an input or output location, and for these pairs the states are restricted
to input and output variables only:
IOrestrict : Run
→
Run
IOrestrict(r)
≡
(l,
σ
/
{
v
|
v:Var
•
mode(v)
∈{
IN,OUT
}}
)
|
(l,
σ
)
in
r
•
mode(l)
∈{
IN,OUT
}
,
An
I/O map ρ
is a bijective, mode preserving variable mapping between I/O
variables:
type
IOMap =
{|
ρ
:Var
m
Var
•
bijective(
ρ
)
∧
IOmodepreserving(
ρ
)
|}
value
bijective : (Var
m
Var)
→
Bool
bijective(
ρ
)
≡
∀
∈
rng
ρ
⇒
∃
∈
dom
ρ
∧
ρ
(v1) = v2)),
(
v2 : Var
•
v2
(
!v1:Var
•
v1
m
Var)
→
IOmodepreserving : (Var
Bool
IOmodepreserving(
ρ
)
≡
(
∀
⇒
IOmode(
ρ
(v)) = mode(v)
v:Var
•
v
∈
dom
ρ
∧
mode(v)
∈{
IN,OUT
}
)
Two runs are
I/O equivalent
wrt. an I/O map if their I/O restrictions have
(1) the same length, (2) the same order of input locations and output locations,
and (3) their states agree on input variables and output variables modulo the
I/O map:
equiv : Run
×
Run
×
IOMap
→
Bool
equiv(r1, r2,
ρ
)
≡
let
r1 io = IOrestrict(r1), r2 io = IOrestrict(r2)
in
len
r1 io =
len
r2 io
∧
(
∀
j:
Int
•
⇒
let
(l1,
σ
1) = r1 io(j), (l2,
σ
2) = r2 io(j)
in
mode(l1) = mode(l2)
j
>
0
∧
j
≤
len
r1 io
∧
σ
1=
σ
2
◦
ρ
end
)
end
,
Finally, we can define two IOTS'es to be
I/O behavioural equivalent
wrt. an
I/O map, if there is a bijection
γ
between I/O equivalent runs of the two IOTS'es:
IOMap
∼
equiv : IOTS
×
IOTS
×
→
Bool
equiv(iots1, iots2,
ρ
)
≡
(
∃
m
Run
•
dom
γ
= eval(iots1)
γ
:Run
∧
rng
γ
= eval(iots2)
∧
(
∀
r1, r2 : Run
•
r1
=r2
⇒
γ
(r1)
=
γ
(r2))
∧
Search WWH ::
Custom Search