MuAlloy: A Mutation Testing Framework for Alloy

MuAlloy is a command line tool built on top of Alloy4.2. The tool provides basic features to mutate an Alloy model at its AST level and generate non-equivalent mutant models. For each non-equivalent mutant model, MuAlloy is able to generate an Alloy instance that kills it. All mutant killing instances can be encoded as AUnit tests and saved on the disk. MuAlloy can also run mutation testing on any model given some tests.

Requirements:

• Operating Systems

  • Linux (64 bit)
  • Mac OS (64 bit)

• Dependencies

  • Java 8: Must be installed and accessible from PATH.
  • Bash 4.4: Must be installed and accessible from PATH.
  • Gradle 4.3.1: Must be installed and accessible from PATH.
  • Alloy 4.2: Must be in the classpath. MuAlloy comes with Alloy4.2 under libs/alloy4.2.jar.
  • Commons CLI 1.4: Must be in the classpath. MuAlloy comes with Commons CLI under libs/commons-cli-1.4.jar.

Installation:

Clone MuAlloy repo

To run MuAlloy, use git to clone the repository.

git clone git@github.com:kaiyuanw/MuAlloy.git

Build MuAlloy

To build MuAlloy, Java 8 and Gradle 4.3.1 must be installed. Then, you can run ./mualloy.sh --build in Bash 4.4 to build MuAlloy.

Quick Start:

Generate Mutants

To generate mutants, run

./mualloy.sh --generate-mutants -o <arg> -m <arg> [-s <arg>] [-t <arg>]

or use the full argument name

./mualloy.sh --generate-mutants --model-path <arg> --mutant-dir <arg> [--scope <arg>] [--test-path <arg>]

• -o,--model-path: This argument is required. Pass the model you want to mutate as the argument.
• -m,--mutant-dir: This argument is required. Pass the directory to which you want to save mutants as the argument. If the directory does not exist, a new directory will be created.
• -s,--scope: This argument is optional. Pass the Alloy scope for equivalence checking, which is mainly used to prune equivalent mutants. For each non-equivalent mutant, the scope will also be used to generate a run command for the corresponding AUnit test that kills the mutant. If the argument is not specified, a default value of 3 is used.
• -t,--test-path: This argument is optional. Pass the path to which you want to save mutant killing test suite as the argument. If the argument is not specified, no mutant killing test suite will be generated. Note that the generated test suite only contains unique test predicates and the corresponding run commands.

The command also reports the number of equivalent mutants, non-equivalent mutants and unique tests.

Mutation Testing

To run mutation testing, run

./mualloy.sh --run-mutation-testing -o <arg> -m <arg> -t <arg>

or use the full argument name

./mualloy.sh --run-mutation-testing --model-path <arg> --mutant-dir <arg> --test-path <arg>

• -o,--model-path: This argument is required. Pass the original model as the argument. MuAlloy collects the test satisfiability result for the original model and then compare it with the test result for a mutant model. If the results are different, then the mutant is killed. Otherwise, it is not.
• -m,--mutant-dir: This argument is required. Pass the directory to which mutants are saved as the argument. MuAlloy collects test results for each of the mutant models and checks if it can be killed by the test suite or not.
• -t,--test-path: This argument is required. Pass the test suite you want to run as the argument. MuAlloy runs the test suite against the original model and mutant models to compute the mutation score for the test suite. Note that the test suite should only contain the test predicates and the corresponding run commands.

The command also reports whether each mutant is killed by the test suite or not. After MuAlloy finishes running the test suite against all mutants, the command reports the mutation score.

Included Examples

MuAlloy provides 13 example models and the commands to generate mutants and collect mutation score for each model. The experiments/models directory contains all example models and some of them come from the standard Alloy distribution:

• addr: Models an address book.
• bempl: Models a toy lab security policy.
• binaryTree: Models an arbitrary binary tree.
• ctree: Models a two colored undirected tree.
• dijkstra: Models how mutexes are grabbed and released by processes, and how Dijkstra's mutex ordering criterion can prevent deadlocks.
• farmer: Models the farmer crossing river problem.
• fullTree: Models a full binary tree.
• grade: Models a grade book.
• grand: Models an "I'm my own grandpa" puzzle.
• handshake: Models Halmos handshake problem.
• nqueens: Models N queens problem.
• other: Models another toy lab security policy.
• singlyLinkedList: Models an acyclic singly linked list.

To generate mutants for a given example model, run

./mualloy.sh --generate-mutants-example ${model}

where ${model} can be one of [addr, bempl, binaryTree, ctree, dijkstra, farmer, fullTree, grade, grand, handshake, nqueens, other, singlyLinkedList]. By default, MuAlloy reads the model from experiments/models/${model}.als and generates mutants under experiments/gen/${model} directory. MuAlloy saves the mutant killing test suite at experiments/gen/tests/${model}.als. The scope used varies for different models. For more details, take a look at models.sh.

To generate mutants for all 13 example models, run

./mualloy.sh --generate-mutants-example-all

To run mutation testing for a given example model and a test suite, run

./mualloy.sh --run-mutation-testing-example "${model}"

where ${model} can be one of [addr, bempl, binaryTree, ctree, dijkstra, farmer, fullTree, grade, grand, handshake, nqueens, other, singlyLinkedList]. By default, MuAlloy reads the model and mutants from experiments/models/${model}.als and experiments/gen/${model} directory, respectively. This means you should first generate mutants for example models and then run mutation testing. MuAlloy reads the test suite at experiments/test-suite/${model}.als. Note that the test suites under experiments/test-suite are actually generated using MuAlloy so all mutants should be killed.

To run mutation testing for all 13 example models, run

./mualloy.sh --run-mutation-testing-example-all

Mutation Operators

MuAlloy supports the following mutation operators.

Operator	Description
MOR	Multiplicity Operator Replacement. E.g. some sig S => lone sig S
QOR	Quantifier Operator Replacement. E.g. all s: S => some s: S
UOR	Unary Operator Replacement. E.g. some S => no S
BOR	Binary Operator Replacement. E.g. a + b => a - b
LOR	Formula List Operator Replacement. E.g. a && b => a || b
UOI	Unary Operator Insertion. E.g. a.b => a.*b
UOD	Unary Operator Deletion. E.g. a.^b => a.b
BOE	Binary Operator Exchange. E.g. a - b => b - a
IEOE	Imply-Else Operator Exchange. E.g. a => b else c => a => c else b

The full mutations are shown below:

• MOR: ${x} sig S {...} to ${y} sig S {...} where ${x}, ${y} ∈ {ε, lone, one, some}. ε means empty string and it represents set multiplicity in Alloy signature declaration by default.
• QOR: ${x} s: S | ... to ${y} s: S | ... where ${x}, ${y} ∈ {all, no, lone, one, some}.
• UOR: s: ${x} S to s: ${y} S where ${x}, ${y} ∈ {set, lone, one, some}; ${x} S to ${y} S where ${x}, ${y} ∈ {no, lone, one, some}; a.${x}b to a.${y}b where ${x}, ${y} ∈ {*, ^}.
• BOR: a ${x} b to a ${y} b where ${x}, ${y} ∈ {+, &, -} or {=, !=, in, !in} or {=>, <=>}.
• LOR: a ${x} b ${x} ... to a ${y} b ${y} ... where ${x}, ${y} ∈ {&&, ||}.
• UOI: a to ${x}a where ${x} ∈ {*, ^, ~}.
• UOD: ${x}a to a where ${x} ∈ {*, ^, ~} or {!}.
• BOE: a ${x} b to b ${x} a where ${x} ∈ {-} or {in, !in, =>}.
• IEOE: a => b else c to a => c else b.

When the above mutation operators involve both ${x} and ${y}, they cannot be the same relational operator.

Background

Alloy Model

We show an acyclic singly linked list Alloy model below:

module SinglyLinkedList
sig List {
  header: lone Node
}
sig Node {
  link: lone Node
}
pred Acyclic (l: List) {
  no l.header or some n: l.header.*link | no n.link 
}
run Acyclic

The model declares a set of List and Node atoms. Each List atom has zero or one header of type Node. Each Node atom has zero or one following Node along link. header and link are partial functions. The predicate Acyclic restricts its parameter l to be acyclic. The body of the Acyclic predicate states that l is acyclic if (1) it does not have an header or (2) there exists some Node reachable from l's header following zero or more link, such that the Node does not have a subsequent node along the link.

Alloy Instance

Below is an satisfiable Alloy instance for the above list model if we run the Acyclic predicate:

The instance states that there are two List atoms (List0 and List1) and two Node atoms (Node0 and Node1). List0's header is Node1 and List1's header is Node0. Node1's next node is Node0. Assuming List0 is implicitly passed as the argument of Acyclic predicate, we can see that List0 is indeed acyclic as there is no loop in the list.

AUnit Test

An AUnit test is a pair of a model valuation and a run command. For example, the above Alloy instance can be written as an AUnit test as below:

pred test {
  some disj List0, List1: List {
    some disj Node0, Node1: Node {
      List = List0 + List1
      header = List0->Node1 + List1->Node0
      Node = Node0 + Node1
      link = Node1->Node0
      Acyclic[List0]
    }
  }
}
run test

The test declares 2 disjoint List atoms (List0 and List1) and 2 disjoint Node atoms (Node0 and Node1). It restricts the entire List set to be {List0, List1} and Node set to be {Node0, Node1}. The predicate also states that the header maps List0 to Node1 and List1 to Node0, and the link maps Node1 to Node0. If you run the test predicate, you will obtain the isomorphic Alloy instance shown above.

Killing Mutant

One of the mutant MuAlloy generates from the list example model using QOR is shown below:

module SinglyLinkedList
sig List {
  header: lone Node
}
sig Node {
  link: lone Node
}
pred Acyclic (l: List) {
  no l.header or all n: l.header.*link | no n.link 
}
run Acyclic

MuAlloy mutates some n: ... to all n: ..., which restricts every Node in l without a subsequent Node along the link. This overconstrains l so it can be empty or only have one Node. The above AUnit test will be unsatisfiable for List0 as Node1 has a subsequent node Node0. Since the test is satisfiable for the original model but is unsatisfiable for the mutant, it kills the mutant. Similarly, if an AUnit test is unsatisfiable for the original model but is satisfiable for the mutant, it also kills the mutant.

Limitation

MuAlloy currently does not support mutating AST nodes declared inside signature facts because the equivalence checking is not supported for now. The workaround is to move signature fact to a stand-alone fact declaration. We may support mutating signature facts in a future release.

Publications

• "Towards a Test Automation Framework for Alloy." Allison Sullivan, Razieh Nokhbeh Zaeem, Sarfraz Khurshid, and Darko Marinov, SPIN 2014
• "MuAlloy : An automated mutation system for Alloy." Kaiyuan Wang, Master Thesis 2015
• "Automated Test Generation and Mutation Testing for Alloy." Allison Sullivan, Kaiyuan Wang, Razieh Nokhbeh Zaeem, and Sarfraz Khurshid, ICST 2017
• "MuAlloy: A Mutation Testing Framework for Alloy." Kaiyuan Wang, Allison Sullivan, and Sarfraz Khurshid, ICSE 2018

License

MIT License, see LICENSE for more information.