LTL Verifier for C FSM

Kripkomat is a small utility which analyzes a C finite state machine and generates a NuSMV model. Properties are extracted automatically.

This is very much a proof of concept.