NuSMV 2.0 User Manual

• Introduction
• Examples
• Syntax
  • Expressions
    • Simple Expressions
      • Case Expressions
      • Set Expressions
    • Next Expressions
  • Definition of the Kripke structure
    • State Variables
      • Type Specifiers
    • Input Variables
    • ASSIGN declarations
    • TRANS declarations
    • INIT declarations
    • INVAR declarations
    • DEFINE declarations
    • ISA declarations
    • MODULE declarations
    • Identifiers
    • The main module
    • Processes
    • FAIRNESS declarations
  • Specifications
    • CTL Specifications
    • LTL Specifications
    • Real Time CTL Specifications and Computations
• Running NuSMV interactively
  • Model Reading and Building
  • Commands for Checking Specifications
  • Simulation Commands
  • Traces Inspection Commands
  • Interface to the DD Package
  • Administration Commands
  • Other Environment Variables
• Running NuSMV batch
• Getting started with BMC
  • A simple model
  • Checking of LTL properties
  • Checking of invariant properties
  • Further information
  • BMC commands details
    • Relevant environment variables
    • BMC commands for checking of LTL specifications
    • BMC commands for checking of invariants
    • BMC commands for DIMACS files generation
    • BMC commands for simulation
• Bibliography
• Compatibility with CMU SMV
• New reserved words
• Command Index
• Variable Index
• Index

This document was generated on 6 November 2001 using texi2html 1.56k.