NuSMV-ARCTL-TLACE is a modified version of NuSMV 2.2.2. NuSMV 2.2.2 has been extended with two new functionalities. The first extension is the model checking of ARCTL, an extension of CTL including actions. It has been mainly implemented by Franco Raimondi. He has implemented the model checking algorithms. José Vander Meulen has then implemented the generation of counterexamples of ARCTL specifications. The second extension is the generation of enriched counterexamples: tree-like annotated counterexamples (TLACEs), implemented by Simon Busard. The provided version is a merge of the two extensions. First, it allows to model check ARCTL specifications over SMV models, then it allows to generate TLACEs explaining why an (AR)CTL specification is not satisfied by a given model. ------------ INSTALLATION ------------ Standard procedure (linux) -------------------------- To install the tool, use the standard installation procedure for NuSMV: cd cudd-2.3.0.1; make # Compile CUDD cd ../nusmv; ./configure make More information is given in nusmv/INSTALL. Mac OS X -------- To install the tool on Mac OS X, use the following procedure: cd cudd-2.3.0.1; make -f Makefile_os_x_64bit # Compile CUDD using OS X makefile cd ../nusmv ./configure CC="gcc -m32" # Configure NuSMV to use gcc with -m32 option make More information is given in nusmv/INSTALL. ------------- DOCUMENTATION ------------- ARCTL ----- Some information about the model checking of ARCTL can be found in the ARCTL/ directory. This directory contains a short document explaining what has been done and a CHANGELOG containing all the changes made to the initial version of NuSMV 2.2.2 by F. Raimondi. Some examples of model checking of ARCTL can be found in ARCTL/examples. TLACE ----- Manuals and references The generation of TLACEs is widely discussed in the master thesis of Simon Busard, given in the TLACE/ directory (TLACE/thesis.pdf). A short manual is given in TLACE/manual.pdf. It explains how to invoke the added functionalities and how to use the tool implemented to visualize TLACEs. A CHANGELOG file is given in TLACE/CHANGELOG.pdf. It describes the changes made to NuSMV-ARCTL, i.e. the version of NuSMV 2.2.2 modified to integrate the model checking of ARCTL. Examples Some SMV models are provided to be able to test the new functionalities. They are given in the TLACE/examples directory. A README file shortly explaining how to run them is given. ------- CONTENT ------- This archive contains: - an AUTHORS file giving the names and emails of people that developed this modified version of NuSMV 2.2.2. - a CHANGELOG file explaining how to get the changes made to NuSMV 2.2.2. - the sources of CUDD (cudd-2.3.0.1/ directory) used by NuSMV to manipulate BDDs. - the sources of NuSMV (nusmv/ directory). - the ARCTL directory containing all given material about the ARCTL extension. - the TLACE directory containing all given material about the TLACE extension. - this file. --------- COPYRIGHT --------- NuSMV-ARCTL-TLACE is licensed under the GNU Lesser General Public License (LGPL in short). File LGPL-2.1 contains a copy of the License. ------- CREDITS ------- NuSMV-ARCTL-TLACE is maintained and distributed by the LVL Group at Université catholique de Louvain. Please contact for any question regarding this software distribution. The following people contributed to this specific extension of NuSMV: * Simon Busard * José Vander Meulen * Franco Raimondi NuSMV is a symbolic model checker developed as a joint project between several partners and distributed under the GNU LGPL license. Please contact for getting in touch with the NuSMV development staff.