The SMV language can be divided roughly into three parts - the definitional language, the structural language, and the language of expressions. The definitional part of the language declares signals and their relationship to each other. It includes type declarations and assignments. The structural part of the language combines definitional components. It provides language constructs for defining modules and structured data types, and for instantiating them. It also provides constructor loops, for describing regularly structured systems, and a collection of conditional structures that make describing complicated state transition tables easier. Finally, expressions in SMV are very similar to expressions in other languages, both hardware description languages and programming languages. For this reason, expressions will be discussed last, as any expressions appearing in discussions of other parts of the language should be self explanatory.