#include "realtime.h"
-typedef enum {
- RR_N, RR_E, RR_H
-} ResolutionResult;
+/* values for Train->resolution: */
+#define RR_N 0u
+#define RR_E 1u
+#define RR_H 2u
-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 */
+/* We record R in tra->resolution,
+ * U in segi->tr_updated and D in segi->res_detect */
void resolve_begin(void) {
SEG_IV;
FOR_SEG {
seg->res_detect= 0;
+ seg->tr_updated= 0;
}
}
#define NOOP (void)0
-#define TRAIN(t,tra) \
- Train *t= (tra); \
- TrainNum t##n= (tra) - trains; \
- TrainResolution *t##r= rx + t##n;
-
-#define BLANKREASONS(array, sentinelmember) \
- ((*(SegmentNum*)(array))= NOTA(Segment))
-
-#define ADDREASON(array, newvalue) do{ \
- typeof(*(array)) addreason_i; \
- for (addreason_i=(array); \
- ; \
- addreason_i++) { \
- assert(addreason_i < ARRAY_END(array)); \
- if (!SOMEP(*(SegmentNum*)(addreason_i))) { \
- *addreason_i++= newvalue; \
- *(SegmentNum*)addreason_i= NOTA(Segment); \
- assert(addreason_i < ARRAY_END(array)); \
- break; \
- } \
- if (*addreason_i == newvalue) \
- break; \
- } \
- }while(0)
+int resolve_complete(void) {
+ int problems, phase, nextphase;
+ TRAIN_ITERVARS(t);
+ TRAIN_ITERVARS(t2);
+ TRAIN_ITERVARS(tplus);
+ SEGMENT_ITERVARS(d);
+ SEGMENT_ITERVARS(d1);
+ SEGMENT_ITERVARS(dplus);
-#define FOR_TRAIN_R(t) FOR_TRAIN(t, t##r=rx, t##r++)
+ problems= 0;
+ FOR_TRAIN(t,NOOP,NOOP) t->resolution= RR_N;
-int resolve_complete(void) {
- int problems;
- SEG_IV;
+ for (phase=0; phase<3; phase=nextphase) {
+ nextphase= phase+1;
+ oprintf(UPO, "resolving iteration %c\n", "EHX"[phase]);
- rx= mmalloc(sizeof(*rx) * n_trains);
- FOR_TRAIN_R(t) {
- tr->r= RR_N;
- BLANKREASONS(tr->why_eh);
- BLANKREASONS(tr->whynot_e);
- }
+ oprintf(UPO, "resolving calculate-u\n");
- while 1 {
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++; }
+
+#define ADDTO_U_EH(homeowner,HH_HE,string) \
+ if (d->homeowner && d->homeowner->resolution == HH_HE) { \
+ oprintf(UPO, "resolving covered @%s " string " %s\n", \
+ di->pname, d->homeowner->pname); \
+ updated++; \
+ }
+ ADDTO_U_EH(home, RR_H, "at-home");
+ ADDTO_U_EH(owner, RR_E, "as-expected");
+
assert(updated<=1);
d->tr_updated= updated;
}
+ oprintf(UPO, "resolving searching\n");
FOR_SEGMENT(d, NOOP, NOOP) {
if (!(d->res_detect && !d->tr_updated))
continue;
/* 3. we have a violation of D \subset U, namely d */
- ProofElement why_h;
- why_h.d= d;
- why_h.t= NOTA(Train);
-
+ oprintf(UPO, "resolving violation @%s\n", di->pname);
+ nextphase= 0;
+
if (d->owner) { /* 3a perhaps */
- TRAIN(t, d->owner); /* t st d \elem E(t) */
- why_h.t= tn;
- if (tr->r == RR_H)
+ oprintf(UPO, "resolving expected %s\n", t->pname);
+
+ if (t->resolution == RR_H) {
+ oprintf(UPO, "resolving expected-is-at-home\n");
goto not_3a;
+ }
- if (tr->r == RR_E)
+ if (t->resolution == RR_E)
/* we added it in this sweep and have found another d */
goto already_3a;
- assert(tr->r == RR_N);
+ assert(t->resolution == RR_N);
/* check E(t) \disjoint U */
+ int clashes= 0;
FOR_SEGMENT(d1, NOOP, NOOP) {
if (d1->owner == t && d1->tr_updated) {
FOR_TRAIN(t2, NOOP, NOOP) {
- if (t2r->r == HH_H && d1->owner == t2) {
- Clash clash;
- clash.d1= d1;
- clash.t2= t2;
- ADDREASON(tr->whynot_e, clash);
+ if (t2->resolution == RR_H && d1->owner == t2) {
+ oprintf(UPO, "resolving clash @%s %s\n",
+ d1i->pname, t2->pname);
+ clashes++;
}
}
}
}
- if (SOMEP(tr->whynot_e[0]))
+ if (clashes) {
+ oprintf(UPO, "resolving expected-has-clashes\n");
goto not_3a;
+ }
/* Yay! 3a. */
- tr->r= RR_E;
+ t->resolution= RR_E;
already_3a:
- ProofElement why_e;
- why_e.d= d;
- why_e.t= NOTA(Train);
- ADDREASON(tr->why_eh, why_e);
+ oprintf(UPO, "resolving supposing %s as-expected\n", t->pname);
continue;
}
-
not_3a:
+
if (d->home) { /* 3b then */
- TRAIN(t1, d->home); /* t' st d \elem H(t') */
-
- if (tr->r == RR_H)
- /* added in this sweep, have found another d */
- goto already_3b;
+ if (phase<1)
+ continue;
- FOR_SEGMENT(dplus, NOOP, NOOP) {
- if (!dplus->owner) continue;
- TRAIN(tplus, dplus->owner);
- if (tplusr->r != HH_E) continue;
- dplus->tr_updated= 0;
- }
- FOR_TRAIN_R(tplus) {
- BLANKREASONS(tplusr->whynot_e);
- if (tplusr->r == HH_E) {
- tplusr->r= HH_N;
- BLANKREASONS(tplusr->why_eh);
+ Train *t1= d->home; /* t' st d \elem H(t') */
+ oprintf(UPO, "resolving home %s\n", t1->pname);
+
+ oprintf(UPO, "resolving reset-expecteds\n");
+ FOR_TRAIN(tplus, NOOP,NOOP) {
+ if (tplus->resolution == RR_E) {
+ oprintf(UPO, "resolving supposing %s absent\n", tplus->pname);
+ tplus->resolution= RR_N;
}
}
+ /* Now must trim U to correspond to our setting of R(t+)=N
+ * so that any other implied Hs are spotted. */
+ FOR_SEGMENT(dplus, NOOP,NOOP) {
+ Train *tplus= dplus->owner;
+ if (!(tplus && tplus->resolution == RR_E)) continue;
+ dplus->tr_updated= 0;
+ }
- tr->r= RR_H;
- BLANKREASONS(tr->why_eh);
-
- already_3b:
- ADDREASON(tr->why_eh, why_h);
- fixme /* need to make us scan for case 3a first, so that
- when we report a problem we report as reasons
- for some H only those ds which would not have
- been satisfied by E. perhaps scan for Es
- and then only for Hs, each time ? */
-
- /* 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 (
-
+ t1->resolution= RR_H;
- goto found;
+ oprintf(UPO, "resolving supposing %s at-home\n", t1->pname);
+ continue;
}
- /* no (more) unexpected trains */
- break;
- found:
-
-
- if (problems) oprintf(UPO,"resolve problems %d\n",problems);
- return !problems;
+ /* Oh dear, 3c. */
+ if (phase<2)
+ continue;
- found:
- if (!seg->home) {
- /* completely unexpected presence of train */
- oprintf(UPO,"resolve inexplicable %s\n",segi->pname);
- seg->res_detect= 0;
+ oprintf(UPO, "resolving inexplicable @%s\n", di->pname);
+ d->res_detect= 0;
problems++;
- continue;
}
- /* train put back in its home (we assume!) */
- resolve_send_home(seg->home,seg,"spotted");
-
-
+ }
- SEGMENT_ITERVARS(inner);
+ if (problems) oprintf(UPO,"resolve problems %d\n",problems);
- if (inner->home == seg->home) oprintf(UPO," +%s",inneri->pname);
-
+ FOR_SEGMENT(d,NOOP,NOOP)
+ d->tr_updated= d->res_detect= 0;
- if (inner->train
-
- } else {
-
-
+ if (problems)
+ return -1;
- 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