[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.
I need to cancel my office hours from 3-4 this afternoon. I will still be reading email this afternoon and evening. If you have any questions, send me mail. Or, if you do MSN messenger (or something compatible) send me (jones@cs.byu.edu) your contact info and we can IM.
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
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.
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...
a;
a->false[style="dashed"];
a->true[style="solid"];
true;
false;
This works, because if you do not provide a label, the node will be labeled with the name it is declared with in the input file. However, nodes can have a label attribute which is not the same as the name they are defined with. This is what I needed to do. The name each node is declared with should be the unique table index and the label should be the var. So the above might become:
38[label=a];
38->0[style="dashed"];
38->1[style="solid"];
1;
0;
I don't know if anyone else will have the problem, but I wanted to pass it on just in case.
[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.
[Symbolic model checker] The class interface is pretty simple and builds on your Kripke to BDD translators. Due October 31.
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
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.
[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.
[a yacc file, the corresponding lex file] You will be especially interested in the "expr" rule.
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.
[schedule] the schedule has been updated so that... the BDD package is due next Wednesday (10/15), the Kripke to BDD translator is due the following wednesday (10/22) and the symbolic model checker is due the friday after that (10/31-Halloween!).
[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.
translating infix to postfix, eval using a stack
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.
BDD_of (oper *, bdd a, bdd b):bdd
x = least top variable of a and b
if (*,a,b) is in results table, return results(*,a,b)
if (a and b are terminals) then
{ return a pointer to (a * b)}
if (both bdds have x as roots) then
{ low = BDD_of (*, a|x0, b|x0)
high = BDD_of (*,a|x1, b|x1)
}
else
{ f = bdd with x as root
g = the other bdd
low = BDD_of (*, f|x0,g)
high = BDD_of (*,f|x1,g)
}
if (low = high) return (if random() is even then low else high
if ((x,low,high) is in the BDD table) return BDD(x,low,high)
new-bdd = (x,low,high) // this is not a constructor call!
insert (*, a, b, new-bdd) into result table.
add new-bdd to table.
return pointer to new-bdd;
BDD table: key = hash(var, low, high) data = (var,low,high,bdd*)
results table: key = hash(oper,bdd,bdd) data = (var,low,high)
Notes about the project:
1. The function BDD_of, written above, is essentially your BDD object constructor for a binary boolean expression. You also need to implement constructors for unary expressions and boolean expressions written as strings. The constructor for unary expressions is a modification of the constructor for binary expressions left for you to design.
2. The constructor for boolean expressions written as strings uses your parser and then a recursive sequence of BDD constructor calls. It’s a strange thing to call a constructor recursively inside a constructor. The potential problem is that you’ll loose the pointer to the new object you created inside a recursive call—unless you store a pointer to the new object in a global piece of persistent memory. In this project, you’ll store a pointer to the new object in the BDD table. I will call a clean_memory () function before exiting. A good idea would be to traverse your BDD table and call the destructor methods for each BDD object pointer in the table.
3. I will not modify any of your state. More precisely, when I call unique_table_index () I will not attempt to modify the state of your global hash table (which makes sense because I won’t know the name of your global hash table). Also, when I call top_variable (), I will not attempt to modify the string you give me.
4. This project builds on many concepts you learned in other classes. These concepts include hash tables, recursion, parsing, and dynamic programming. I don’t intend to cover parsing, hash tables and dynamic programming in enough detail for you to complete the project. I hope you either remember the topics from your earlier classes, or feel confident enough to relearn them out of an old text book or library book.
[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.
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.
In project 2, your hash and results tables are limited to 3096 entries
The project is due Tuesday the 14th
[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.
Convert the expression (a /\ b) \/ (a /\ c) to a BDD. Use the algorithm we are developing in class. Show your results and BDD tables. Will be moved back to Wednesday if we don't get through an example on friday.