Information Technology Reference
In-Depth Information
or
lowered
by the motor and when the gate is
moved
. These derived properties
will form our vocabulary for discussing motor properties. They can be used
throughout the specification to simplify its presentation. The property that the
gate is
moved
includes the time motor decel over which it is decelerated when
the motor is turned off.
lifted
=
λ t
:
Time
•
motor
(
t
)=on
∧
dir
(
t
)=up
lowered
=
λ t
:
Time
•
motor
(
t
)=on
∧
dir
(
t
)=down
moved
=
λ t
:
Time
•
(
∃
J
:
Interval
(
Time
)
•
sup
(
J
)=
t
∧
#
J
≤
motor decel
∧
(
motor
= on)
in
J
)
The supremum,
sup
(
J
), of a set of times
J
is the least upper bound of
J
,andthe
infimum,
inf
(
J
), is the greatest lower bound. A predicate,
P
,holdswithinaset
of times
J
, written
P
in
J
, if there exists a time within
J
at which
P
holds. We
also introduce an ordering,
lower
, on the gate position and its reflexive transitive
closure,
lower
∗
. This allows us to express the property that the gate is either
rising (monotonically upwards) or falling (monotonically downwards).
lower
{
closed
→
neither
,
neither
→
open
}
monotonic up
=
=
λ I
:
Interval
(
Time
)
•
lower
∗
(
pos
(
t
1
)
, pos
(
t
2
))
∀
t
1
, t
2
:
I
•
t
1
≤
t
2
⇒
monotonic down
=
λ I
:
Interval
(
Time
)
•
lower
∗
(
pos
(
t
2
)
, pos
(
t
1
))
∀
t
1
, t
2
:
I
•
t
1
≤
t
2
⇒
If the motor has been on in the direction up for at least some constant uptime,the
gate will have reached the open position. A similar condition applies for downward
travel.
8
The gate remains stationary after the motor has been turned off for time
motor decel. After the motor has been turned off the gate can only continue
its travel in the direction in which it was going (for at most motor decel). In
the definition, an interval
I
adjoins an interval
J
, written
I
adjoins
J
,ifthe
supremum of
I
is equal to the infimum of
J
, i.e.
sup
(
I
)=
inf
(
J
). Infix relations,
such as
adjoins
, bind more tightly than binary logical operators.
MotorOperation
=
λ T
:
Interval
(
Time
)
•
∀
I
:
Interval
(
T
)
•
((
lifted
∧
pos
= open)
over
I
⇒
#
I
≤
uptime)
∧
((
lowered
∧
pos
= closed)
over
I
⇒
#
I
≤
downtime)
∧
¬
moved
)
over
I
)
⇒
∃
p
:
Height
•
(
pos
=
p
)
over
I
))
(((
(
∧
∀
I , J
:
Interval
(
T
)
•
I
adjoins
J
⇒
(
lifted
over
I
∧
(
motor
= off)
over
J
⇒
monotonic up
(
I
∪
J
))
(
lowered
over
I
∧
(
motor
= off)
over
J
⇒
monotonic down
(
I
∪
J
))
8
Because we chose to describe
pos
as having only three values, rather than giving it a
numeric value, we now naturally describe the gate's speed of movement only in terms
of the travel time between the extreme positions.
Search WWH ::
Custom Search