Homework 3
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
/cse/classes/CMPE293/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
/cse/classes/CMPE293/hw3_examples
You can run the scripts by:
mocha -t < pete_hw3.sl
and similarly for the other examples.
The three examples provided should all pass the test, i.e., the
invariant holds.
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.
-
The file pete_hw3.sl, and the other *.sl files, are
script files, that contain calls to Mocha commands.
Note: the demarc.rm (and demarc.sl) example is
considerably more complex than the other two; you can use it to
stress-test your implementation.
Read these script files, and modify them as indicated there in order
to do invariant verification by backward reachability.
-
What you have done, in your homework, is to provide the implementation
for sl_checkinvback.
Test sl_checkinvback, and compare the execution time, maximum
BDD size, and number of iterations of the backwards and forwards
approaches for the examples provided.
Then, inject errors in the examples, modifying the .rm code
(that you must copy to your own directory), and see how forward and
backward exploration perform in presence of errors.
-
Submit: You must email me your implementation of
slLuca.c as an attachment. I will then compile it and test it
on various examples.
- IMPORTANT: Do not erase hw3_mocha after you are
done. I will most likely give another homework consisting in
implementing functions in Mocha, and it will be easier for you if you
keep this installation around till then.
Luca de Alfaro
luca@soe.ucsc.edu