MutaLog - a Tool for Mutating Logic Formulas

1 Introduction

What is MutaLog?

MutaLog is a testing tool which allows performing mutation analysis of logic formulas.

Features

MutaLog allows:

- Loading a logic formula from a file. MutaLog supports the DIMACS (Conjunctive Normal Form) format,
- Visualizing the clauses of the formula
- Create mutants of the formula,
- Load a test suite and evaluate the mutation score towards the formula mutants.

2 Usage

Command Line Interface

MutaLog can be used through a command line interface. The command is as follows:

    java -jar MutaLog.jar [options] [command] [command options]  Commands:
        mutation_score      Evaluate the mutation score of the test suite
          Usage: mutation_score [options]
            Options:
              -and   Use operator AND mutants
                     Default: false
              -cn    Use clause negation mutants
                     Default: false
              -co    Use clause omission mutants
                     Default: false
            * -f     The CNF formula file (.dimacs)
              -ln    Use literal negation mutants
                     Default: false
              -lo    Use literal omission mutants
                     Default: false
              -or    Use operator OR mutants
                     Default: false
            * -ts    The test suite file

Starting Window

Without option provided to the tool, the GUI starts. The main window contains a menu and tool bar located at the top of the window, to access to the functions of the , and a status bar located at the bottom of the window.

The Menu Bar

It contains 3 items : |

The File item allows: Loading a logic formula, Loading a test suite, Quitting the application. |

The Execute item allows: Evaluating the mutation score of the test suite, Stopping the execution of the application. |

The Help item allows: Opening this user guide, Visualizing information about the version of the tool. |

The Tool Bar

It contains 7 buttons which correspond to shortcuts to the main functionalities of the tool: |

From left to right:

- File -> Load a logic formula
- File -> Load a test suite
- File -> Exit

- Execute -> Evaluate the mutation score of the test suite
- Execute -> Stop the execution

Load a logic formula

MutaLog supports the DIMACS (Conjunctive Normal Form) format for logic formulas. An input file starts with comments (each line starts with c). The number of variables and the number of clauses is defined by the line p cnf variables clauses. Each of the next lines specifies a clause: a positive literal is denoted by the corresponding number, and a negative literal is denoted by the corresponding negative number. The last number in a line should be zero. For example c A sample .cnf file. p cnf 3 2 1 -3 0 2 3 -1 0
After having loaded a logic formula, the following window appears:

The upper part contains information related to the formula, like the number of variables. The lower part contains the list of clauses.

Load a test suite and evaluate the mutation score

After loading a test suite, the following window appears:

On the lower part, the different test cases of the test suite are displayed. After choosing to evaluate the mutation score, a configuration window allows selecting the desired mutants for the logic formula:

Finally, after confirming the selected mutants, the mutation score is calculated and the mutants are displayed. Invalid mutants are stroked and killed mutants are displayed in red. The invalid mutants are not taken into account for evaluating the score.