Quelle NextMoveController.vdmrt Sprache: VDM

class NextMoveController

instance variables
obs : map Grid`Point to Grid`PointAvalibility;
mobs : set of MovingObstacle := {};
thread
-- periodic (period,jitter,delay,offset) (operation
periodic(2500E6,1,0,0)( LocateMovingObstacles);

sync
--check before move
mutex (SetObs, IsPointBlocked);

-- no simultanious calls
mutex (SetObs);
mutex (WaitForAvalibility);

mutex (LocateMovingObstacles);
mutex (GetNextPoint);
per GetNextPoint => #fin(LocateMovingObstacles) > #fin(GetNextPoint);
per IsPointBlocked => #fin(SetObs) > #fin(IsPointBlocked);

operations

public NextMoveController: () ==> NextMoveController
NextMoveController () ==
(
   skip;
);

public AddMovingObsticle : MovingObstacle ==> ()
AddMovingObsticle(mo) ==
   mobs := mobs union {mo};

private LocateMovingObstacles : () ==>()
LocateMovingObstacles() ==
duration(100)
(

    let m = { mo.GetPos()|-><Occupied> | mo in set mobs} in
     SetObs(m);
);

private SetObs: map Grid`Point to Grid`PointAvalibility ==> ()
SetObs(mp) ==
  (
   obs := { |->};
   -- remove old data could be replaced by using the thread
   -- id of the thread
   obs := obs ++ mp
);

private WaitForAvalibility: Grid`Point ==> ()
WaitForAvalibility(p) ==
   while IsPointBlocked(p) do
    (
     Util`PrintDebug("Waiting for obstacle on pos:");
     Util`PrintValue(p);
     Util`PrintInt(time);

     skip;
   );

private IsPointBlocked: Grid`Point ==> bool
IsPointBlocked(p) ==
(

          Util`PrintDebug("Requesting Pos");
          Util`PrintValue(p);
          Util`PrintDebug("Mobs");
          for all mo in set dom obs do
            Util`PrintValue(mo);

if p in set dom obs then
Util`PrintDebug("in")
else
Util`PrintDebug("not");

   return p in set dom obs;
);

public GetNextPoint : set of Grid`Point * Grid`Point ==> [Grid`Point]
GetNextPoint(neighbours, dest) ==
   let tmp : set1 of Grid`Point ={p| p in set neighbours
             & not exists q in set neighbours &
                      Distance(p, dest) > Distance(q, dest)}
    in
      for all p in set tmp
        do
        (

          WaitForAvalibility(p);


           return p
        )
pre card neighbours > 0;

functions

  Distance: Grid`Point * Grid`Point -> nat
  Distance(p1, p2) ==
    def a = (p2.X-p1.X)* (p2.X-p1.X) + (p2.Y-p1.Y)* (p2.Y-p1.Y)
      in
        if 0<= a then
          floor(MATH`sqrt(a))
        else
           0;

end NextMoveController

class NextMoveControllerTest is subclass of TestCase
values

operations
protected SetUp: () ==> ()
SetUp () == skip;

protected RunTest: () ==> ()
RunTest () == skip;

  protected TearDown: () ==> ()
TearDown () == skip

end NextMoveControllerTest

quality85%

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