CSE308 - Tutorial 6 - Bounded Model Checking

Setup

Setting up the tutorial.

Download and extract the files of the tutorial CSE308-TD6-1-handin.zip. You’ll have a folder called CSE308-TD6-1-handin.

You need to install the python package contained in the requirements.txt file with pip

$ pip install -r requirements.txt

In case you have conflicts installing the packages versions, you can try with a python environment (or with anaconda) (see tutorial 2 if you need to install pip on the lab machines).

You need to install a SAT solver to be able to check the satisfiability of the BMC encodings. We will install the z3 solver (which does more than SAT in practice, but we don’t care):

$ pysmt-install --z3

You can check things have been sucesfull with:

$ pysmt-install --check

It will show a list of installed solvers, for example:

Installed Solvers:
  msat      True (5.6.1)
  cvc4      False (None)              Not in Python's path!
  z3        True (4.8.7)
  yices     False (None)              Not in Python's path!
  btor      False (None)              Not in Python's path!
  picosat   False (None)              Not in Python's path!
  bdd       True (2.0.3)

Solvers: z3, msat, bdd
Quantifier Eliminators: z3, msat_fm, msat_lw, bdd, shannon, selfsub
UNSAT-Cores: z3, msat
Interpolators: msat

Make sure the line for z3 tells True (we don’t care about the other solvers now).

Warning: we had issue installing the solvers with Python 3.12

In that case, what seems to work is to install the missing dependencies, in particular:

$ pip install setuptools

Warning: some of you got a bug related to ssl certificates when downloading z3. The symptom for the issue is an exception like this one when trying to install z3:

...
Error while trying to get the archive using link 'https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-osx-10.14.6.zip' (trial 1/3)
...
ssl.SSLCertVerificationError: [SSL: CERTIFICATE_VERIFY_FAILED] certificate verify failed: unable to get local issuer certificate (_ssl.c:1000)

We can cirumvent the issue with the following commands:

$ curl -LO --remote-name 'https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-osx-10.14.6.zip'
$ mv z3-4.8.7-x64-osx-10.14.6.zip ~/.smt_solvers/z3

Instead of curl you can use wget, or just downloading the file yourself and then moving it in the ~/.smt_solvers/z3 folder.

At this point you can try to install z3 again:

$ pysmt-install z3

Evaluation.

You will receive 100 points, distributed for each function you have to implement:

• BMC for G p, no loopback: 30

• BMC for G p, loopback: 20

• Counter-example construction: 20

• BMC for F p: 15

• BMC for FG p: 15

You have some test cases available, but passing the test cases does not mean your solution is correct. I will mainly evaluate if your code implements the algorithms we saw in class.

Deadline.

The deadline for submitting the exercise to obtain a full grade is Thursday 23 at 23:59. You can submit your work after that deadline but you will receive only 50% of the total grade.

Implement the BMC encoding for G p properties

Here and in the rest of the tutorial you will work in the file mc308/bmc.py (and use the test cases in mc308/tests/test_bmc.py). In the first exercise you will implement the Bounded Model Checking algorithm for checking properties of the form G p, where p is a propositional logic formula.

We provided you with the class SymbolicTS that represents symbolic transition systems (always in bmc.py). You can create a transition system as follows:

V = [Symbol('a'), Symbol('b'))
a,b = V
a_next = get_next(a)
b_next = get_next(b)

ts = SymbolicTS(V, And([Not(a),Not(b)]), And(Iff(a_next,a)))

We represent Boolean formulas using the PySMT library. You can take a quick look at Boolean Logic with PySMT to understand how to declare Boolean variables, how to build a formula using the logical operators, checking the satisfiablity of a formula, and processing the model in case the formula is satisfiable.

Your task is to implement the function bmc_Gp_no_loop defined in the file bmc.py:

def bmc_Gp_no_loop(ts, p, k):
    """
    Find a violations to the property G p exploring k steps

    Here, don't care about loopback (find a finite-path)

    Here, you have to create the BMC formula that finds a violation to
    properties of the form G p.
    Create the BMC formula in the encoding variable.

    """

    encoding = None

    if encoding is None:
        raise NotImplementedError()

    return check_formula(ts, "G " + p.serialize(), encoding, k)

The function takes as input a symbolic transition system (ts), the property p to check (i.e., the p in G p), and the length of your encoding, k.

The function already adds the code that check if your bmc encoding is satisfiable or not and in case tries to print a counter-example (the counter-example construction is still not complete, and you will implement this next). So, your taks is to provide to the check_formula function the bounded model checking encoding for finding violations to the formula.

We already provided you with a function in the symbolic transition system class called retime. retime(f, i) takes as input a formula that only contains variables from the set V and V' (V_next in the code) and and integer i, and produces a formula where all the variables V are replaced with variables with index i, and all the variables V_next are replaced with variables with index i+1. For example:

ts.retime(And(a, a_next), 2)

where a is the Symbol variable with name a (so, the formula is really a & a_next) will return the formula (represented ad PySMT object) corresponding to a_at_2 & a_at_3. Use this function to create the formulas of your BMC encoding.

You can run the bmc algorithm and test your solution with the file mc308/tests/test_bmc.py and the function test_gp_no_loop in the TestBMC class:

pytest mc308/tests/test_bmc.py::TestBMC::test_gp_no_loop

If may need to install pytest on the lab machine, just type pip install pytest.

As usual, you can add more test cases to see if your solution makes sense.

Infinite counterexamples for G p

Your task is to implement the function bmc_Gp defined in the file bmc.py:

def bmc_Gp(ts, p, k)
    ...

to only find infinite paths as violation to the LTL property.

You can run your function with:

pytest mc308/tests/test_bmc.py::TestBMC::test_gp

Construct the counter-example

Implement the function bmc_get_cex defined in the file bmc.py to extract a counter-example path from the model found by the SAT solver:

def bmc_get_cex(ts, encoding, k):
    ...

This function creates a counter-example (a path in the transition system) from the model found by the SAT solver.

We expect the counter example to be a list of states, and each state is a list of assignments to the variables of the system. So, each element of the counter-example list is a list of assignments to variables of the transition systems. We represent an assignment as a tuple (e.g., (a,True), where the variable a is assigned to the boolean value True). Valid assignments either True or False.

So, for example, a counter-example with 3 states would look like:

[ [(a,True), (b, False)], [(a,True), (b, True)] [(a,True), (b, False)] ]

In the function you’ll also need to check if there is a loop from the last state k to one of the previous states. The function should return the index of the loop, if one exist, or -1 otherwise.

In the end, the function returns a tuple containing the counterexample list and the integer number for the loopback.

There are no explicit test cases for this function, but you can see the counter-example that your function computes adding the -s switch to the test cases, e.g.:

pytest mc308/tests/test_bmc.py::TestBMC::test_gp -s

BMC for F p properties

Implement the function bmc_Fp defined in the file bmc.py to find violations to LTL properties of the form F p:

def bmc_Fp(ts, p, k)
    ...

You can run your function with:

pytest mc308/tests/test_bmc.py::TestBMC::test_fp

BMC for FG p properties

Implement the function bmc_FGp defined in the file bmc.py to find violations to LTL properties of the form FG p:

def bmc_FGp(ts, p, k)
    ...

You can run your function with:

pytest mc308/tests/test_bmc.py::TestBMC::test_fgp

Upload your solution

You will upload a single file, bmc.py containing all your code.