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.


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.


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


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.



For combinatorial cli, you need yices version 1. Download it from 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                  -- This help message.

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

My sw links