1. added nusmv for monolithic; 2. added func tests for parameterized
restructuring, added monolithic func tests, changed configuration procedure