Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMSL/SAFERSL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 1 kB

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.11 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.