Router route reconfiguration planning
View Patent ↗A method for solving the reconfiguration planning problem transforms the requirement that an invariant is always preserved into a constraint on the times at which the configuration parameters change. The method then solves this constraint to obtain the required reconfiguration plan. When this constraint is strengthened with a synthesis constraint, it is ensured that any final configuration that is computed is also reachable. An extension of the method allows parameters to take on multiple intermediate values.
1. A method of creating reconfiguration plans for changing variables from an initial value to a final value in a system while preserving constraints, comprising:
a processor for performing computer instructions for:
assigning configuration values v 1 , . . . , vk for each variable in a the system where k is a number of variables in the system;
assigning time [v] to be a positive, integer-valued time at which the value of configuration variable v is changed from init [v] to final [v], where time [v] is a one-to-one mapping between the set of configuration variables and the integers in the interval [1, k];
encoding a reconfiguration sequence where the value of a configuration variable v immediately after time t is defined as follows: If time [v]=<t then init [v] else final [v];
forming a reconstruction plan by finding values of the time variables time [v 1 ], . . . , time [vk] so that Invariant holds immediately after each time in [1, k]; and
computing by first deriving a constraint on the time variables for the Invariant to hold after a generic time t and for each t in [1, . . . , k], the constraint is instantiated.
2. The method as set forth in claim 1 , where for every configuration variable v in the definition of Invariant, replace v by the expression if time [v] =<t then init [v] else final [v] and the resulting constraint is holds (Invariant, t); Let all_times [Invariant] is the conjunction of holds (Invariant, 1), . . . , holds (Invariant, k); and solve the conjunction of all_times (Invariant) and the constraint that for no two distinct variables x, y is it the case that time [x] time [y].
3. The method of claim 1 , where variables assume intermediate values mid [v] and the variables change to mid [v] at time t 1 [v] and to final [v] at time t 2 [v]; and computing holds (Invariant, t), replace every occurrence of v in the definition of Invariant by the expression:
if t 1 [v]<=t then init [v]
else if t 2 [v]<=t then mid [v]
else final [v]
all_times(Invariant) is then the conjunction of holds (Invariant, t) for each value of t in 1, . . . , 2*k where k is the number of configuration variables.