This package contains test-cases for the model-checking direct analyses.