Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: tracker.vdmsl Sprache: VDM

Original von: VDM^©

types

Tracker :: containers : ContainerInfo
           phases     : PhaseInfo
  inv mk_Tracker(containers,phases) ==
    Consistent(containers,phases) and
    PhasesDistinguished(phases) and
    MaterialSafe(containers,phases);

ContainerInfo = map ContainerId to Container;

PhaseInfo = map PhaseId to Phase;

Container :: fiss_mass : real
             material  : Material;

Phase :: contents          : set of ContainerId
         expected_materials: set1 of Material
        capacity          : nat
inv p == card p.contents <= p.capacity;

ContainerId = token;

PhaseId = token;

Material = token

functions

-- introduce a new container to the plant (map union)

  Introduce : Tracker * ContainerId * real * Material -> Tracker
  Introduce(trk, cid, quan, mat) ==
     mk_Tracker(trk.containers munion
                {cid |-> mk_Container(quan, mat)},
                trk.phases)
  pre cid not in set dom trk.containers;

-- permission to move (simple Boolean function)

Permission: Tracker * ContainerId * PhaseId  ->  bool
Permission(mk_Tracker(containers, phases), cid, dest) ==
    cid in set dom containers and
    dest in set dom phases and
    card phases(dest).contents < phases(dest).capacity and
    containers(cid).material in set phases(dest).expected_materials;

-- Remove a container from the contents of a phase

Remove: Tracker * ContainerId * PhaseId -> Tracker
Remove(mk_Tracker(containers, phases), cid, source) ==
  let pha = mk_Phase(phases(source).contents \ {cid},
                     phases(source).expected_materials,
                     phases(source).capacity)
  in
    mk_Tracker(containers, phases ++ {source |-> pha})
pre source in set dom phases and
    cid in set phases(source).contents;

-- move a known container between two phases

Move: Tracker * ContainerId * PhaseId * PhaseId -> Tracker
Move(trk, cid, ptoid, pfromid) ==
  let cont = trk.phases(ptoid)
  in
   let pha = mk_Phase(cont.contents union {cid},
                      cont.expected_materials,
                      cont.capacity)
   in
     mk_Tracker(trk.containers,
                Remove(trk,cid,pfromid).phases ++
                {ptoid |-> pha})
pre Permission(trk, cid, ptoid) and
    pre_Remove(trk,cid,pfromid);

-- delete a container from the plant

Delete: Tracker * ContainerId * PhaseId  ->  Tracker
Delete(tkr, cid, source) ==
   mk_Tracker({cid} <-: tkr.containers,
              Remove(tkr, cid, source).phases)
pre pre_Remove(tkr,cid,source);

-- Auxiliary functions defined for inv-Tracker
  Consistent: ContainerInfo * PhaseInfo -> bool
  Consistent(containers, phases) ==
     forall ph in set rng phases &
        ph.contents subset dom containers;

  PhasesDistinguished: PhaseInfo -> bool
  PhasesDistinguished(phases) ==
     not exists p1, p2 in set dom phases &
        p1 <> p2 and
        phases(p1).contents inter phases(p2).contents <> {};

  MaterialSafe: ContainerInfo * PhaseInfo -> bool
  MaterialSafe(containers, phases) ==
     forall ph in set rng phases &
        forall cid in set ph.contents &
    cid in set dom containers and
           containers(cid).material in set ph.expected_materials

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.