Contents

• Preface
• Contents
• List of Figures
• 1. Introduction
  • 1.1 Overview
  • 1.2 Form of representation
• 2. Foundations
  • 2.1 Getting started
  • 2.2 General rules for the dialogue with INA
  • 2.3 Files, extensions, formats and the entering of nets
    • 2.3.1 Important files
    • 2.3.2 File extensions
    • 2.3.3 Entering nets
    • 2.3.4 File formats
  • 2.4 The structure of an INA -session
    • 2.4.1 Starting and exiting INA
    • 2.4.2 The session report
    • 2.4.3 Analysis of several nets following the same pattern
  • 2.5 Options
    • 2.5.1 Token types
    • 2.5.2 Time option
    • 2.5.3 Firing rule
    • 2.5.4 Priorities
    • 2.5.5 Firing strategy
    • 2.5.6 Line length
• 3. Editor
  • 3.1 Reading and writing
  • 3.2 Deleting and changing
  • 3.3 Merging
• 4. Firing
  • 4.1 Fundamentals
  • 4.2 State representations
    • 4.2.1 State representation without time allocation
    • 4.2.2 State representation under time allocation
  • 4.3 Auxiliary functions
  • 4.4 Firing Functions
    • 4.4.1 General remarks
    • 4.4.2 Firing under time constraints
  • 4.5 Example
• 5. Reduction
  • 5.1 Fundamentals
  • 5.2 Auxiliary functions
  • 5.3 Reduction procedures
• 6. Analysis
  • 6.1 Fundamentals
  • 6.2 Analysis status
    • 6.2.1 Elementary net properties
    • 6.2.2 Further properties
  • 6.3 Analysis menu and pre-analysis
  • 6.4 Simplex oriented methods
    • 6.4.1 Fast boundedness test
    • 6.4.2 Fast non-reachability test
  • 6.5 Reachability analysis
    • 6.5.1 Reductions of the state graph
    • 6.5.2 Predicates and CTL model checking
    • 6.5.3 Computation of paths
    • 6.5.4 Computation and analysis of graphs
  • 6.6 Invariant analysis
    • 6.6.1 Computing invariants
    • 6.6.2 Semipositive invariants
    • 6.6.3 Testing invariants
  • 6.7 Structural analysis
• Bibliography
• Index
• About this manual