/*
* resolve detected trains into initial state
*/
+/*
+ * Algorithm:
+ *
+ * Notation and background:
+ *
+ * S set of segments
+ * D \subset S set of segments where we have detection
+ *
+ * T set of trains
+ * H(t) \subset S home range for train t \elem T
+ * E(t) \subset S set of segments where train t last expected
+ *
+ * H(t) \disjoint H(t') for t != t'
+ * E(t) \disjoint E(t') for t != t'
+ * but not necessarily E(t) \disjoint H(t')
+ *
+ * We want to find a mapping R(t)
+ * R(t) \elem { N, E, H } t \elem T, N(t') = \null
+ * giving
+ * A(t) = (R(t))(t) segments allocated to train t
+ * U = \union_{t} A(t)
+ * satisfing
+ * A(t) \disjoint A(t') for t != t' `disjoincy'
+ * D \subset U `coverage'
+ * and the solution is somehow optimal or at least not badly suboptimal.
+ *
+ * We compute R incrementally, maintaining disjoincy,,
+ * while increasing U. At each stage R is an optimal solution
+ * to the problem posed by D' = U, and we maintain this invariant.
+ *
+ * We define an optimality ordering on R by counting occurrences of
+ * H, E, and H in the range, in that order. Ie,
+ * Count(R,x) = |{ t: R(t) = x }|
+ * Rank(R) = Count(R,H) * (|T|+1) + Count(R,E)
+ * and compare Ranks numerically, lower being better.
+ *
+ * So we mean that for any incrementally computed R, there is no
+ * R' satisfying the same subproblem D' = U for which Rank(R') < Rank(R).
+ *
+ * For the benefit of client programs, we record the key elements of
+ * the proofs that we generate for non-N values of R.
+ *
+ * 1. Initially we set \all_{t} R(t) = N.
+ *
+ * Optimality: This is minimal for U = \null, as Rank(R) = 0.
+ *
+ * 2. Then we search for lack of coverage, ie violations of D \subset U.
+ * If none are found we are done.
+ *
+ * 3. Let d \elem D but d !\elem U.
+ * 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.
+ * If so set R2(t) = E giving a solution to U2.
+ *
+ * Optimality: if d \elem D then we need U2 to include d.
+ * That means d \elem E(t) or d \elem H(t'). No E(t')
+ * other than E(t) can help since they are disjoint, and
+ * we would certainly prefer adding E(t) to adding H(t').
+ * (Adding H(t') and removing some other H(t'') doesn't
+ * work either because the Hs are disjoint, so no
+ * H can stand in for any other.)
+ *
+ * So the rank increase by 1 is is minimal for U2.
+ *
+ * Proof elements: R(t) = E is demonstrated by
+ * every d meeting these conditions.
+ *
+ * 3b. Alternatively, hope that d \elem H(t)
+ *
+ * If so set R2(t) = H
+ * \all 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.
+ *
+ * (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')
+ *
+ * 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.
+ * 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
+ * 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''
+ *
+ * R2 consists only of Hs and Ns. All of the Hs are necessary
+ * for U2 by the above, so R2 is minimal for U2.
+ *
+ * The rank is increased: we increase Count(R,H) and set
+ * Count(R,E) to 0.
+ *
+ * 3c. If neither of these is true, we are stuck and cannot
+ * 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.
+ *
+ * Termination: at each iteration 3a or 3b, we strictly increase Rank.
+ * At each iteration 3c we reduce D.
+ * Rank cannot exceed |T|*(|T|+1) and D starts out finite. So
+ * eventually we must succeed or fail.
+ *
+ */
#include "realtime.h"
-int resolve_failed(void) {
+typedef struct {
+
+};
+
+
+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;
+
+ 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;
+ }
+
+ }
+
+
+
+
+int resolve_complete(void) {
+ int problems;
+ SEG_IV;
+
+ while 1 {
+ FOR_SEG {
+ if (seg->res_detect && !seg->tr_updated && !seg->owner)
+ goto found;
+ }
+ /* no (more) unexpected trains */
+ if (problems) oprintf(UPO,"resolve problems %d\n",problems);
+ return !problems;
+
+ found:
+ if (!seg->home) {
+ /* completely unexpected presence of train */
+ oprintf(UPO,"resolve inexplicable %s\n",segi->pname);
+ seg->res_detect= 0;
+ problems++;
+ continue;
+ }
+ /* train put back in its home (we assume!) */
+ resolve_send_home(seg->home,seg,"spotted");
+
+
+
+ SEGMENT_ITERVARS(inner);
+
+ if (inner->home == seg->home) oprintf(UPO," +%s",inneri->pname);
+
+
+ if (inner->train
+
+ } else {
+
+
+
+ FOR_SEG
return 0;
}
~ijackson / trains.git / commitdiff