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