IVy Installation Notes

These instructions will allow a basic installation of the IVy language and checker. This sequence worked well on a fresh install of Debian 11. Ubuntu 20.04 may come with additional installation steps, some of which are listed at the bottom of this document.

Because this involves strange configurations with Python and other common programs, it may be good to install in a Docker container or virtual machine.

NOTE: It is not the most up-to-date version, but the only version of IVy I’ve been able to get to work recently is a few versions old (it can be installed from the archived microsoft repository, rather than the new kenmcmil or formal-verification-research respository). You’re welcome to try installing the new version, especially if you’re confident you can document the resolution to the errors it produces.

Prerequisites

IVy requires a great deal of prerequisites, but they can thankfully all be installed using the following sequence of commands:

sudo apt-get update
sudo apt-get install python2 g++ cmake python-ply git python-tk tix pkg-config libssl-dev curl libreadline-dev

IVy relies on python pointing to python2.7 rather than python3, so execute the following to link then check the python command:

sudo ln /usr/bin/python2 /usr/bin/python
python --version

Correct output indicates the version is python2.7.

Installing Pip2 is a bit of a challenge on newer systems, but the following sequence has always worked for me:

curl https://bootstrap.pypa.io/pip/2.7/get-pip.py --output get-pip.py
sudo python get-pip.py
sudo ln /usr/local/bin/pip2 /usr/bin/pip2

Verify the version of pip, it should correspond to python2.7. Then create a link like we did with python2.7.

pip2 --version
sudo ln /usr/local/bin/pip /usr/bin/pip
pip --version

Now let’s take care of the pygraphviz dependency, which is probably more involved than it should be:

sudo apt-get install graphviz graphviz-dev build-essential autoconf libtool pkg-config python-opengl python-pil python-pyrex python-pyside.qtopengl idle-python2.7 qt4-dev-tools qt4-designer libqtgui4 libqtcore4 libqt4-xml libqt4-test libqt4-script libqt4-network libqt4-dbus python-qt4 python-qt4-gl libgle3 python-dev libssl-dev python-dev graphviz libgraphviz-dev pkg-config python-dev build-essential libssl-dev libffi-dev      libxml2-dev libxslt1-dev zlib1g-dev python-pip libpcap-dev libpq-dev build-essential libssl-dev libffi-dev python-dev cmake libreadline-dev
sudo pip install pygraphviz

Make sure you’re in the folder you’d like to have IVy installed in. If you followed the dedicated VM or Docker advice, this is usually best left in the home directory.

Getting IVy and Submodules

There are three main places you can get IVy from. The current repository is at github.com/kenmcmil/ivy but you’ll need to take caution if you use it. An old but more reliable repository is at github.com/microsoft/ivy and this is the one we recommend.

Clone the repository ensuring you have the submodule dependencies with the following:

git clone --recurse-submodules https://github.com/microsoft/ivy.git 
cd ivy
python build_submodules.py

This will take a long time, and expect warnings but not errors. The last couple of lines should look something like this, but it might change if you choose to install a newer version:

[100%] Built target test-openssl.t
cp -a include/*.h include/picotls ../../ivy/include/
cp -a *.a ../../ivy/lib/

Building and Installing IVy

Next, install IVy using this command, still in the ivy directory:

sudo python setup.py install

Testing Installation

You should now have a working installation of IVy. Check it using the following:

cd examples/ivy
ivy_check client_server.ivy

Your output should not produce errors, and it should resemble the following:

   The following properties are assumed initially:
       client_server.ivy: line 6: (no name)

   The following action implementations are present:
       client_server.ivy: line 9: implementation of connect
       client_server.ivy: line 17: implementation of disconnect
       client_server.ivy: line 25: implementation of error

   The following program assertions are treated as assumptions:
       in action disconnect when called from the environment:
           client_server.ivy: line 20: assumption
       in action connect when called from the environment:
           client_server.ivy: line 12: assumption
       in action error when called from the environment:
           client_server.ivy: line 29: assumption

OK

Prism API Notes

The following notes are an unofficial documentation for some of the functionality of the PRISM API (in Java). At the time of the creation of this document, there is no known source for official PRISM API documentation.

Let x and other single letters always represent a user-named variable.

Initialization

Import a few things:

// from PRISM
import prism.Prism; // main PRISM things
import prism.PrismDevNullLog; // Logging
import prism.PrismLog; // Logging
import prism.PrismPrintStreamLog; // Logging
import prism.PrismException; // Exception handling

// from PRISM's parser
import parser.Values; // Parsing state variable values
import parser.ast.Expression; // Handling CSL properties
import parser.ast.ModulesFile; // Importing the model

Create a log called mainLog for PRISM to use:

PrismLog mainLog = new PrismDevNullLog();

Initialize a PRISM simulation engine, where mainLog is of type PrismLog, noting the use of “s” in “initialise:

Prism prism = new Prism(mainLog);
prism.initialise();

Parse a model from a file, then load the model for checking:

ModulesFile modulesFile = prism.parseModelFile(new File("model.sm"));
prism.loadPRISMModel(modulesFile);

Load a model into a simulator engine:

prism.loadModelIntoSimulator();
SimulatorEngine sim = prism.getSimulator();

Let sim be the SimulatorEngine we created at the previous step.

Initialize a new path, noting the use of “s” in “initialise”.

sim.createNewPath();
sim.initialisePath(null);

Simulating

Let sim be the SimulatorEngine we created at initialization.

The following functions can be called from sim to simulate the model.

Transitions and Probabilities

All of these functions can be found in the PRISM source code. See prism/SimulatorEngine.java for details.

The following returns an int value representing the total number of transitions available at the current simulator state.

sim.getNumTransitions()

Available transitions are assigned and can be located using a numerical index. This index changes at each state. Transition names are stored in PRISM (surrounded by square brackets), so you can use the transition’s name to find the index.

This task relies on this function to get the transition’s name given its index i. It returns a String with the transition’s name in square brackets.

sim.getTransitionActionString(i)

The following loop can help you find the index of the transition given the transition’s name. The value index is the index of the desired transition, and t_name is the transition’s name stored in a String.

int index = 0;
for (int i = 0; i < sim.getNumTransitions(); i++) {
    String s1 = String.format("[%s]", t_name);
    String s2 = sim.getTransitionActionString(i);
    if (s1.equalsIgnoreCase(s2)) {
        index = i;
        break;
    }
}

Of course, transitions also have associated probabilities (for a DTMC) or rates (for a CTMC). The following function returns a double with the probability(DTMC) or the rate (CTMC), where i is the transition index.

sim.getTransitionProbability(i)

It is desirable to find the probability of a transition in a CTMC. From Introduction to the Numerical Solution to Markov Chains page 20:

For an ergodic CTMC the one-step transition probabilities of its EMC, denoted by $s_{ij}$ […] are given by

$$ s_{ij} = \frac{q_{ij}}{\sum_{j\neq i}q_{ij}}, j \neq i $$

$$ s_{ij} = 0, j = i $$

That is, the probability of transition i equals the rate of transition i divided by the sum of all other outgoing transition rates from the current state.

This calculation is implemented using the following loops. The loops remain separate because while the loop indices are identical, the second loop breaks when it finds the index of the state. Some clever manipulation can resolve this, but at the expense of the clarity desired in this document.

// Get the total rate by accumulating all outgoing rates
for (int idx=0; idx < sim.getNumTransitions(); idx++) {
    totalRate += sim.getTransitionProbability(idx);
} 

// Get the index of the transition of interest, as before
for (int idx=0; idx < sim.getNumTransitions(); idx++) {
    String s1 = String.format("[%s]",tr_st[tdx]);
    String s2 = sim.getTransitionActionString(idx);
    if (s1.equalsIgnoreCase(s2)) {
        index = idx;
        break;
    }
}

// Get the rate of the transition of interest
double rate = sim.getTransitionProbability(index);

// Get the probability of the transition to fire
double transition_probability = rate / totalRate;

Once you have selected the transition you desire to fire, it is almost trivial to manually fire the transition, given its index i:

sim.manualTransition(i);

You may need to go back after firing a transition. You can backtrack to a given step i (starting your path at step 0), using this function:

sim.backtrackTo(i);

If you are keeping track of a rolling state index j as you walk along a path, you can call it this way to go back to your most recent state:

sim.backtrackTo(j-1);

States and Properties

The following function gets the current state (as a State object):

sim.getCurrentState()

To get the state variable values from the current state, use the following variable (not function):

sim.getCurrentState().varValues

This will return an Object array. The Object is often of type Integer or String. To get the value as an int, you can use the following to fill the integer array values with the variable values.

// Get the objects from the state variable values
Object[] varList = sim.getCurrentState().varValues;
// Initialize a new array to store the variables
int[] values = new int[varList.length];
// Loop through the variable list to convert to ints
for (int i = 0; i < varList.length; i++) {
    // Check if Object values is an Integer or a String
    if (templist_c[i] instanceof Integer) {
        values[i] = (Integer) varList[i];
    }
    else if (templist_c[i] instanceof String) {
        values[i] = Integer.parseInt((String) varList[i]);
    }
}

The indices of state variables do not change at differing states, like transition indices do. If you need to see the name of a state variable at index i, use the following, which returns a String of the variable name.

sim.getVariableName(i)

To parse a property from a string csl_str, the following sequence will create a target state expression target and get the first property it finds from the string. The string is a Boolean condition (such as x > 5)

Expression target = prism.parsePropertiesString(csl_str).getProperty(0);

To evaluate whether a current state satisfies the property, the following function evaluates the Boolean property in Expression target to true or false:

target.evaluateBoolean(sim.getCurrentState())

Of course, you can call it on any State object, so if you save a State s and check it later, it looks like this:

State s = sim.getCurrentState()
// many lines of doing interesting things
if (target.evaluateBoolean(s)) // do something

There are a number of additional evaluate functions, but they are not covered here. See prism/Expression.java for details in code comments.

Full Path and Termination

The full path can be accessed using the following:

sim.getPathFull()

The path can be exported using the following:

sim.getPathFull().exportToLog(
    new PrismPrintStreamLog(System.out), true, ",", null
);

Close PRISM down with the following:

prism.closeDown();