#+title: evidential-calculator
#+options: toc:nil

Badges

#+html:
#+html:
#+html:
#+html:
#+html:

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 [[id:57261ec4-5032-4efb-b94d-27b2c3435eeb][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).

#+begin_src shell
cat examples/models/acme-model.smv | python3.9 src/calc_evidence.py -t "sufficient"
#+end_src

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:

#+begin_src shell
python3 src/calc_evidence.py -a "add_job_b" -t "sufficient" examples/models/acme-model.smv
#+end_src

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

#+begin_example
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
#+end_example
** Usage via Docker
For quick tryouts, we provide a Dockerfile. Build it by running the following
command:

#+begin_src shell
docker build . -t evic
#+end_src

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

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

• Installation
  ** Dependencies
  The code depends on [[https://github.com/LouvainVerificationLab/pynusmv][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.

#+begin_src shell
sudo apt install build-essential zip zlib1g-dev libexpat-dev flex bison swig patchelf
sudo apt install python3 python3-dev libpython3-dev python3-pip
#+end_src

If you are running a distro, install Python 3.9.8 from source, like so:
#+begin_src shell
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
#+end_src

** Install Module Via Python's Package Manager =pip=
In case you want to install the module named =evidence_set_calculation=,
you could run

#+begin_src shell
pip3 install .
#+end_src

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:

#+begin_src shell
python3.9 -m venv venv
source venv/bin/activate
pip3 install -r requirements.txt
#+end_src