While model checking can be a very useful tool for hardware and software development, one of the downsides is a high computation time once the models become more complex. One of the tools used for model checking is the NuSMV model checker, which (partially) uses symbolic model checking based on binary decision diagrams to verify models for given specifications. This thesis will present a new perspective, taking a closer look at the graphs generated by NuSMV and make comparisons to the source codes. Results of this might give insight on possible future improvements.