|
types
Trace = seq of [Event];
Event = <A> | <V>;
state Pacemaker of
aperiod : nat
vdelay : nat
init p == p = mk_Pacemaker(15,10)
end
operations
Init: nat * nat ==> ()
Init(aperi,vdel) ==
(aperiod := aperi;
vdelay := vdel);
IdealHeart: () ==> Trace
IdealHeart() ==
return [ if i mod aperiod = 1
then <A>
elseif i mod aperiod = vdelay + 1
then <V>
else nil
| i in set {1,...,100}];
FaultyHeart() tr : Trace
post len tr = 100 and
Periodic(tr,<A>,aperiod) and
not Periodic(tr,<V>,aperiod);
functions
Periodic: Trace * Event * nat1 -> bool
Periodic(tr,e,p) ==
forall t in set inds tr &
(tr(t) = e) =>
(t + p <= len tr =>
((tr(t+p) = e and
forall i in set {t+1, ..., t+p-1} & tr(i) <> e))
and
(t + p > len tr =>
forall i in set {t+1, ..., len tr} & tr(i) <> e));
values
wrongTR: Trace = [<A>, nil, <V>, nil, nil, <A>, nil, nil, nil, nil ];
operations
Pace: Trace * nat1 * nat1 ==> Trace
Pace(tr,aperi,vdel) ==
return [nil] ^
[ if (i mod aperi = vdel + 1) and tr(i) <> <V>
then <V>
else nil
| i in set inds tl tr];
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
