Recursive MCA Algorithms

This section presents the list of recursive MCA algorithms implemented in CTLog. A recursive MCA algorithm combines smaller MCAs into larger ones.

Warning

The current version of these algorithms do not support SUT models with constraints.

Even if you use a SUT model with constraints, they will ignore them.

For the examples, we will use the following SUT model from the CT Competition 2023:

[System]
-- specify system name
Name: MCA_0

[Parameter]
-- general syntax is parameter_name : value1, value2, ...
Par0 (enum) : PAR0_0
Par1 (enum) : PAR1_0, PAR1_1, PAR1_2, PAR1_3, PAR1_4
Par2 (boolean) : true, false
Par3 (boolean) : true, false
Par4 (boolean) : true, false
Par5 (enum) : PAR5_0, PAR5_1, PAR5_2
Par6 (enum) : PAR6_0, PAR6_1, PAR6_2, PAR6_3, PAR6_4, PAR6_5, PAR6_6, PAR6_7, PAR6_8, PAR6_9, PAR6_10, PAR6_11
Par7 (boolean) : true, false
Par8 (enum) : PAR8_0, PAR8_1, PAR8_2, PAR8_3
Par9 (enum) : PAR9_0, PAR9_1, PAR9_2, PAR9_3, PAR9_4, PAR9_5, PAR9_6, PAR9_7, PAR9_8, PAR9_9, PAR9_10, PAR9_11, PAR9_12
Par10 (boolean) : true, false
Par11 (boolean) : true, false
Par12 (boolean) : true, false
Par13 (enum) : PAR13_0, PAR13_1, PAR13_2, PAR13_3, PAR13_4, PAR13_5, PAR13_6, PAR13_7, PAR13_8
Par14 (enum) : PAR14_0, PAR14_1, PAR14_2, PAR14_3, PAR14_4, PAR14_5, PAR14_6
Par15 (boolean) : true, false
Par16 (boolean) : true, false
Par17 (boolean) : true, false

ReMiCA Algorithm

The ReMiCA Algorithm is a recursive algorithm introduced in ReMiCA: Recursive Construction of High-Strength Mixed Covering Arrays (under review).

To use ReMiCA you can run:

ctlog mcac algorithms run RemicaAlgorithm MCA_0.acts 3 --args block_size=9

ReMiCA needs the block_size parameter. In this case, we specify two partitions of 9 parameters each. The generated output is the following:

[...]
c T: PAR0_0,PAR1_4,*,*,true,*,PAR6_2,true,*,PAR9_10,true,true,true,*,*,true,true,true
c T: PAR0_0,PAR1_4,*,*,true,*,PAR6_0,true,*,PAR9_11,true,true,true,*,*,true,true,true
c T: PAR0_0,*,*,*,true,*,PAR6_1,true,PAR8_2,PAR9_2,true,true,true,*,*,true,true,true
c T: PAR0_0,*,*,*,true,*,PAR6_0,true,PAR8_1,PAR9_5,true,true,true,*,*,true,true,true
Finished output of test cases. Size: 1670
Validating MCAC...
VALIDATION OK
Num covered: 49544
Num forbidden: 0

We can specify a smaller block_size, and ReMiCA will combine the resulting MCAs recursively:

ctlog mcac algorithms run RemicaAlgorithm MCA_0.acts 3 --args block_size=4

In this case, you should expect a lower running time at the expense of returning a larger MCA:

[...]
c T: PAR0_0,PAR1_0,true,true,true,PAR5_0,PAR6_0,false,PAR8_0,PAR9_0,false,false,false,PAR13_0,PAR14_0,false,true,true
c T: *,PAR1_0,true,true,true,PAR5_0,PAR6_0,true,PAR8_0,PAR9_0,false,true,false,PAR13_0,PAR14_0,true,false,false
c T: *,PAR1_0,true,true,true,PAR5_0,PAR6_0,true,PAR8_0,PAR9_0,false,false,true,PAR13_0,PAR14_0,false,true,false
c T: *,PAR1_0,true,true,true,PAR5_0,PAR6_0,false,PAR8_0,PAR9_0,false,true,true,PAR13_0,PAR14_0,false,false,true
Finished output of test cases. Size: 3040
Validating MCAC...
VALIDATION OK
Num covered: 49544
Num forbidden: 0

Weaken-Product Algorithm

This is our implementation of the weaken-product algorithm described in [UQWF22]. Unlike with ReMiCA Algorithm, here we cannot specify a block size. Instead, the algorithm will always partition the parameters in two blocs with the same number of parameters (plus-minus one).

You can run weaken-product using the following command:

ctlog mcac algorithms run WeakenProductAlgorithm MCA_0.acts 3

This generates the following output:

[...]
c T: *,PAR1_0,true,true,*,PAR5_0,PAR6_1,*,PAR8_0,PAR9_1,*,*,*,PAR13_8,PAR14_0,*,*,*
c T: *,PAR1_3,false,false,*,PAR5_2,PAR6_6,*,PAR8_3,PAR9_8,*,*,*,PAR13_5,PAR14_1,*,*,*
c T: *,PAR1_3,false,false,*,PAR5_2,PAR6_4,*,PAR8_2,PAR9_12,*,*,*,PAR13_6,PAR14_3,*,*,*
c T: *,PAR1_4,false,false,*,PAR5_1,PAR6_10,*,PAR8_1,PAR9_6,*,*,*,PAR13_3,PAR14_5,*,*,*
Finished output of test cases. Size: 1826
Validating MCAC...
VALIDATION OK
Num covered: 49544
Num forbidden: 0