First, grab the mocha-hw.tgz tarball, and expand it somewhere where you have at least 60 MB of space. If this is a problem, let me know.
Your code goes into mocha-homework/src/sl/slLuca.c (yes, I know, I know, the name is not serious, but...).
If you look at the source code, sl_checkinvback is implemented in terms of a command SlCheckInvBackCmd, which in turn is implemented in terms of a call to computeBackReach. There is where you have to add your code. A stub for computeBackReach is already provided.
I advise that you look at ComputeReach in order to understand how to write computeBackReach.
There are comments all over the file; read ComputeReach, read the stub of computeBackReach, and search the file for 'CMPE278'. That should be enough information.
Note: this version of mocha may not work from the GUI; you may have to start it with mocha -t.
In order to test your homework, grab the file hw_test_input.tgz and expand it. The files ending with .rm are reactive module files, the files ending with .sl are script files used for testing. If you do (after you put the mocha you compiled in the path):
mocha -t < invariant_passes.sl
then the invariant should pass after 132 iterations, both for forward (sl_checkinv) and backward (sl_checkinvback) search. On the other hand, if you do
mocha -t < invariant_fails.sl
then the invariant should fail at iteration 36.
If you are wondering, the last v/s in the tcl commands indicates verbose or silent.
You are of course welcome to use the course bulletin board to share information and insight about the workings of the various function calls, information about mocha, etc etc. However, write your code by yourself.