* 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.
* 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.
* 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.
#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;
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;
+ }
+
+ }
+
+
+
~ijackson / trains.git / commitdiff