December 04, 2003
Final Project due Friday 12/06
This will allow you to ajust any code mangled by the incorrect property automata I posted last week. Good luck!
December 03, 2003
A correct property automata
As you may have noticed, the property automata I posted last week is ok, but doesn't represent the negation of "Always P". I am not sure what it represents. Its almost "not always q". I negated the property one too many times and got something else. Here's a correct negation of of "Always P." The moral of this story is: be careful about properties and negations, because you might negate the property one too many times. If we need to extend the deadline, we will. We'll talk about it in class. more...November 25, 2003
Example Property automata
The following code creates an automata for the negation of "Always P" in a universe with atomic propositions P and Q.
more...November 24, 2003
Project 6 Due Wed 12/3
Note that project 6 is "simply" a matter of implementing the double DFS algorithm of figure 9.8 (page 130) using the state generation algorithm outlined on page 139.
November 21, 2003
Project 6 Description
[Project 6] I posted the description. Its alot like the CTL model checking project, but you get the negation of hte property as a buchi automata rather than as a string.
November 12, 2003
The new new version of project 5
[Syllabus for] I've updated this version and deleted the second version of the syllabus. Note that the correct version of the project has a timestamp in big red letteres.
November 11, 2003
Project 5 updated.
[Syllabus] There's a constructor that takes the state count for a new automata, and the "add_vertex" method returns the index of the vertex just added.
October 28, 2003
Sample CTL problems for microwave example
[microwave.txt] and here are a few properties from the book (page 38). (Also, I added EX and AX to the project description. I'd accidently left them off).
"heat AF start ~ | AG" which is not satisfied by the microwave. (changed 10/29 at 4pm)
"error heat & ~ AG" which is satisfied by the microwave.
"close EX" which is satisfied by the microwave.
"start ~ EG" which is satisfied by the microwave.
"heat EG" which is not.
October 27, 2003
New BDD package
The package was changed at 8am Thursday the 30th to fix a bug.
Two new methods have been added to the BDD package for use in the CTL model checker.
They are BDD(BDD*) which returns a primed version of the BDD inputted.
and bool topVarPrimed() which returns true or false about whether there are any primed variables in that particular BDD
This should be useful in implementing checkEX
October 22, 2003
Kripke->BDD due Friday (10/25) & What to turn in
The Kripke to BDD translator is due friday by midnight (which means monday morning at 8 if you need it).
You should turn in all files you need to make your translator work. If you have a file with main in it and a Make file, it would be helpful to turn those in too.
October 21, 2003
Graphviz nodes and labels
In your BDD packages, you may have noticed that graphviz didn't always make 2 nodes out of 2 different nodes with the same label. This happens when node B appears twice, but has different children for each appearance. Dan Delory has posted a fine explanaition of how to get around this...
more...October 20, 2003
Symbolic MC project revised and posted
[Symbolic model checker] The class interface is pretty simple and builds on your Kripke to BDD translators. Due October 31.
Working BDD
If you never got your BDD class to work properly and you want to risk using somebody elses here are some links.
If you download before 9:30am Thursday the 23rd you should redownload.
Two new methods have been added to the BDD package for use in the CTL model checker.
They are BDD(BDD*) which returns a primed version of the BDD inputted.
and bool topVarPrimed() which returns true or false about whether there are any primed variables int that particular BDD
October 17, 2003
Kripke to BDD class definition
I've created the class specificatin for the Kripke to BDD translator. Its about what you'd expect: a constructor with a Kripke object as a parameter and a bunch of methods that return BDD objects. See the syllabus for details.
October 15, 2003
b_var and b_const in bool_op enumeration
[syllabus] As you might guess, the b_var and b_const members of the bool_op enumeration don't belong in the bool_op enumeration. I've taken them out in the syllabus. You may take them out of your class implementation.
October 14, 2003
Sample yacc file
[a yacc file, the corresponding lex file] You will be especially interested in the "expr" rule.
October 10, 2003
No Parens in Postfix expresions
The postfix boolean expressions (which will be passed to your BDD constructor if you #define POSTFIX) will not contain parentheses. The expression will contain a space between variables and operators so you can use strtok to tokenize if you'd like.
October 08, 2003
GraphViz
[Graphviz homepage] Graphviz has been installed on the machines in room 1102 of the TMCB (that's the fruits lab with cherry.cs.byu.edu, apple.cs.byu.edu etc). To run graphviz, you would generate a text file describing the graph (see the documentation at the above site) then run dot on that file. If your text file was called "my_file.txt" then you might use "dot -Tps dot-file.dot > output.ps" to generate a postscript file called output.ps that contains your graph.
Brent's postfix wonderland
translating infix to postfix, eval using a stack
Project 2 implementation notes
Some notes about implementing the project which relate the bdd_of function (which we discussed in class) to the BDD constructors you will implement. Also some thoughts about recursively calling constructors inside constructors.
more...Postfix syntax
[Postfix example Expressions] You may assume that boolean expressions are given to you in postfix if you like. If you use postfix, be sure to #define POSTFIX in your header files so I know which version of a boolean expression to pass your constructor.
BDD class clarifications
Two things: first, two of the constructors are redundant. The constructor for (char *variable_name) and (char *boolexpr) have the same type. Fortunately, they have the same behavior since a variable name is a special class of boolean expression. Second, I will only call restrict on the root, or top, varible of a bdd. The project description has been updated.
October 06, 2003
Updates for Project 2
In project 2, your hash and results tables are limited to 3096 entries
The project is due Tuesday the 14th
Using Lex for your parser
[Yacc manual] You may use yacc to generate your abstract syntax tree in the BDD project. Yacc (Yet Another Compiler Compiler) is a tool for building a compiler from the grammatical rules that describe a programming language. The resulting compiler will make calls into a C (or C++) program so you can use Yacc to build an abstract syntax tree object or to build a sequence of BDD constructor calls. If there is sufficient interest, I'll post some Yacc input file examples.
September 29, 2003
valgrind output
For full credit, valgrind should report 0 errors, 0 bytes definitely lost and 0 bytes in use at exit. If you compile your program with -ggdb valgring will give you line numbers and function names for memory leak locations.
more...valgrind and the STL
[valgrind faq (see Q14)] If you are using the STL and get 'still reachable' memory at the end of your program, even though you shouldn't, then you are probably suffering from memory pooling. Memory pooliing is a feature, not a bug, in the STL implementations. For a good discussion see the faq entry above. To eliminate the reachable memory, force the compiler to use malloc and free. You can do this by setting the GLIBCPP_FORCE_NEW environment variable by doing export GLIBCPP_FORCE_NEW=1 (or similar depending on your shell).
I will have GLIBCPP_FORCE_NEW set in my environment when I compile and check your stuff. Thanks to Micah Lewis for asking the question.
September 25, 2003
How to use valgrind
Recall that CS 586 projects must not have memory leaks to get full credit. I've install a memory debugger in /users/faculty/jones/bin. Its called valgrind. To use it, run
valgrind --leak-check=yes --leak-resolution=high < program and args >
September 24, 2003
Final changes to project one (due Monday 9/29)
Project 1 has been modified to reflect the changes we made in class. Whew. Its due by midnight Monday, which really means Tueday morning around 8am. Good luck and keep asking questions about the project as they come up...
September 22, 2003
Project 1 public methods modified
Added a constructor that takes the name of a file containing a Kripke structure, deleted the read_kripke method and refined the definition of the next_states and propositions interfaces.
[Project 1]
September 19, 2003
Added "read_kripke" method to Proj. 1
[Project 1 from the syllabus] We need a public method for reading in a Kripke from a file. The function takes a filename, and creates a Kripke structure from the file. I’ll check your projects by writing a wrapper that uses your public methods to read and analyze your Kripke structure. That method will be:
void read_kripke (file *filename);
I've updated the syllabus to reflect the change
September 17, 2003
Example Kripke data files
Simple Kripke
Loop Kripke
Boring Kripke
September 16, 2003
Project 1 Clarification
The format of files containing Kripke structures has been clarified. The clarification is "there may be one or more lines beginning with “Transitions” that identify transitions. Similarly, there may be one or more lines beginning with “Label.” Each “Label” line contains one state and a list of atomic proposition (AP) labels for that state. No white space in strings used as APs, no commas between transition pairs an white space is ok everywhere else."
[Project 1 Description (from syllabus)]