products/sources/formale sprachen/VDM/VDMSL/EngineSL/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: engine.vdmsl   Sprache: VDM

Original von: VDM©
types

ValvePos = <open> | <closed>;

SwitchPos = <on> | <off>;

StartAttempt = nat
inv s == s <= DVMAXNUMBERATTEMPTS;

StartState = <FuelSwitchAtCut> | 
             <StartCommanded> |
             <WaitForFuelOnConditions> |
             <WaitForLightUp> |
             <WaitForStarterOnConditions> |
             <WaitForIdle> |
             <EngineStarted> |
             <CoolAndFlushCycle> |
             <AttemptAborted> | 
             <SequenceAborted>;
             
values

DVMINN2GNDFOC : real = 26;

DVMINTGTGNDFOC : real = 100;

DVATORABOVEIDLE : real = 55;

DVMAXNUMBERATTEMPTS : int = 2;

DVHOTSTART : real = 305;

DVMAXLIGHTWAITTIME : int = 180;

STATEMAP = {1 |-> <FuelSwitchAtCut>, 
            2 |-> <StartCommanded>,
            3 |-> <WaitForStarterOnConditions>,
            4 |-> <WaitForFuelOnConditions>, 
            5 |-> <WaitForLightUp>,
            6 |-> <WaitForIdle>,
            7 |-> <EngineStarted>,
            8 |-> <CoolAndFlushCycle>,
            9 |-> <AttemptAborted>,
            10 |-> <SequenceAborted>}
            
state StartingSystem of
  sstate : StartState
  startswitch : SwitchPos
  fuelswitch : SwitchPos
  n2 : real
  aog : bool
  starteron : bool
  sov : ValvePos
  lit : bool
  ignon : bool  
  startcomplete : bool
  startaborted : bool
  attempt : StartAttempt
  lightuptimer : int
  coolflushcmd : bool
  stalldet : bool
  ign_flt : bool
  sov_flt : bool
  starter_flt : bool
  n2_flt : bool
  tgt_flt : bool
init ss == 
  ss = mk_StartingSystem (<FuelSwitchAtCut>, <off>, <off>, 0, true,
                          false, <closed>, false, false, false, false, 
                          0, 0, false, false, false, false, false, false, 
                          false)
end

functions

LightUpDetect : real -> bool
LightUpDetect (tempTGT) ==
  tempTGT > DVMINTGTGNDFOC;

FOCDetect : SwitchPos * SwitchPos * real * bool -> bool
FOCDetect (fuelswitch, startswitch, n2, aog) ==
  (fuelswitch = <on>) and
  (startswitch = <on>) and
  (n2 > DVMINN2GNDFOC) and
  aog;
  
ReturnState : int -> StartState
ReturnState (i) ==
  STATEMAP (i);

LightupTimeOutDetect : int -> bool
LightupTimeOutDetect (lightuptimer) ==
  lightuptimer > DVMAXLIGHTWAITTIME;

GroundFailureDetected : bool * bool * bool * bool * bool * real -> bool
GroundFailureDetected (ign_flt, starter_flt, sov_flt, n2_flt, tgt_flt, n2) ==
  ign_flt or starter_flt or sov_flt or n2_flt or
  tgt_flt or(n2 > DVMINN2GNDFOC)
  
operations

StarterOn () 
ext rd sstate : StartState
    rd startswitch : SwitchPos
    rd aog : bool
    wr starteron : bool
    rd fuelswitch : SwitchPos
pre (fuelswitch = <on>) and (startswitch = <on>) and aog
post starteron;

StarterOff () 
ext rd startswitch : SwitchPos
    rd lit : bool
    wr starteron : bool
pre startswitch = <off> or lit
post not starteron;

OpenSOV () 
ext rd startswitch : SwitchPos
    rd fuelswitch : SwitchPos
    rd n2 : real
    rd aog : bool
    wr sov : ValvePos
pre startswitch = <on> and 
    FOCDetect (fuelswitch, startswitch, n2, aog)
post sov = <open>;

IgnOn (tempTGT : real) 
ext rd sov : ValvePos
    wr ignon : bool
pre (sov = <open>) and not LightUpDetect(tempTGT)
post ignon;

IgnOff (tempTGT : real) 
ext rd sov : ValvePos
    wr ignon : bool
pre (sov = <open>) and LightUpDetect (tempTGT)
post not ignon;

StartComplete (tempTGT : real) 
ext rd n2 : real
    wr startcomplete : bool
pre LightUpDetect (tempTGT) and
    (n2 > DVATORABOVEIDLE)
post startcomplete;

SequenceAbort () 
ext rd fuelswitch : SwitchPos
    wr attempt : StartAttempt
    wr startaborted : bool
    rd starter_flt : bool
    rd ign_flt
    rd sov_flt
    rd n2_flt
    rd tgt_flt
    rd n2
pre GroundFailureDetected (ign_flt, starter_flt, sov_flt, n2_flt, tgt_flt, n2) or
    (fuelswitch = <off>) or
    (attempt >= DVMAXNUMBERATTEMPTS)
post startaborted and (attempt = 0) ;

CoolFlush (tempTGT : real)
ext rd lightuptimer : int
    rd coolflushcmd : bool
    rd stalldet : bool
    wr attempt : StartAttempt
pre LightupTimeOutDetect (lightuptimer) and coolflushcmd or
    (tempTGT > DVHOTSTART) or stalldet
post (attempt = attempt~ + 1)

¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff