next up previous
Next: Instantiation. Up: System Architecture Previous: System Architecture


This module provides all the parsing routines, which process a file written in NUSMV language, check its syntactic correctness, and build a parse tree representing the internal format of the input file. The same parsing routines are used to implement commands for the interaction shell, such as the specification at command line of new properties to be verified.

NuSMV <>