Next: The semantic check module.
Up: System Architecture
This module performs the encoding of data types and finite ranges into
boolean domains. Having this module as a separate one makes it possible to
have different encoding policies that can be more appropriate for different
kinds of variables. Currently only the standard CMU SMV encoding is possible,
but there are plans to integrate into this architecture other forms of
encoding, e.g., those used in Word-Level SMV .