From f47b4c3e26c50d61a080ab2251232dfe03a25d8a Mon Sep 17 00:00:00 2001 From: ian Date: Wed, 26 Mar 2008 18:18:24 +0000 Subject: [PATCH] wip resolution code; partial checkin - wiring in liberator:things/trains/hostside/startup.c --- hostside/resolve.c | 197 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 196 insertions(+), 1 deletion(-) diff --git a/hostside/resolve.c b/hostside/resolve.c index 73bb763..4b7b331 100644 --- a/hostside/resolve.c +++ b/hostside/resolve.c @@ -1,9 +1,204 @@ /* * 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; } -- 2.30.2