Module Resolution

module Resolution: sig .. end

Naive implementation of the resolution algorithm of adaptability constraints. The goal of the implementation is to illustrate the algorithm presented in the article MPC 2012, not to provide an efficient implementation of the algorithm.
Author(s): Louis Mandel, Florence Plateau

Resolution algorithm

exception Solve

The Solve exception is raised if a constraint system cannot be solved.

Translation of subtyping constraints to adaptability constraints

Introduction of word variables c_n and simplification of type varaibles such that the subtyping constraint system is rewritten into an equivalent adaptability constraint system.

val split_clock_type : Clock_type.clock_type ->
       Clock_type.clock_type_variable * Clock_expression.word_expr

Separate the type variable and the word expression in a clock type.

val adaptability_cstr_of_subtyping_cstr : Clock_type.subtype_cstr -> Clock_expression.adaptability_cstr

Rewrite a subtyping constraint 'a_x on p_x on p_x' on ... <: 'a_y on p_y on p_y' on ... into an adaptability constraint c_x on p_x on p_x' on ... <: c_y on p_y on p_y' on ... or into p_x on p_x' on ... <: p_y on p_y' on ... if 'a_x = 'a_y.

val adaptability_cstrs_of_subtyping_cstrs : Clock_type.subtype_cstr list -> Clock_expression.adaptability_cstr list

Rewrite a subtyping constraint system into an adaptability constraint system.

Simplification of adaptability constraints

Computation of on and simplification of p_x <: p_y constraints in an adaptability constraint system. The resulting system is an equivalent adaptability constraint system where all the constraints have the simple shape c_x on p_x <: c_y on p_y.

val simplify_adaptability_cstr : Clock_expression.adaptability_cstr ->
       Clock_expression.simplified_adaptability_cstr option

Simplify an adaptability constraint c_x on p_1 on p_1' on ... <: c_y on p_2 on p_2' on ... into c_x on p_x <: c_y on p_y or check that an adaptability constraint p_1 on p_1' on ... <: p_2 on p_2' on ... is satisfied.

val simplified_adaptability_cstrs_of_adaptability_cstrs : Clock_expression.adaptability_cstr list ->
       Clock_expression.simplified_adaptability_cstr list

Rewrite an adaptability constraint system into an equivalent one where all the constraints have the simple shape c_x on p_x <: c_y on p_y.

Translation of simplified adaptability constraints to adjusted adaptability constraints

This step takes as input a simplified adaptability constraint system where the shape of the constraint is c_x on p_x <: c_y on p_y. It returns an equivalent adaptability constraint system where for each c_n, the size of its samplers is equal.

val adjust_size : Clock_expression.word_variable * Pbword.periodic_binary_word ->
       Clock_expression.simplified_adaptability_cstr list ->
       Clock_expression.word_variable * Pbword.periodic_binary_word

Rewrite c on p into c on p' such that p = p' and |p'.u| = max { |p''.u| | p'' \in samplers_c(A) } and |p'.v| = lcm { |p''.v| | p'' \in samplers_c(A) }.

val adjusted_adaptability_cstrs_of_simplified_adaptability_cstrs : Clock_expression.simplified_adaptability_cstr list ->
       Clock_expression.simplified_adaptability_cstr list

Adjuste the size of each sampler in each constraint of a simplified adaptability constraint system.

Choice of the number of 1s in the solution and translation of adjusted adaptability constraints to synchronizability and precedence constraints

In this step, we choose the number of 1s in each variable c_n. Then we transforme an adjusted adaptability constraint system into the corresponding synchronizability and precedence constraints.

val choose_nbones : Clock_expression.word_variable ->
       Clock_expression.simplified_adaptability_cstr list -> int -> int -> int * int

Choose for a variable c_n the number of 1s in the prefix (|c_n.u|_1) and in the periodic part (|c_n.v|_1) such that |c_n.u|_1 = |p_n.u| + k * |p_n.v| ( = |p'_n.u| + k * |p'_n.v| = ...) and |c_n.n|_1 = k' * |p_n.v| ( = k' * |p'_n.v| = ...) with p_n \in samplers_{c_n}(A), p'_n \in samplers_{c_n}(A), ...

val make_choice : int ->
       int ->
       Clock_expression.simplified_adaptability_cstr list ->
       Clock_expression.choice_of_number_of_1

Choose for each variable in an adjusted adaptability constraint system its number of 1s in the prefix and periodic part.

val split_adaptability_cstr : Clock_expression.simplified_adaptability_cstr ->
       Clock_expression.synchronizability_cstr * Clock_expression.precedence_cstr

Split an adaptability constraint c_x on p_x <: c_y on p_y into a synchronizability constraint c_x on p_x |><| c_y on p_y and a precedence constraint c_x on p_x <= c_y on p_y.

val synchronizability_and_precedence_cstrs_of_adjusted_adaptability_cstrs : Clock_expression.simplified_adaptability_cstr list ->
       Clock_expression.synchronizability_cstr list *
       Clock_expression.precedence_cstr list

Split an adaptability constraint system into equivalent synchronizability and precedence constraint systems.

Synchronizability and precedence constraints to linear constraints on the index of 1s and size of unknown words

This translation depends on the choice of number on 1s in the unknown words.

val simplify_synchronizability_cstr : Clock_expression.synchronizability_cstr -> Clock_expression.linear_cstr

Simplify a synchronizability constraint c_x on p_x |><| c_y on p_y into a constraint on the size of the word variables: |p_y.v|_1 * |c_x| = |p_x.v|_1 * |c_y|.

val simplify_synchronizability_cstrs : Clock_expression.synchronizability_cstr list ->
       Clock_expression.linear_cstr list

Simplify a synchronizability constraint system.

val simplify_precedence_cstr : int ->
       int -> Clock_expression.precedence_cstr -> Clock_expression.linear_cstr list

Simplify a precedence constraint c_x on p_x <= c_y on p_y into constraints on the indexes of 1s: for all 1 <= j <= h, I_{c_x}(I_{p_x}(j)) <= I_{c_x}(I_{p_x}(j)) with

h = max (|p_x.u|_1 + k * |p_x.v|_1, |p_y.u|_1 + k * |p_y.v|_1) +
              lcm (k' * |p_x.v|_1, k' * |p_y.v|_1)

val simplify_precedence_cstrs : Clock_expression.choice_of_number_of_1 ->
       Clock_expression.precedence_cstr list -> Clock_expression.linear_cstr list

Simplify a precedence constraint system.

val build_periodicity_cstr : Clock_expression.integer_variable ->
       int * int -> Clock_expression.linear_cstr

Build the periodicity constraint associated to a variable I_{c_n}(j'). Suppose that j' = j + l * |c_n.v|_1, the periodicity constraint is: I_{c_n}(j') - I_{c_n}(j) = l * |c_n.v|.

val build_periodicity_cstrs : Clock_expression.linear_cstr list ->
       Clock_expression.choice_of_number_of_1 -> Clock_expression.linear_cstr list

Build the set of periodicity constraints.

val build_sufficient_size_cstr : Clock_expression.word_variable -> int * int -> Clock_expression.linear_cstr

Build sufficient size constraint from the choice of number of 1s of a word variable: 1 + I_{c_n}(|c_n.u|_1 + |c_n.u|_1) - I_{c_n}(|c_n.u|_1 + 1) <= |c_n.v|.

val build_sufficient_size_cstrs : Clock_expression.choice_of_number_of_1 -> Clock_expression.linear_cstr list

Build the set of sufficient size constraints.

val build_sufficient_index_cstr : Clock_expression.integer_variable -> Clock_expression.linear_cstr

Build sufficient indexes constraints from and index on 1 variable I_{c_n}(j): I_{c_n}(j) >= j.

val build_sufficient_index_cstrs : Clock_expression.linear_cstr list ->
       Clock_expression.linear_cstr list ->
       Clock_expression.linear_cstr list -> Clock_expression.linear_cstr list

Build the set of sufficient indexes constraints.

val build_increasing_index_cstrs_of_c_n : Clock_expression.Integer_var_set.t -> Clock_expression.linear_cstr list

Build increasing indexes constraint: I_{c_n}(j') - I_{c_n}(j) >= j' - j.

val build_increasing_index_cstrs : Clock_expression.linear_cstr list ->
       Clock_expression.linear_cstr list ->
       Clock_expression.linear_cstr list -> Clock_expression.linear_cstr list

Build increasing indexes constraint system.

val iof_and_size_cstrs_of_synchronizability_and_precedence_cstrs : Clock_expression.choice_of_number_of_1 ->
       Clock_expression.synchronizability_cstr list ->
       Clock_expression.precedence_cstr list -> Clock_expression.iof_and_size_cstrs

Build indexes of 1s and size constraints corresponding to synchronizability and precedence constraints.

From adaptability constraints to linear constraints

val iof_and_size_cstrs_of_adaptability_cstrs : ?verbose:bool ->
       int ->
       int ->
       Clock_expression.adaptability_cstr list ->
       Clock_expression.iof_and_size_cstrs

Build directely the indexes of 1s and size constraints corresponding to adaptability constraints.

Linear constraints solving

val iof_and_size_cstrs_solving : ?verbose:bool ->
       Clock_expression.iof_and_size_cstrs -> int Clock_expression.Integer_var_map.t

Solve the linear constraints on the indexes of 1s and sizes.

val check_iof_and_size_sol : Clock_expression.iof_and_size_cstrs ->
       int Clock_expression.Integer_var_map.t -> bool

Check the solution of a system of constraints on indexes of 1s and sizes.

Word reconstruction

val compute_size_c_n_u : Clock_expression.word_variable ->
       int -> int Clock_expression.Integer_var_map.t -> int

Compute the prefix size of a variable c_n. It is the index before the first 1 in c_n.v.

val build_pbword : Clock_expression.word_variable ->
       int ->
       int -> int Clock_expression.Integer_var_map.t -> Pbword.periodic_binary_word

Build an ultimately periodic binary word from the number of 1s of its prefix and periodic part, the size of its prefix and periodic part, and the indexes of its 1s.

val pbwords_of_iof_and_size_sol : Clock_expression.choice_of_number_of_1 ->
       int Clock_expression.Integer_var_map.t ->
       Pbword.periodic_binary_word Clock_expression.Word_var_map.t

Build the ultimately periodic binary words corresponding to the solution of sizes and indexes of 1s.

val check_adaptability_sol : Pbword.periodic_binary_word Clock_expression.Word_var_map.t ->
       Clock_expression.adaptability_cstr list -> bool

Check the solution of an adaptability constraint system.

Subtyping constraints solving

val constraint_system_solving : ?verbose:bool ->
       int ->
       int ->
       Clock_type.subtype_cstr list ->
       Pbword.periodic_binary_word Clock_expression.Word_var_map.t

Solve a subtyping constraint system.

Example

Let us transform the following subtyping constraint system into linear constraints: { 'a_1 on 10(1) <: 'a_2 on (01) ; 'a_2 on (01) on (10) <: 'a_3 on (1) ; 'a_2 on (01) on (01) <: 'a_3 on (1) ; }.

val subtyping_cstrs_C' : Clock_type.subtype_cstr list

val iof_and_size_cstrs_C' : Pbword.periodic_binary_word Clock_expression.Word_var_map.t