Index of values

The adaptability test of two ultimately periodic binary words: p_1 <: p_2.

The synchronizability test of two ultimately periodic binary words: p_1 |><| p_2 <=> rate p1 = rate p2.

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.

Rewrite a subtyping constraint system into an adaptability constraint system.

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) }.

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

Build increasing indexes constraint system.

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

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.

Build the periodicity constraint associated to a variable I_{c_n}(j').

Build the set of periodicity constraints.

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

Build the set of sufficient indexes constraints.

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|.

Build the set of sufficient size constraints.

Check the solution of an adaptability constraint system.

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

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), ...

Compute the prefix size of a variable c_n.

Solve a subtyping constraint system.

Print a list of elements.

Greatest common divisor.

Increase prefix size of n bits: u(vv') = uv(v'v) with |v| = n.

Index of the jth 1 of an ultimately periodic binary word p: I_p(j).

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

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

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

Least common multiple.

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

Number of 1s a finite word u: |u|_1.

Computation of the on operator: u_3(v_3) = u_1(v_1) on u_2(v_2) with |u_3| = max (|u_1|, I_{p_1}(|u_2|)), |v_3| = (lcm (|v_1|_1, |v_2|) / |v_1|_1) * |v_1| and for all 1 <= i <= |u_3|, u_3[i] = (p_1 on p_2)[i] and for all 1 <= i <= |v_3|, v_3[i] = (p_1 on p_2)[|u_3| + i]

Compute ons in an expression c on p1 on p2 on ... or p1 on p2 on ....

The ultimately periodic binary word (1).

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

The precedence test of two ultimately periodic binary words: p_1 <= p_2 <=> I_{p_1}(j) <= I_{p_2}(j), for all 1 <= j <= h with h = max (|p_1.u|_1,|p_2.u|_1) + lcm (|p_1.v|_1,|p_2.v|_1).

Computation of the rate of an ultimately periodic binary word: rate p = |p.v|_1 / |p.v|.

Repeat periodic pattern: u(v) = u(v^k).

Samplers of a variable c_n in a simplified adaptability constraint system A: { p_n | (c_n on p_n <: c_y on p_y) \in A \/ (c_x on p_x <: c_n on p_n) \in A }.

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.

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.

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).

Simplify a precedence constraint system.

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|.

Simplify a synchronizability constraint system.

Size of a finite word u: |u|.

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.

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

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

Set of integer variables that appear in a linear constraint system.

Set of word variables that appear in a simplified adaptability constraint system.