# $Id: ReadMe,v 1.1 2006/06/24 01:02:15 schuppan Exp $ This archive contains models of the IEEE 1394 (FireWire) Tree Identify Protocol. The models were originally a contribution to a workshop on the IEEE 1394 (FireWire) protocol [1]. They are discussed in more detail in [2]. Overview ======== The model comes in two main flavors - for in the input language of CMU SMV, in directory 'bsmv', and - for the enhanced input language of Cadence SMV, in directory 'csmv'. The former gives good results with Bwolen Yang's version of SMV. CMU SMV, Cadence SMV, and NuSMV also work. The latter version can be used to do symmetry reduction or bounded model checking with Cadence SMV. Installation ============ Prerequisites - Bwolen Yang's or any other CMU SMV-compatible version of SMV - Cadence SMV - cpp, sed, make, bash, and some other UNIX tools To install - unpack the distribution file ('tar -xvz -f fac.tar.gz') - change to the directory ('cd fac') - edit configure and enter your path for Bwolen Yangs's version of SMV (or any other CMU-SMV compatible model checker) and for Cadence SMV. If no paths are entered, configure tries some default paths. - run configure ('./configure') - make prepare ('make prepare') Now you can do - 'make interleave' or - 'make sequential' or - 'make bmcinterleave' or - 'make bmcsequential' to generate and verify the models (this may take a long time), or - 'cd examples' to browse some of the examples. Examples ======== The examples directory contains some models that can be browsed or verified without using any of the scripts: - bsmv: models for Bwolen Yang's SMV - nodes_6_4_0.smv: 6 nodes, cycle, 4 ports, fully determined - nodes_6_4_1.smv: 6 nodes, cycle, 4 ports, force-root undetermined - nodes_6nc_4_0.smv: 6 nodes, no cycle, 4 ports, fully determinied - nodes_6nc_4_1.smv: 6 nodes, cycle, 4 ports, force-root undetermined - nodes_3_3_2.smv: 3 nodes, cycle, 3 ports, topology undetermined - nodes_3_3_3.smv: 6 nodes, cycle, 4 ports, fully undetermined - csmv-symm: models for symmetry reduction with Cadence SMV: - nodes_3_3_cfn.smv/.groups: 3 nodes, 3 ports, topology undetermined, no symmetry reduction - nodes_3_3_scfn.smv/.groups: 3 nodes, 3 ports, topology undetermined, symmetry reduction - nodes_3_3_n.smv/.groups: 3 nodes, 3 ports, fully undetermined, no symmetry reduction - nodes_3_3_sn.smv/.groups: 3 nodes, 3 ports, fully undetermined, symmetry reduction - csmv-bmc: models for bounded model checking with Cadence SMV: - nodes_2_3_det_0.smv: 2 nodes, 3 ports, fully determined, 0 iterations in root contention - nodes_2_3_det_2.smv: 2 nodes, 3 ports, fully determined, 2 iterations in root contention - nodes_2_3_n_0.smv: 2 nodes, 3 ports, fully undetermined, 0 iterations in root contention - nodes_2_3_n_2.smv: 2 nodes, 3 ports, fully undetermined, 2 iterations in root contention To verify, use - bsmv: bsmv -f MODEL - csmv-symm: csmv -force -persist -together -f -r -rev MODEL - csmv-bmc: csmv -force -bmc -l [20|28] MODEL where 'bsmv' is Bwolen Yang's SMV, 'csmv' Cadence SMV. Use '-l 20' for 0 iterations in root contention, '-l 28' for 2. Some Details ============ Makefile -------- The targets of the top-level Makefile are as follows: - 'all' is 'prepare' - 'prepare' builds generator for bsmv and sets up directory structure - 'sequential' builds and verifies models - in bsmv - in csmv only with symmetry reduction - verifies all models for bsmv then for csmv - 'interleave' builds and verifies models - in bsmv - in csmv only with symmetry reduction - verifies all models with small number of nodes first (interleaves between bsmv and csmv) - use this if you want to verify only up to a certain number of nodes but want to see flavors for bsmv and csmv - 'bmcsequential' as 'sequential' but does also bounded model checking - 'bmcinterleave' as 'interleave' but does also bounded model checking - 'clean' removes generator for bsmv - 'distclean' is 'clean' and removes also the data generated by the runs of the model checkers Modify TLIMIT in the top-level Makefile to change the wall clock limit (default: 6 h, i.e. a total run time of several days). timenodes --------- The script 'fac/bin/timenodes' generates and verifies all models discussed in [2]. It takes as command line parameters whether the top-level iteration should be on the model checker ('-sequential', bsmv first) or on the number of nodes ('-interleave', small models first), whether or not bounded model checking is enabled ('-nobmc'/'-bmc'), and the wall clock limit ('-t seconds'). CMU version ----------- The models for the CMU version are generated by a C-program, 'genall'. You can use 'genall' to generate a single model. For documentation see 'fac/bsmv/src/genall.c'. A script 'fac/bsmv/bin/timenode' invokes 'genall' and runs the model checker for a specific model with number of nodes, ports, determinism, and wall clock limit given on the command line. Cadence version --------------- The models for the Cadence version can be generated by setting some parameters in a single, generic input file, 'fac/csmv/lib/nodes_bmc.smv.in'. Modify this file to generate a single model. Some documentation is provided in that file. Two scripts exist for generating and model checking with symmetry reduction ('timenodesymm') and to do bounded model checking with that model ('timenodebmc'). Both scripts take number of nodes, ports, determinism, and wall clock limit as command line parameters. For 'timenodebmc' the number of iterations in root contention must also be specified. References ========== [1] S. Maharaj, J. Romijn, C. Shankland (eds.): Proceedings of the IEEE 1394 (FireWire) Workshop, Berlin, Germany, March 13th 2001. Department of Computing Science and Mathematics, University of Stirling, March 2001 [2] V. Schuppan and A. Biere: Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV. To be published in a special issue of Formal Aspects of Computing. Viktor Schuppan, Armin Biere Zurich, Oct 28 2002