Backward Reachability Homework
The assignment
In this homework, you have to implement the function
computeBackReach.
Try to write it in an efficient way. The best hint I can give is to
study the implementation of computeReach, and write
something similar to it.
If mode=1, which indicates "verbose" operation, your
implementation should print, at each iteration, the number of the
iteration, and the size of the BDD representing the states that can reach
the violation of the invariant. Look at computeReach for how
to do this.
Setup details:
To set up for the homework, do the following on a Linux machine.
- Copy the content of the directory
/projects/bubble/hw3_mocha to your own directory tree.
You need to have some 40MB of space for this; let me know if this is a
problem. Go to the hw3_mocha directory.
- If you are using bash, edit the file bash_setup
to reflect the location of the current directory, then do
source bash_setup
If you are using csh or tcsh, then do
the same for csh_setup
- Your code should go in the file
hw3_mocha/src/sl/slLuca.c
You will see a placeholder at computeBackReach.
Search also for the string CMPE293 for related information.
- You can find the documentation on arrays, BDDs, etc, in the
directory hw3_mocha/mocha_doc
- Read the implementation of computeReach carefully (it was
explained in class). What you have to do is fairly similar.
- Prepare for compilation by doing, in directory hw3_mocha:
rm Makefile configure.status configure.cache
./configure
make
- I prepared some examples so that you can test your
implementation. Go to the directory
hw3_mocha/examples
You can run the scripts by:
mocha -t < inv_passes.sl
mocha -t < inv_fails.sl
In the first example, the invariant should pass (both the forward, and
the backward check).
In the second example, the invariant should fail (both the forward, and
the backward check).
Note that for some arcane reasons, the invariant is specified as the
set of reachable states of a "specification" module.
This is a detail you don't need to be concerned about.
-
Submit: You must email me your implementation of
slLuca.c as an attachment, together with the output of the
scripts inv_passes.sl and inv_fails.sl.
I will then compile your implementation and test it on various examples.
Luca de Alfaro
luca@soe.ucsc.edu