From 5196b3cede185fe5e5ba396241d26882050d7c0b Mon Sep 17 00:00:00 2001 From: ian Date: Wed, 26 Mar 2008 22:47:12 +0000 Subject: [PATCH] wip hostside resolver continues; still startup.c not checked in here --- hostside/resolve.c | 197 +++++++++++++++++++++++++++++++++++---------- 1 file changed, 154 insertions(+), 43 deletions(-) diff --git a/hostside/resolve.c b/hostside/resolve.c index 4b7b331..e471163 100644 --- a/hostside/resolve.c +++ b/hostside/resolve.c @@ -54,7 +54,8 @@ * We will now calculate new R which we will call R2 * giving new U which we will call U2. * - * 3a. Hope that d \elem E(t) with E(t) \disjoint U. + * 3a. Hope that \exists{t} st d \elem E(t) with + * E(t) \disjoint U and R(t) = N. * If so set R2(t) = E giving a solution to U2. * * Optimality: if d \elem D then we need U2 to include d. @@ -70,41 +71,48 @@ * Proof elements: R(t) = E is demonstrated by * every d meeting these conditions. * - * 3b. Alternatively, hope that d \elem H(t) + * 3b. Alternatively, hope that d \elem H(t') * - * If so set R2(t) = H - * \all R2(t') = N where R(t') = E. + * If so set R2(t') = H + * \all_{t+} R2(t+) = N where R(t+) = E. * * Optimality: in the case we are now dealing with, we * didn't succeed with the test for 3a, so either: * - * (i) There is no t' where d \elem E(t'), so R(t) = H is - * essential because no solution without R(t) = H has d \elem U2. + * (i) There is no t where d \elem E(t), so R(t') = H is + * essential because no solution without R(t') = H has d \elem U2. * - * (ii) There is t' where d \elem E(t') but E(t') !\disjoint U - * In this case, consider a clash d'' between E(t') and U - * d'' \elem U, d'' \elem E(t') + * (ii) There is t where d \elem E(t) but R(t) = H. + * We have therefore already proved that R(t) cannot be E. * - * This clash at d'' is preventing us covering d with E(t'). + * (iii) There is t where d \elem E(t) but E(t) !\disjoint U + * In this case, consider a clash d' between E(t) and U + * d' \elem U, d' \elem E(t) + * + * This clash at d' is preventing us covering d with E(t). * E's can't clash since they are disjoint so it must be * a clash with some H. But we have no unavoidable H's * in our solution to U, so this solution to U2 has no * unavoidable H's either. * * Or to put it algebraically, - * d'' != d, because d !\elem U. - * d'' \elem A(t'') for some t'' since d'' \elem U. - * If R(t'') = E, d'' \elem E(t'') but E's are disjoint. + * d' != d, because d !\elem U. + * d' \elem A(t'') for some t'' since d' \elem U. + * If R(t'') = E, d' \elem E(t'') but E's are disjoint. * So R(t'') = H, which must have been unavoidable by our * inductive premise. Thus for U2, R2(t'') = H is also * unavoidable. * - * Proof elements: R(t) = H is demonstrated by + * Proof elements: R(t') = H is demonstrated by * every d meeting these conditions - * together with in case (ii) - * the alternative train t' (there can be only one) plus - * every clash d'' between E(t') and U - * plus for each such d'' the corresponding t'' + * together with for each such d + * the alternative train t if applicable + * (there can be only one) + * plus in case (iii) + * every clash d' between E(t) and U + * plus for each such d' the corresponding t'' + * (we record all this indexed by t so we can reuse it + * if needed) * * R2 consists only of Hs and Ns. All of the Hs are necessary * for U2 by the above, so R2 is minimal for U2. @@ -116,7 +124,11 @@ * satisfy d. This is an error. We remove d from D * and continue anyway to see if we can find any more. * - * Proof elements: Lack of solution is demonstrated by d. + * Proof elements: Lack of solution is demonstrated + * separately by every such d together with + * for each d if d \elem E(t) for some t + * that t + * plus the clashes d'' as for 3b(iii). * * Termination: at each iteration 3a or 3b, we strictly increase Rank. * At each iteration 3c we reduce D. @@ -127,51 +139,125 @@ #include "realtime.h" +typedef enum { + RR_N, RR_E, RR_H +} ResolutionResult; + typedef struct { + SegmentNum d; /* proof element d from 3a, 3b, 3c */ /* sentinel has NOTA */ + TrainNum t; /* proof element t from 3b(ii) and 3b(iii) */ +} ProofElement; -}; +typedef struct { + SegmentNum d1; /* proof element d' from 3b(iii) */ /* sentinel has NOTA */ + TrainNum t2; /* proof element t'' from 3b(iii) */ +} Clash; + +typedef struct { + ResolutionResult r; /* R(t) */ + ProofElement why_eh[NUM_SEGMENTS]; /* entry for 3a's t, proof of R(t)=E + * entry for 3b's t', proof of R(t')=H */ + Clash whynot_e[NUM_SEGMENTS]; /* in the entry for train t' from 3b(iii), + * clashes d' and corresponding t'' */ +} TrainResolution; +static TrainResolution *rx; /* [0,n_trains> */ +/* We record U in segi->tr_updated and D in segi->res_detect */ void resolve_begin(void) { SEG_IV; FOR_SEG { - seg->tr_updated= 0; seg->res_detect= 0; } } -fixme deal with until_detect etc. - -static void send_home(Train *tra, const char *why, Segment *why_seg) { - const char *trap; +#define NOOP (void)0 - trap= tra->i->pname; - oprintf(UPO,"resolve home %s %s %s\n",trap, why, why_seg->i->pname); - - FOR_SEG { - if (seg->home==tra && seg->owner && seg->owner!=tra) - send_home(seg->owner,"displaced",seg); +#define TRAIN(t,tra) \ + Train *t= (tra); \ + TrainNum t##n= (tra) - trains; \ + TrainResolution *t##r= rx + t##n; - if (seg->owner==tra && seg->home!=tra) { - oprintf(UPO,"resolve home %s nolonger %s\n",trap, seg->i->pname); - seg->owner= 0; - } - - } - - - +#define APPENDING(array, variable, isreal) \ + typeof(*array) variable; \ + for ((variable)=(array); \ + ; \ + (variable)++) { \ + assert((variable) < (array)+sizeof((array))/sizeof(*(array))); \ + if (!(isreal)) break; \ + } int resolve_complete(void) { int problems; SEG_IV; + rx= mmalloc(sizeof(*rx) * n_trains); + FOR_TRA { + rx[tran].r= RR_N; + rx[tran].why_eh.d= NOTA(Segment); + rx[tran].whynot_e.d1= NOTA(Segment); + } + while 1 { - FOR_SEG { - if (seg->res_detect && !seg->tr_updated && !seg->owner) - goto found; + FOR_SEGMENT(d, NOOP, NOOP) { /* calculate U */ + unsigned updated= 0; + if (d->home) { TRAIN(t, d->home); if (tr->r == HH_H) updated++; } + if (d->owner) { TRAIN(t, d->owner); if (tr->r == HH_E) updated++; } + assert(updated<=1); + d->tr_updated= updated; } + + FOR_SEGMENT(d, NOOP, NOOP) { + if (!(d->res_detect && !d->tr_updated)) + continue; + /* 3. we have a violation of D \subset U, namely d */ + + if (d->owner) { /* 3a perhaps */ + TRAIN(t, d->owner); /* t st d \elem E(t) */ + if (tr->r == RR_H || SOMEP(tr->whynot_e[0])) + goto not_3a; + + /* check E(t) \disjoint U */ + Clash clash; + FOR_SEGMENT(clash.d1, NOOP, NOOP) { + if (clash.d1->owner == t && clash.d1->tr_updated) { + FOR_TRAIN(clash.t2, NOOP, NOOP) { + if (clash.t2r->r == HH_H && clash.d1->owner == clash.t2) { + ADDREASON(tr->whynot_e, clash, SOMEP(clash->clash.d1)); + } + } + } + } + if (SOMEP(tr->whynot_e[0])) + goto not_3a; + + /* Yay! 3a. */ + + + /* tr->whynot_e is already filled in */ + goto not_3a; + assert(tr->r == RR_N); + + + if (tr->whynot_e + + + goto not_e; + + + + FOR_TRAIN(t_, NOOP, NOOP) { + if ( + + + goto found; + } /* no (more) unexpected trains */ + break; + + found: + + if (problems) oprintf(UPO,"resolve problems %d\n",problems); return !problems; @@ -202,3 +288,28 @@ int resolve_complete(void) { FOR_SEG return 0; } + + + +fixme deal with until_detect etc. + seg->tr_updated= 0; + +static void send_home(Train *tra, const char *why, Segment *why_seg) { + const char *trap; + + trap= tra->i->pname; + oprintf(UPO,"resolve home %s %s %s\n",trap, why, why_seg->i->pname); + + FOR_SEG { + if (seg->home==tra && seg->owner && seg->owner!=tra) + send_home(seg->owner,"displaced",seg); + + if (seg->owner==tra && seg->home!=tra) { + oprintf(UPO,"resolve home %s nolonger %s\n",trap, seg->i->pname); + seg->owner= 0; + } + + } + + + -- 2.30.2