Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: InductionController.vdmpp Sprache: VDM

Original von: VDM^©

-- ===============================================================================================================
-- InductionController in tray allocation for a sortation system
-- By José Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class InductionController
types

values
  public InductionRate : nat = 2;     -- trays between each item

instance variables
  priority : nat := 0;    -- priotity of induction, incremented each time wait to induct item
  id : nat1;       -- Induction ID
  allocator : TrayAllocator;    -- TrayAllocator
  items : seq of Item := [];   -- set of items ready to be inducted
  stepCount: nat := 0;     -- Counts the number of steps between inducting items

  -- If induction is waiting there must be items in sequence
  inv priority > 0 => len items > 0;

operations

    -- InductionController constructor
public InductionController: TrayAllocator * nat ==> InductionController
InductionController(a, n) ==
(
  allocator := a;
  id := n;
);

-- Returns induction controller UID
pure public GetId: () ==> nat
GetId() ==
  return id;

-- Returns priority of induction controller
public GetPriority: () ==> nat
GetPriority() ==
  return priority;

-- Returns true if induction is wating with an item
public IsItemWaiting: () ==> bool
IsItemWaiting() ==
  return priority > 0;

-- Get size of waiting item in number of trays
public GetSizeOfWaitingItem: () ==> nat
GetSizeOfWaitingItem() ==
  if not IsItemWaiting()
  then
   return 0 -- No waiting items
  else
   let item = hd items
    in item.GetSizeOfTrays();

    -- Enviroment feeds a new item on induction
public FeedItem: Item ==> ()
FeedItem(i) ==
  items := items ^ [i];

    -- Simulate sorter-ring moved one tray step
public TrayStep: () ==> ()
TrayStep() ==
(
  -- Induct next item based on InductionRate
  stepCount := stepCount + 1;
  if IsItemWaiting() or (stepCount >= InductionRate)
  then
  (
   InductNextItem();
   stepCount := 0;
  )
);

-- It any items on induction then induct next item
-- If next item could be inducted then removed it from the head of item sequence
-- If item could not be inducted then increment priority
    private InductNextItem: () ==> ()
    InductNextItem() ==
  let n = len items
  in
   if n > 0
   then
    let item = hd items
      in
       if allocator.InductItem(self, item)
       then
        (
      atomic -- Due to invariant
      (
          items := tl items;
          priority := 0
         );
        )
       else
         priority := priority + 1; -- Increment priority wait counter

functions

sync

--thread

traces

end InductionController

¤ Dauer der Verarbeitung: 0.16 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.