Model Checking is a formal technique for the verification of finite systems. However, it is well known that this technique suffers from the state explosion problem. We describe work in progress to implement in the TINA toolbox an enumerative variant of a state based observation graph algorithm defined by Klai and Poitrenaud.