Go to the first, previous, next, last section, table of contents.
ISA declarations
There are cases in which some parts of a module could be shared among
different modules, or could be used as a module themselves. In
NuSMV it is possible to declare the common parts as separate
modules, and then use the ISA declaration to import the common
parts inside a module declaration.
The syntax of an ISA declaration is as follows:
isa_declaration :: "ISA" atom
where atom must be the name of a declared module.
The ISA declaration can be thought as a simple macro expansion
command, because the body of the module referenced by an ISA
command is replaced to the ISA declaration.