hostside/resolve.c

   1 /*
   2  * resolve detected trains into initial state
   3  */
   4 /*
   5  * Algorithm:
   6  *
   7  *  Notation and background:
   8  *
   9  *      S                       set of segments
  10  *      D \subset S             set of segments where we have detection
  11  *
  12  *      T                       set of trains
  13  *      H(t) \subset S          home range for train t \elem T
  14  *      E(t) \subset S          set of segments where train t last expected
  15  *
  16  *      H(t) \disjoint H(t')   for t != t'
  17  *      E(t) \disjoint E(t')   for t != t'
  18  *      but not necessarily E(t) \disjoint H(t')
  19  *
  20  *  We want to find a mapping R(t)
  21  *      R(t) \elem { N, E, H }          t \elem T,  N(t') = \null
  22  *  giving
  23  *      A(t) = (R(t))(t)                segments allocated to train t
  24  *      U = \union_{t} A(t)
  25  *  satisfing
  26  *      A(t) \disjoint A(t')              for t != t'   `disjoincy'
  27  *      D \subset U                                     `coverage'
  28  *  and the solution is somehow optimal or at least not badly suboptimal.
  29  *
  30  * We compute R incrementally, maintaining disjoincy,,
  31  * while increasing U.  At each stage R is an optimal solution
  32  * to the problem posed by D' = U, and we maintain this invariant.
  33  *
  34  * We define an optimality ordering on R by counting occurrences of
  35  * H, E, and H in the range, in that order.  Ie,
  36  *      Count(R,x) = |{ t: R(t) = x }|
  37  *      Rank(R) = Count(R,H) * (|T|+1) + Count(R,E)
  38  * and compare Ranks numerically, lower being better.
  39  *
  40  * So we mean that for any incrementally computed R, there is no
  41  * R' satisfying the same subproblem D' = U for which Rank(R') < Rank(R).
  42  *
  43  * For the benefit of client programs, we record the key elements of
  44  * the proofs that we generate for non-N values of R.
  45  *
  46  *  1.  Initially we set \all_{t} R(t) = N.
  47  *
  48  *      Optimality: This is minimal for U = \null, as Rank(R) = 0.
  49  *
  50  *  2.  Then we search for lack of coverage, ie violations of D \subset U.
  51  *      If none are found we are done.
  52  *
  53  *  3.  Let  d \elem D  but  d !\elem U.
  54  *      We will now calculate new R which we will call R2
  55  *      giving new U which we will call U2.
  56  *
  57  *  3a. Hope that  \exists{t} st d \elem E(t)  with
  58  *      E(t) \disjoint U  and  R(t) = N.
  59  *      If so set R2(t) = E giving a solution to U2.
  60  *
  61  *      Optimality: if d \elem D then we need U2 to include d.
  62  *      That means d \elem E(t) or d \elem H(t').  No E(t')
  63  *      other than E(t) can help since they are disjoint, and
  64  *      we would certainly prefer adding E(t) to adding H(t').
  65  *      (Adding H(t') and removing some other H(t'') doesn't
  66  *      work either because the Hs are disjoint, so no
  67  *      H can stand in for any other.)
  68  *
  69  *      So the rank increase by 1 is is minimal for U2.
  70  *
  71  *      Proof elements: R(t) = E is demonstrated by
  72  *      every d meeting these conditions.
  73  *
  74  *  3b. Alternatively, hope that  d \elem H(t')
  75  *
  76  *      If so set  R2(t') = H
  77  *                 \all_{t+} R2(t+) = N where R(t+) = E.
  78  *
  79  *      Optimality: in the case we are now dealing with, we
  80  *      didn't succeed with the test for 3a, so either:
  81  *
  82  *      (i)  There is no t where d \elem E(t), so R(t') = H is
  83  *           essential because no solution without R(t') = H has d \elem U2.
  84  *
  85  *      (ii) There is t where d \elem E(t) but R(t) = H.
  86  *           We have therefore already proved that R(t) cannot be E.
  87  *
  88  *      (iii) There is t where d \elem E(t) but E(t) !\disjoint U
  89  *           In this case, consider a clash d' between E(t) and U
  90  *               d' \elem U,  d' \elem E(t)
  91  *
  92  *           This clash at d' is preventing us covering d with E(t).
  93  *           E's can't clash since they are disjoint so it must be
  94  *           a clash with some H.  But we have no unavoidable H's
  95  *           in our solution to U, so this solution to U2 has no
  96  *           unavoidable H's either.
  97  *
  98  *           Or to put it algebraically,
  99  *            d' != d, because d !\elem U.
 100  *            d' \elem A(t'') for some t'' since d' \elem U.
 101  *            If R(t'') = E, d' \elem E(t'') but E's are disjoint.
 102  *            So R(t'') = H, which must have been unavoidable by our
 103  *            inductive premise.  Thus for U2, R2(t'') = H is also
 104  *            unavoidable.
 105  *
 106  *      Proof elements: R(t') = H is demonstrated by
 107  *      every d meeting these conditions
 108  *      together with for each such d
 109  *          the alternative train t if applicable
 110  *          (there can be only one)
 111  *      plus in case (iii)
 112  *          every clash d' between E(t) and U
 113  *          plus for each such d' the corresponding t''
 114  *          (we record all this indexed by t so we can reuse it
 115  *           if needed)
 116  *
 117  *      R2 consists only of Hs and Ns.  All of the Hs are necessary
 118  *      for U2 by the above, so R2 is minimal for U2.
 119  *
 120  *      The rank is increased: we increase Count(R,H) and set
 121  *      Count(R,E) to 0.
 122  *
 123  *  3c. If neither of these is true, we are stuck and cannot
 124  *      satisfy d.  This is an error.  We remove d from D
 125  *      and continue anyway to see if we can find any more.
 126  *
 127  *      Proof elements: Lack of solution is demonstrated
 128  *      separately by every such  d  together with
 129  *      for each d if d \elem E(t) for some t
 130  *          that t
 131  *          plus the clashes d'' as for 3b(iii).
 132  *
 133  *  Termination: at each iteration 3a or 3b, we strictly increase Rank.
 134  *  At each iteration 3c we reduce D.
 135  *  Rank cannot exceed |T|*(|T|+1) and D starts out finite. So
 136  *  eventually we must succeed or fail.
 137  *
 138  */
 139
 140 #include "realtime.h"
 141
 142 /* values for Train->resolution: */
 143 #define RR_N 0u
 144 #define RR_E 1u
 145 #define RR_H 2u
 146
 147 /* We record R in tra->resolution,
 148  * U in segi->tr_updated and D in segi->res_detect */
 149
 150 void resolve_begin(void) {
 151   SEG_IV;
 152   actual_inversions_start();
 153   FOR_SEG {
 154     seg->res_detect= 0;
 155     seg->tr_updated= 0;
 156     if (segi->invertible)
 157       actual_inversions_segment(seg);
 158     else
 159       seg->seg_inverted= 0;
 160   }
 161   actual_inversions_done();
 162 }
 163
 164 #define NOOP (void)0
 165
 166 int resolve_complete(void) {
 167   int problems, phase, nextphase;
 168   TRAIN_ITERVARS(t);
 169   TRAIN_ITERVARS(t2);
 170   TRAIN_ITERVARS(tplus);
 171   SEGMENT_ITERVARS(d);
 172   SEGMENT_ITERVARS(d1);
 173   SEGMENT_ITERVARS(dplus);
 174
 175   problems= 0;
 176   FOR_TRAIN(t,NOOP,NOOP) t->resolution= RR_N;
 177
 178   for (phase=0; phase<3; phase=nextphase) {
 179     nextphase= phase+1;
 180     oprintf(UPO, "resolving iteration %c\n", "EHX"[phase]);
 181
 182     oprintf(UPO, "resolving  calculate-u\n");
 183
 184     FOR_SEGMENT(d, NOOP, NOOP) { /* calculate U */
 185       unsigned updated= 0;
 186
 187 #define ADDTO_U_EH(homeowner,HH_HE,string)                      \
 188       if (d->homeowner && d->homeowner->resolution == HH_HE) {  \
 189         oprintf(UPO, "resolving   covered @%s " string " %s\n", \
 190                 di->pname, d->homeowner->pname);                \
 191         updated++;                                              \
 192       }
 193       ADDTO_U_EH(home,  RR_H, "at-home");
 194       ADDTO_U_EH(owner, RR_E, "as-expected");
 195
 196       assert(updated<=1);
 197       d->tr_updated= updated;
 198     }
 199
 200     oprintf(UPO, "resolving  searching\n");
 201     FOR_SEGMENT(d, NOOP, NOOP) {
 202       if (!(d->res_detect && !d->tr_updated))
 203         continue;
 204       /* 3. we have a violation of D \subset U, namely d */
 205
 206       oprintf(UPO, "resolving   violation @%s\n", di->pname);
 207
 208       if (d->owner) { /* 3a perhaps */
 209         oprintf(UPO, "resolving    expected %s\n", t->pname);
 210
 211         if (t->resolution == RR_H) {
 212           oprintf(UPO, "resolving     expected-is-at-home\n");
 213           goto not_3a;
 214         }
 215
 216         if (t->resolution == RR_E)
 217           /* we added it in this sweep and have found another d */
 218           goto already_3a;
 219         assert(t->resolution == RR_N);
 220
 221         /* check E(t) \disjoint U */
 222         int clashes= 0;
 223         FOR_SEGMENT(d1, NOOP, NOOP) {
 224           if (d1->owner == t && d1->tr_updated) {
 225             FOR_TRAIN(t2, NOOP, NOOP) {
 226               if (t2->resolution == RR_H && d1->owner == t2) {
 227                 oprintf(UPO, "resolving     clash @%s %s\n",
 228                         d1i->pname, t2->pname);
 229                 clashes++;
 230               }
 231             }
 232           }
 233         }
 234         if (clashes) {
 235           oprintf(UPO, "resolving    expected-has-clashes\n");
 236           goto not_3a;
 237         }
 238
 239         /* Yay! 3a. */
 240         t->resolution= RR_E;
 241         nextphase= 0;
 242       already_3a:
 243         oprintf(UPO, "resolving    supposing %s as-expected\n", t->pname);
 244         continue;
 245       }
 246     not_3a:
 247
 248       if (d->home) { /* 3b then */
 249         if (phase<1)
 250           continue;
 251
 252         Train *t1= d->home; /* t' st d \elem H(t') */
 253         oprintf(UPO, "resolving    home %s\n", t1->pname);
 254
 255         oprintf(UPO, "resolving    reset-expecteds\n");
 256         FOR_TRAIN(tplus, NOOP,NOOP) {
 257           if (tplus->resolution == RR_E) {
 258             oprintf(UPO, "resolving    supposing %s absent\n", tplus->pname);
 259             tplus->resolution= RR_N;
 260             nextphase= 0;
 261           }
 262         }
 263         /* Now must trim U to correspond to our setting of R(t+)=N
 264          * so that any other implied Hs are spotted. */
 265         FOR_SEGMENT(dplus, NOOP,NOOP) {
 266           Train *tplus= dplus->owner;
 267           if (!(tplus && tplus->resolution == RR_E)) continue;
 268           dplus->tr_updated= 0;
 269         }
 270
 271         t1->resolution= RR_H;
 272         nextphase= 0;
 273
 274         oprintf(UPO, "resolving    supposing %s at-home\n", t1->pname);
 275         continue;
 276       }
 277
 278       /* Oh dear, 3c. */
 279       if (phase<2)
 280         continue;
 281
 282       oprintf(UPO, "resolving    inexplicable @%s\n", di->pname);
 283       d->res_detect= 0;
 284       problems++;
 285     }
 286   }
 287
 288   if (problems) oprintf(UPO,"resolve problems %d\n",problems);
 289
 290   FOR_SEGMENT(d,NOOP,NOOP)
 291     d->tr_updated= d->res_detect= 0;
 292
 293   if (problems)
 294     return -1;
 295
 296   return 0;
 297 }