PRISMA

This is PRISMA, a web-based reasoning tool to generate realistic model instances that satisfy a given set of constraints.

The tool first uses a goal-directed reasoning to produce an initial set of tuple instances (aka EDB) and allows users to replace the abstract values with realistic data. To do so, PRISMA supports two workflows:

• LLM-based, where users specify domain bounds and descriptions to guide an LLM that will generate data, and
• CSV-based loading.

Both of them produce refined EDB instances that maintain logical consistency while incorporating domain-appropriate realistic values. This way, our tool can obtain human-readable data examples that can prove/disprove model reasoning problems (e.g. state reachability, class liveliness, constraint redundancy, etc).

This tool is developed by inLab FIB - UPC [https://inlab.fib.upc.edu/]

Services

Service	Description	External Port
frontend	Web UI (served via Nginx)	3000
backend	REST API	Internal only
ollama	Local LLM inference engine	Internal only

Only the frontend is accessible from outside Docker. Backend and Ollama communicate internally via the prisma-net network.

Requirements

• Docker with Docker Compose

Configuration

Create a .env file in the project root if you want to use Google Gemini:

GOOGLE_GEMINI_API_KEY=your_key_here

If not set, the variable defaults to empty and the application uses Ollama only.

Usage

Start:

docker compose up -d

Stop:

docker compose down

Access the application: http://localhost:3000

Persistent Data

Ollama model data is stored in the ollama_data Docker volume and persists across restarts.

Paper experiments

The standalone experiment runner, fixed paper configuration and Docker Compose instructions are documented in experiments/README.md.