ATGT with SMT solver for combinatorial testing with constraints

ATGT in the combinatorial command line interface flavor supports only constrained combinatorial interaction testing (CCIT) with the SMT solver Yices and it is a command line version. It is simpler to install and use than the complete ATGT tool.

Papers

For combinatorial testing see my papers published at TAP 2008, TAP 2009 (for the use of SMT solver), and in the Journal of Automated Reasoning.

Calvagna, Andrea and Gargantini, Angelo
A Formal Logic Approach to Constrained Combinatorial Testing
in Journal of Automated ReasoningSpringer Netherlands, vol. 45, n. 4 (2010): 331-358
[abstract][download][DOI]
Andrea Calvagna and Angelo Gargantini
Combining Satisfiability Solving and Heuristics to Constrained Combinatorial Interaction Testing
in Third International Conference on Tests And Proofs (TAP)Springer-Verlag (2009):27–42
[abstract][download][DOI]
Andrea Calvagna and Angelo Gargantini
A Logic-Based Approach to Combinatorial Testing with Constraints
in Tests and Proofs, Second International Conference, TAP, Prato, Italy, April 9-11, 2008. Proceedings (Eds. Bernhard Beckert and Reiner Hähnle) Springer, Lecture Notes in Computer Science, vol. 4966 (2008): 66-83
[abstract][download][DOI]

License

ATGT is released under the EPL license. For details about EPL see here.

Download

To download the jar file for ATGT SMT CCIT CLI, click here. To download the examples we use (including those we use for combinatorial testing), click here.

Documentation

Yices

For combinatorial cli, you need yices version 1. Download it from http://yices.csl.sri.com/. The simplest way is to use yices at command line. Check if it works:

[garganti@angelocompaq local]$ yices --help
Yices (version 1.0.34). Copyright 2005, 2006 SRI International.
GMP (version 5.0.4). Copyright Free Software Foundation, Inc.
Build date: Fri Feb 24 10:19:28 PST 2012
Usage: yices [ options ] [ filename ] 
Help:
  -?, --help                  -- This help message.
Main:
...

Alternatively, the JNA version of Yices can be used and it is much faster. Put the dll or the .so libary in your path. However, the current version with JNA does not support the constraints yet (TODO).

How to run atgt with SMT for CCIT

Download atgt_smt_ccit.jar. Open a command window, move to the directory where you saved atgt_smt_ccit.jar. Then type

$java -jar atgt_smt_ccit.jar <asmespec>

with the following options:

 <asmespec>                               : AsmetaL input file (e.g. spec.asm)
 -collect                                 : use collect (default:false)
 -order [NOVELTY | RANDOM | AS_GENERATED] : ordering TPs (NOVELTY default)
 -reduce                                  : reduce after generation (default:false)
 -solver [YICES | YICES_JNA | Z3_JNA]     : solver (yices default)
 -t N                                     : t-wise (default:2)
 -verbose                                 : be verbose


 Example: java -jar atgt_smt_ccit.jar  -collect -reduce -t 3 -verbose bbs.asm