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);
Posted by jones at December 3, 2003 09:17 AM