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.