BeAFix

BeAFix

Our tool extends AlloyAnalyzer 5.1.0, and tries to repair an Alloy model marked with expressions to be mutated. It supports repairing expressions inside facts, assertions, functions, and predicates. A marked expression has the form {#m#([vars]) expression} where vars is a comma separated list of variables related to the marked expression, this is used by the variabilization pruning technique. As an example we can consider the following marked expressions:

• {#m#() some x : T | P[x]} where the whole quantifier expression is marked for mutation.

• some x : T | {#m#(x) P[x]} where only a part of an expression is marked for mutation.

Our technique is based on exhaustive search of repair candidates (generated by applying mutation operators) up to a certain bound (amount of mutations per marked expressions and/or a specific amount of time). As a way to reduce how many candidates we need to visit in our search, we use several pruning techniques as well as prioritizing partially repaired candidates.

Our tools is in constant development, the paper's version is found in the replication package. But if you want to run custom experiments or "play" with the tool, we suggest using the latest version. Requirements are Java 8, macOs or Linux (on Windows 10 Alloy Analyzer doesn't seem to work because of missing libraries). The latest version of our tool can be found in the releases section of our repository.

Mutation Operators

• AORB : Replaces binary arithmetic operators (division, multiplication, modulo, addition and subtraction).

• BES : Given a binary expression returns both operands as mutations (a op b -> {a, b}).

• BESOR : Replaces binary set operators (join, union, diff, intersection, and overriding).

• COR : Replaces binary conditional operators (and, or, implies, and if and only if).

• CUOI : Negates a boolean expression.

• EMOR : Replaces equality operators by membership operators:

  • • • • • == <-> in

          • != <-> !in

• JEE : Extends a join expression, given a.b it can generate expressions like a.b.c and a.x.y.

• JER : Replaces part of a join expression, given a.b it can generate expressions like a.x but will not generate expressions like x.y (which replaces more than one join operand).

• JES : Reduces a join expression by either removing one join operand or replacing a join expression with another expression with no joins (variables, signatures, fields).

• MOR : Replaces multiplicity operators in a unary expression (no, some, lone, one).

• NESE : Given an expression A, this operator will add, for each variable or join x, some x => A. For example,
  list'.rest = list and list'.element = e will be mutated to
  (some list'.rest && some list && some list'.element && some e) => list'.rest = list and list'.element = e.

• QTOI : Given an expression x, this operators generates no x, some x, lone x, and one x.

• QTOR : Replaces the operator in a quantifier expression (all, lone, no, one, and some), for the moment comprehension and sum operators are not considered.

• ROR : Replaces relational binary operators (equal, not equal, greater, not greater, greater or equal, not greater or equal, less, not less, less or equal, and not less or equal).

• RUOD : Deletes unary relational operators (transpose, closure, and reflexive closure).

• RUOI : Inserts unary relational operators (transpose, closure, and reflexive closure).

• RUOR : Replaces unary relational operators (transpose, closure, and reflexive closure).

• SSE : Extends an expression that can be viewed as a set, for example: x can be mutated to x + y.

• SSS : Reduces an expression that can be viewed as a set, for example: x can be mutated to x - y.

• VCR : Replaces a field, signature, variable, or constant, which is not a part of a join expression, with reachable variables, signatures, fields, and, constants.

All mutations are both type checked (although some invalid mutations can happen); irrelevant mutations are also analysed and skipped, as for example, adding a closure operator to an expression with a reflexive closure operator; and finally, repeated expressions are also detected and removed from analysis.

Adding Mutation Operators

BeAFix core is implemented in org.alloytools.alloy.core.are.edu.unrc.dc.mutation. Inside the op subpackage are all operators. Any new implemented operator must then be added to Ops enum, overriding the necesessary methods:

• isImplemented() : boolean must return either true or false and will determine if that operator will be used.

• getOperator(CompModule) : Mutator must return the implemented operator inside the op subpackage.

• getComplexity() : Int must return a positive number that will determine in which order (w.r.t. other operators) the operator will be used.

Command Line Interface Version (CLI)

To run the CLI version you need the corresponding jar file (the one that has CLI in the name) and execute java -jar <BeAFixCLI jar> --help to see how to run the tool.

Graphical User Interface Version (GUI)

BeAFix has an Graphical User Interface build upon the Alloy Analyzer. This extension allows users to perform the reparation process in an interactive and graphical way.

BeAFix GUI configuration options

• Variabilization: Enables/disables variabilization pruning technique (default is false).

• Variabilization Test Generation: Enables/disables test generation for variabilization, alternatively manual variabilization tests (run commands with expect 1) can be written and marked with #t# before the run command, any auxiliary signature used for these tests can also be marked with #t# before the signature definition.

• Max tests per command: How many counterexample-based tests will be generated for each check or run ... expect 0 command, this is used for variabilization, default value is 4.

• Tests per generation: How many tests will be generated each time a counterexample is found, this is an upper bound on the amount of instances returned by the solver, default is 1.

• Use expression type: If variabilization will use expressions exact types for constructed relations or more general ones (default and suggested is false).

• User Partial Repair (Guided Search): When enabled this will give priority to candidates for which previously unsatisfied properties are now satisfied (this only works for properties involving only one buggy predicate or function).

• User Partial Repair (Pruning): Enabled/disables partial pruning technique (default is false).

• Full call graph validation: When using any partial repair option, enabling this will result in analyzing all the call graph, instead of a more superficial analysis, default and suggested is true.

• Require independent test for all: When using partial repair, enabling this will require all buggy functions and/or predicated have at least one independent command (only calls one of the buggy functions/predicates) for partial repair to work, instead of allowing partial repair only on those function/predicates that have at least one independent command.

• Timeout: Time budget (in minutes) for the repair process (default is 0, unlimited).

• Use perfect oracle tests to validate repair: This will use any command marked by #po# to only be used after a repair is found to validate if it is spurious or not, this is only useful if tests are used instead of property based oracles, default is false.

• Max mutations per expression: How many mutations are allowed per marked expression (default is 2).

• Mutations per candidate (*): The maximum mutant generation that can be achieved, default is 0 (unlimited).

• Check mutants with existing command (*): Check each mutant to discard those invalid or semantically equivalent to the original model.

• ARepair integration (**): Used to generate tests that can be used by ARepair.

• ARepair integration relaxed (**): Allows test generation from assertions and predicates using more than one predicate or function.

• ARepair integration no instance tests if no facts (**): When a model has no facts and a test stating that an instance should not satisfy a predicate, a related test forcing the existance of that instance will not be generated.

• ARepair integration instance tests branches (**): For tests generated from predicates, which branch to generate (POS: an instance should satisfy the predicate; NEG: an instance should not satisfy the predicate; or BOTH).

• ARepair integration relaxed facts (**): When tests cannot be generated from either assertions or predicates, this will try test generation from predicates by relaxing the models facts.

• ARepair integration force assertion tests (**): When no tests can be generated from assertions, this option will cause assertions to be transformed into predicates and to generate tests from those.

• Use model overrides (**): Enables/disabled overriding certain fields or signatures by functions when generating a test (usefull for generating tests that use ordering).

• Instance based tests (**): Enables/disables generation of tests from run ... expect 1 commands.

• Base test name (**): The base name used for all generated tests, tests will be named <base name><incrementing index>.

• Base test name starting index (**): Starting index for generated tests names.

• Model override folder (**): When model overrides is enabled, this states a folder containing files where the overrides are stored; file name should be <model>.overrides and each line must be type.<name>=<overriding> where type is either signature, field, or function; name is the correspoding signature, field, or function name and overriding is either IGNORE or type.<name>. For example: ordering.overrides with field.First=function.first.

• Buggy funcs file (**): Allow to define buggy functions/predicate/facts so test generation can know which can be trusted and which can't. Lines must be func:<name> for functions and predicates; fact:<name> for named facts; and fact:sig:<name> for signature facts.

(*): Only used for the Generate mutants option in execute menu.
(**): Only used for the Generate tests option in execute menu.

Developers

BeAFix was developed and is currently maintained by:

• Simón Gutiérrez Brida (sgutierrez@dc.exa.unrc.edu.ar | https://github.com/saiema)

• Germán Regis (gregis@dc.exa.unrc.edu.ar | https://github.com/gregistecco)

• Guolong Zheng (gzheng@cse.unl.edu | https://github.com/guolong-zheng)