15-398 Assignments,
Exams and Solutions
Assignment |
Date Assigned |
Date Due |
Link to Solutions |
Homework 1:Parser
Readme |
|
09/23/01 |
|
Homework 2
(ps)
(pdf)
|
09/19/02 |
10/07/02 |
|
Homework 3
(ps)
(pdf)
|
10/10/02 |
10/29/02 |
|
Homework 4
(ps)
(pdf)
|
11/07/02 |
11/22/02 |
|
Homework 5
|
11/07/02 |
12/03/02 |
|
Final Project (optional)
(ps)
(pdf)
|
11/19/02 |
12/05/02 |
|
Typed homework is not
required, but we don't discourage it. It is your responsibility to make
sure your handin is legible. If you want to use LaTeX, use the Sample
LaTeX Template. The postscript version of this template is Postscript
Sample. You are also welcome to use WORD.
-
I have graded the mid-term and posted the results on the same page where the homework results are. I also added the text of the exam and the solution (the smv runs) for them
(tgz)
(zip)
.
-
Check your grades online. Click here
to login.
You should have received a password in your
email. If you did not, if you want to change your password, or
if you forgot your password please email flerda+15-398@cs.cmu.edu.
SPIN and XSPIN
I have installed SPIN and XSPIN in:
/afs/andrew/usr/flerda/classes/15-398/bin
SMV and NuSMV
I have installed SMV and NuSMV in:
/afs/andrew/usr/flerda/classes/15-398/bin
If you add that directory to your path it should
run.
In it there are:
- CMU SMV (command: smv)
- NuSMV 1.1 (command: NuSMV, xNuSMV)
- NuSMV 2.1 (command: NuSMV-2.1)
You are encouraged to try them (I run them on a few
examples on a machine of the linux.andrew.cmu.edu cluster
and they seems to work) and let me know if anything does
not run properly.
Here are some links where you can find more information and
download the tools themselves.
SMV
Official Website:
http://www-2.cs.cmu.edu/~modelcheck/smv.html
Here you can find the source code for UNIX and an
executable for Windows NT. I will soon test the NT version
to see if it works correctly on other versions of Windows.
It also contains links to binaries for some UNIX including
Linux.
NuSMV
Official Website:
http://nusmv.itc.it/
There are binaries and source distribution for NuSMV as
well as documentation.