evidential-calculator

This repository contains a prototypical implementation of a tool that calculates the evidence sets of different classes of evidence.

If you just want to quickly try the tool, you may use the provided Dockerfile (see Usage via Docker).

Usage

General Usage

Using the provided tool is straightforward, just supply a model, which is defined in NuSMV’s input specification language either by piping it into stdin or as a positional argument. In addition to that, specify the class of evidence that should be calculated via -t (either “sufficient” or “necessary” evidence).

cat examples/models/acme-model.smv | python3.9 src/calc_evidence.py -t "sufficient"

If you are only interested in a specific action, you could restrict the calculation to that action by supplying -a, like it is illustrated below:

python3 src/calc_evidence.py -a "add_job_b" -t "sufficient" examples/models/acme-model.smv

For a full reference of the CLI, see the manual page below, or run calc_evidence.py with --help.

usage: calc_evidence.py [-h] [-a ACTION] [-t {sufficient,necessary}] [-o {csv,raw}] [model]

positional arguments:
  model                 Model specified in NuSMV's input language. If not specified read from STDIN

optional arguments:
  -h, --help            show this help message and exit
  -a ACTION, --action ACTION
                        Name of the action of interest. Consider all actions if not specified.
  -t {sufficient,necessary}, --etype {sufficient,necessary}
                        Type of evidence to calculate
  -o {csv,raw}, --output-format {csv,raw}
                        Output format of the calculated sets

Usage via Docker

For quick tryouts, we provide a Dockerfile. Build it by running the following command:

docker build . -t evic

Then, use it by mapping the current working directory into the containers /data-directory and providing the exemplary model to the entrypoint:

docker run -it -v $(pwd):/data evic calc_evidence.py -t sufficient /data/examples/models/lst-4.smv

Installation

Dependencies

The code depends on PyNuSMV, which is included as a submodule. In order to compile it, ensure that you have the following prerequisites installed. Please note that PyNuSMV requires Python 3.9.8.

Assuming you are using Debian 11 (Codename Bullseye), you can run the following commands.

sudo apt install build-essential zip zlib1g-dev libexpat-dev flex bison swig patchelf
sudo apt install python3 python3-dev libpython3-dev python3-pip

If you are running a distro, install Python 3.9.8 from source, like so:

wget https://www.python.org/ftp/python/3.9.8/Python-3.9.8.tgz
tar -xvf Python-3.9.8.tgz
cd Python-3.9.8
./configure --enable-optimizations
make -j $(nproc)
make altinstall

Install Module Via Python’s Package Manager pip

In case you want to install the module named evidence_set_calculation, you could run

pip3 install .

which will install the module as well as the script calc_evidence.

Install Requirements Only

If you want to try the tool or modify the sources, it is best to create a virtual environment named venv and install the requirements in there, like so:

python3.9 -m venv venv
source venv/bin/activate
pip3 install -r requirements.txt