• The input of NuSMV is designed to allow for the description of a Finite Machine State FSM (Synchronus and Asynchronus)
• The only datatypes in the language are finite ones (booleans, scalars & fixed arrays)

Purpose

The purpose of the NuSMV input is to describe the transition relation of the FSM