|
\begin{vdm_al}
module SAFER
imports from AUX all,
from HCM all,
from TS all,
from AAH all
exports all
definitions
state SAFER of
clock : nat
init s ==
s = mk_SAFER(0)
end
operations
ControlCycle: HCM`SwitchPositions * HCM`HandGripPosition * AUX`RotCommand ==>
TS`ThrusterSet
ControlCycle(mk_HCM`SwitchPositions(mode,aah),raw_grip,aah_cmd) ==
let grip_cmd = HCM`GripCommand(raw_grip,mode),
thrusters = TS`SelectedThrusters(grip_cmd,aah_cmd,AAH`ActiveAxes(),
AAH`IgnoreHcm())
in
(AAH`Transition(aah,grip_cmd,clock);
clock := clock + 1;
return thrusters)
post card RESULT <= 4 and
ThrusterConsistency(RESULT)
functions
ThrusterConsistency: set of TS`ThrusterName +> bool
ThrusterConsistency(thrusters) ==
not ({<B1>,<F1>} subset thrusters) and
not ({<B2>,<F2>} subset thrusters) and
not ({<B3>,<F3>} subset thrusters) and
not ({<B4>,<F4>} subset thrusters) and
not (thrusters inter {<L1R>,<L1F>} <> {} and
thrusters inter {<R2R>,<R2F>} <> {}) and
not (thrusters inter {<L3R>,<L3F>} <> {} and
thrusters inter {<R4R>,<R4F>} <> {}) and
not (thrusters inter {<D1R>,<D1F>} <> {} and
thrusters inter {<U3R>,<U3F>} <> {}) and
not (thrusters inter {<D2R>,<D2F>} <> {} and
thrusters inter {<U4R>,<U4F>} <> {})
end SAFER
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
