LAC operon in NuSMV

This is a model of the lac operon regulation. It is an executable NuSMV model obtained by translation from a sync-program model developed for the paper "Modular Verification of Interactive Systems with an Application to Biology" by P. Drabik, A.Maggiolo-Schettini and P. Milazzo.