NuSMV 2.1 User Manual

• Introduction
• Tutorial
  • Examples
  • Simulation
  • CTL model checking
  • LTL model checking
  • Bounded Model Checking
• Syntax
  • Expressions
    • Simple Expressions
      • Case Expressions
      • Set Expressions
    • Next Expressions
  • Definition of the FSM
    • 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
  • Commands for Bounded Model Checking
  • Simulation Commands
  • Traces Inspection Commands
  • Interface to the DD Package
  • Administration Commands
  • Other Environment Variables
• Running NuSMV batch
• Bibliography
• Compatibility with CMU SMV
• Command Index
• Variable Index
• Index

This document was generated on 9 July 2002 using texi2html 1.56k.