CSE308 - Tutorial 7 - Bounded Model Checking

Setup
Evaluation
Implement the BMC encoding for G p properties
Construct the lasso-shaped counter-example
BMC for FG p properties
BMC for arbitrary LTL properties
- A buggy buffer
Submit your work

Setup

You should already have all the dependencies on your system.

In case, run in the terminal the command pysmt-install --check and check you have a SAT (or SMT solver) installed. Your output will be something like:

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)

All is ok as long as you have any of the following installed (True value in the column): msat, cvc4, z3,yices,picosat.

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

Evaluation

You will receive a maximum 20 points, subdivided as follows:

Bmc for G p: 4 points.
Counter-example construction: 2 points.
Bmc for FG p: 4 points.
Generic BMC (no syntactic restriction): 8 points.
Fix for buffer: 2 points.

Deadline.

The deadline for submitting the exercise to obtain a full grade is Thursday May 29th 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/td7.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.

Your task is to implement the function bmc_Gp:

def bmc_Gp(ts : SymbolicTS, p : BoolFormula, k : int) -> Tuple[bool, Optional[KL_lasso]]

The function takes as input a symbolic transition system (ts), the property p to check (i.e., the p from G p), and the length k of the path to check. The function returns a tuple: the first element is False if the function finds a counterexample, and in that case returns a lasso-shaped path as second argument (**for now, ignore the second argument and always return None). If bmc cannot determine if there is a violation, the function returns (True,None).

Your task is to construct the bounded model checking encoding for finding a counterexample to the formula G p.

Some hints:

We already provided you with a function in the symbolic transition system class called retime. retime(f, i, j) takes as input a formula that only contains variables from the set V and V' (V_next in the code), an integer i, and an optional integer j, 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, if j is not provided, and with index j otherwise. 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 a_at_2 & a_at_3. Similarly, ts.retime(And(a, a_next), 2,1) would give you the formula a_at_2 & a_at_1.

Use this function to create the formulas of your BMC encoding.
To check if a formula is satisfiable, you can use different APIs from PySMT.
- The easiest one is is_sat(formula) that returns true if the formula is satisfiable. You can call get_model(formula) to get a satisfying assignment in case.
- You can directly use the Solver class as follows:
```
solver = Solver(logic=QF_BOOL)
solver.add_assertion(encoding)
res = solver.solve()
model = solver.get_model()
```
  An important consideration is that calling get_model on a solver object will not try to find again a satisfying assignment (i.e., calling the CDCL algorithm) but will reuse the previous result (solver carries a state while just calling the function is_sat does not).
You can test your implementation in the function test_gp in the td7_script.py file.

Construct the lasso-shaped counter-example

Extend bmc_Gp to construct a lasso-shaped counter-example from the satisfying assignment found by the SAT solver.

We represent a (k-l)-lasso with the following type:

KL_lasso : TypeAlias = Tuple[List[Mapping[BoolFormula, bool]], int]

where:

The first element of the tuple List[Mapping[BoolFormula, bool]] represent a path of length k: each element of the list is a state in the path, and each state is just a mapping from variables to truth assignments. So, the list [{a : True, b: False}, {a : True, b: True}] represents a path with 2 states, the first state where a is True and b is False and the second state where both a and b are True.
The second element of the tuple is an integer representing l, the index where the loop of the lasso start.

You may find the function get_py_value of the Model object returned from get_model useful. The function returns the value (e.g., true or false) assigned to a variable in the encoding. Model is defined in pysmt.solvers.solver and useful, or not:

There are no explicit test cases for this function, but you can print your model in the examples in td7_script.py.

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 : SymbolicTS, p : BoolFormula, k : int) -> Tuple[bool, Optional[KL_lasso]]

Also here, look for the function `test_fgp in td7_script.py.

BMC for arbitrary LTL properties

Implement the generic BMC encoding for checking a LTL formula already in Negation Normal Form:

def bmc(ts : SymbolicTS, f : LtlFormula, k : int) -> Tuple[bool, Optional[KL_lasso]

Here assume that f is already the negation of the formula you want to check (i.e., the input to \(\Gamma\) in the BMC encoding formula you have on the slides).

Use the test cases for G p and FG p to try your implementation first.

A buggy buffer

Then, take a look at the file buffer.smv.

The SMV model specifies a bounded-size buffer that:

has at most 3 elements (3 bits).
at every step (cycle), the input operation op is either IDLE or INSERT
IDLE means that the buffer state does not change (elements and current size)
INSERT means we insert the input element e in the first position of the buffer (e0), and we shift all the others (e0 to e1, e1 to e2). The current value of e2 is lost.
the buffer provides as output the “older” element inserted in the buffer (or 0s if there are no elements).

You will have to perform two tasks: 1. Use NuSMV to find the bugs in the buffer and fix the SMV model. 2. Test your BMC implementation on the (still buggy) model (it should return reasonable counterexamples to the LTL properties in the SMV model).

For task 1:

Try to verify the LTL properties (from P1 to P4, in order) in the files using the bounded model checking implementation of NuSMV (you can use the app.cmd file for commands.
All the properties should not hold within a reasonable bound (at most 20). Start with the first property, understand what is wrong in the buffer implementation and fix the model.

For task 2:

you can load the buggy model as a symbolic transition system in your ccode as:
```
buffer_ts = get_ts("buffer.vmt")
```
You find buffer.vmt in the src folder.
You will have to write the LTLSPEC properties in Negation Normal Form and then parse it.
```
parser = LTLParser(get_env())
f = parser.parse("G p")
```
As you need to negate the LTLSPEC formula, the conversion in NNF may be tedious to do manually. You can implement it easily and let the machine do the job for you.

Submit your work

You’ll have to upload the following files

Upload form is only available when connected