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