CS 586

Check grades!

Its a good idea to check your grades on blackboard soon. Mail Peter (nvrnvrby@hotmail.com) with discrepancies.

Study list for Final

I've posted a plain text and word copy of the study list for the final in the lecture notes directory (there's a link at the bottom left of the homepage). They are "CS 586 Objectives.doc" and "objectives.txt". The final will be three hours in the classroom on Wednesday from 230-530. I'll be out of town, but someone from the lab will come to proctor the exam.

on line evaluation for 1 hwk credit

Don't forget that you can fill out the online evaluatin of this class (listed as a 501R) for 1 extra homework credit. You must allow your name to be shown to get the credit. Not filling out the form and making your name available will not hurt your homework score.

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!

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.

// The true encoding of ~ Always P as an automata. 
Buchi *b = new Buchi (7); 

int start = add_vertex(); 
int p = b->add_vertex(); 
int pq = b->add_vertex(); 
int q_accept = b->add_vertex(); 
int e_accept= b->add_vertex(); 
int p_accept =b->add_vertex(); 
int pq_accept=b->add_vertex(); 

b->mark_accept (p_accept); 
b->mark_accept(pq_accept); 
b->mark_accept (e_accept); 
b->mark_accept(q_accept); 

b->mark_start (start);

char labels[4][4]; 

strcpy (labels[0], "p"); 
strcpy (labels[1], "q"); 
strcpy (labels[2], ""); 

b->add_edge (start, pq, labels); 
b->add_edge (pq_accept, pq_accept, labels); 
b->add_edge (p_accept, pq_accept, labels); 
b->add_edge (q_accept, pq_accept, labels); 
b->add_edge (e_accept, pq_accept, labels); 
b->add_edge (pq, pq, labels); 
b->add_edge (p, pq, labels); 

strcpy (labels[1], "");  // just have p as a label. 

b->add_edge(start, p, labels); 
b->add_edge(p_accept, p_accept, labels); 
b->add_edge(pq_accept, p_accept, labels); 
b->add_edge(q_accept, p_accept, labels); 
b->add_edge(e_accept, p_accept, labels); 
b->add_edge(p, p, labels); 
b->add_edge(pq,p,labels); 

strcpy (labels[0], "q"); // just q as a label. 

b->add_edge (start, q_accept, labels); 
b->add_edge(q_accept, q_accept, labels); 
b->add_edge(p_accept, q_accept, labels); 
b->add_edge(pq_accept, q_accept, labels); 
b->add_edge(e_accept, q_accept, labels); 
b->add_edge(p, q_accept, labels); 
b->add_edge(pq, q_accept, labels); 

strcpy (labels[0], ""); 

b->add_edge (start, e_accept, labels); 
b->add_edge(e_accept, e_accept, labels); 
b->add_edge(p_accept, e_accept, labels); 
b->add_edge(pq_accept, e_accept, labels); 
b->add_edge(q_accept, e_accept, labels); 
b->add_edge(pq, e_accept, labels); 
b->add_edge(p, e_accept, labels); 

Find error in Mutex 1 using SPIN

Create a model of Mutex 1 (from the Mutex handout) in SPIN. Use that model to show that it is possible to have more than 1 process in the critical section at the same time. Strategically add printfs to your code so that the MSC contains meaningful information. Mail me (jones@cs.byu.edu) the msc.ps from a guided simulation that shows the error. Due last day of class.