[Promela Language Reference , SPIN docs root]
I've updated the online gradebook on routeY. With the exception of homework, which I seem to have nuked. I'll rebuild those grades from records.
The midterm will be in class this Friday. It will be closed book and you may bring in upto 2 pages of notes. The midterm will cover everything up to and including symbolic CTL model checking with fairness (so that's temporal logic, Kripke structures, BDDs, and symbolic CTL model checking). There will be a combination of "work out a small problem" and essay type questions. We'll even do a review Wednesday in class.
[big BDD [pdf]] That's a BDD constructed to represent part of the transition relation for a network of PCI devices. I don't know how many nodes are in this BDD, but the entire BDD computation included an intermediate BDD with more than 16 million nodes.
In addition to our text, you might peruse the following... [Catherine Dochy's BDD Guide, Slides by Armin Biere (most likely), starting at page 33, CAD of VLSI at the Technion by A. Kolodny, start about page 5]
What's the difference between a state, a state formula and a label? A state is a container for labels, a state formula is a predicate (ie, a function that returns true or false) on states and a label is an adjective that describes states. We'll go over this a little on Wednesday just to make sure its all clear.