************************************************************************* SMV BDD Trace Files Bwolen Yang School of Computer Science Carnegie Mellon University bwolen@cs.cmu.edu Last Modified: 8/98 ************************************************************************* This directory contains BDD trace files generated by SMV. From all the SMV models we gathered, we selected a few with running time ranging from 40 seconds to more than an hour and generate its BDD traces. The version of SMV used is based on SMV 2.4.4 with a new conjunctive partitioning algorithm and some improvements on the BDD package. The specification evaluation routines and the counterexample generation routines are not modified. The following is a brief description of each SMV model used, its author(s), and the SMV options used. These trace files are generated on 248MHz UltraSPARC II with 24-hour time limit and 1.2-GByte memory limit. --------------------------------------------------------------------------- short -- A very small file from SMV release's example short.smv. The SMV modeling file short.smv is included at the top of this trace file. This short file is included for illustrative and debugging purposes. --------------------------------------------------------------------------- abp11 -- 11-bit alternating bit protocol. Author: Armin Biere (armin@ira.uka.de, armin@cs.cmu.edu). Execution flags: -k 2690867 -c 2690867 -cp 10000 --------------------------------------------------------------------------- dme2-16 -- Distributed mutual exclusion protocol. Source: Scaled up version of dme2 from the example directory of the SMV distribution. Execution flags: -k 2690867 -c 2690867 -f --------------------------------------------------------------------------- dartes -- communication protocol of an complex Ada program. dpd75 -- dining philosophers with dictionary. ftp3 -- file transfer program. furnace17 -- remote furnace program. key10 -- manages keyboard/screen interaction in a window manager. mmgt20 -- distributed memory manager. over12 -- automated highway system overtake protocol. Author: James Corbett (corbett@hawaii.edu) Execution flags: -k 2690867 -c 2690867 -f --------------------------------------------------------------------------- futurebus -- futurebus cache coherence protocol. Author: E. Clarke (emc@cs.cmu.edu), O. Grumberg, H. Hiraishi, S. Jha, D. Long, K. McMillan, L. Ness Execution flags: -k 2690867 -c 2690867 -f --------------------------------------------------------------------------- motors-stuck, valves-gates -- Batch reactor system models. Author: Scott T Probst (http://www.cheme.cmu.edu/who/faculty/powers/probst/html/research.html) Execution flags: -timeOut 86400 -k 2690867 -c 2690867 -f --------------------------------------------------------------------------- phone-async -- asynchronous model of a simple telephone system. phone-sync-CW -- synchronous model of a similar phone system with Call Waiting. Author: Malte Plath (M.C.Plath@cs.bham.ac.uk) Mark D. Ryan (M.D.Ryan@cs.bham.ac.uk) Execution flags: -timeOut 86400 -k 2690867 -c 2690867 -f --------------------------------------------------------------------------- tcas -- A model of part of a preliminary version of the system requirements specification of TCAS II (Traffic Alert and Collision Avoidance System II). TCAS II is an aircraft collision avoidance system required on most commercial aircraft in United States. Author: William Chan (wchan@cs.washington.edu) Execution flags: -k 2690867 -c 2690867 -cp 10000 --------------------------------------------------------------------------- tomasulo -- A preliminary buggy model for Tomasulo algorithm for out-of-order execution. Author: Yunshan Zhu (zhu+@cs.cmu.edu) Execution flags: -k 2690867 -c 2690867 -cp 10000 -f ---------------------------------------------------------------------------