Pramana

Pramana (Beta) Installation

This section describes the installation of Pramana (Beta).

Creating a New Input Meta-model (Optional)

This section describes the creation of a new input meta-model (if needed) to describe an input domain.

Declarative Specification Generation

This section describes the setup of different parameters required to generate an Alloy declarative model for a new or an existing meta-model. We then show how an Alloy model can be generated from the input meta-model.

Inserting Invariants

This section describes the insertion of additional invariants in the generated Alloy model. This is a manual step at the moment. We intend to automatically transform a subset of the Object Constraint Language (OCL) to Alloy a future version of Pramana.

Generation of Models

In this section we describe how an experiment available as an Alloy model is solved leading to model generation. We specify parameters such as number of models per criteria and SAT solver used.

Transforming Instances to Models

We show how XML solution instances generated by Alloy are transformed to XMI models that conform to the input meta-model.

Reading Models

This section briefly describes how the generated models can be read or used for testing.

Limitations

This section present current limitations of Pramana which we hope to resolve in the coming months...stay tuned :-)

Pramana Logo

Pramana's Logo. The tool is inspired by the french explorer Jacques Cartier. The tool explores the design space of test models.

Related Documents

This section contains publications related to Pramana

Pramana Download

The directory contains Pramana's source code.

Create New Meta-model

This image describes the create of a new meta-model using the Ecore diagram editor

AlloyMetamodel-en

 

Pramana Developer's documentation

This document is a developer's documentation for the work in progress around Pramana