Quelle safer.vdmsl Sprache: VDM

\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}

quality100%

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.