Robust/src/Benchmarks/mlp/directto/README.txt

   1 Any statement *** in asterix *** is an assertion that
   2 disjoint reachability analysis should be able to verify.
   3
   4 The DirectTo benchmark executes a list of messages from
   5 an input file to solve a safe aircraft routing problem.
   6
   7 The D2 (direct-to) singleton object has a singleton
   8 reference to:
   9  -ReadWrite, reads input file, creates messages
  10  -MessageList, commands to execute for building problem
  11  -Static, structure of static constants from input file
  12  -AircraftList, all types of aircraft in problem
  13  -FlightList, list of flights in algorithm
  14  -FixList, list of fixes algorithm computes
  15  -Algorithm, reads from Static
  16  -TrajectorySynthesizer, reads from Static
  17  -Flight, why a singleton Flight object?
  18 so:
  19 *** all memory in the program should be reachable from
  20 at most one of any singleton (D2, Static, etc) ***
  21
  22 MessageList has a Vector of Message objects, where each
  23 one specifys an effect for other structures such as
  24 setting a constant in the Static singleton, or adding
  25 an aircraft type to the Aircraft list, etc.  Message
  26 objects themselves only have references that are freshly
  27 allocated, so:
  28 *** Message objects should be disjoint ***
  29
  30 The ReadWrite singleton appends new Message objects
  31 to the MessageList and has no references of its own,
  32 *** Nothing is reachable from a ReadWrite ***
  33
  34 The Static singleton has primitive members, so
  35 *** Nothing is reachable from a Static ***
  36
  37 AircraftList has a Vector of Aircraft objects, where
  38 each one has a String for type and some primitive
  39 attributes, where the type is generated from a
  40 StringTokenizer (getting a token gets a new String),
  41 and in practice is disjoint for every Aircraft, so:
  42 *** Aircraft objects should be disjoint ***
  43
  44 FixList has a Vector of Fix objects, where each one
  45 has a String name and a Point2d (an alternate point
  46 in a flight plan?).  I believe they are not modified
  47 after being built from freshly allocated tokenizing,
  48 *** Fix objects should be disjoint ***
  49
  50 FlightList has a Vector of Flight objects which have
  51 several fresh, set-once references (flightID String,
  52 a Track, etc).
  53 Flight objects may share Aircraft (types),
  54
  55
  56
  57 In Message.executeMessage(), if you comment out every
  58 message handler except any one of these, they cause
  59 Message objects to show sharing:
  60  - FlightList.addFlightPlan()
  61  - FlightList.amendFlightInfo()
  62  - FlightList.amendFlightPlan() (still a quick analysis!)
  63  - FlightList.sendingAircraft()