CS 586

Example Property automata

The following code creates an automata for the negation of "Always P" in a universe with atomic propositions P and Q.

This automata is designed to check "always p" in a Buchi automata with APs "p" and "q". This automata encodes the negation of "always p".

 

Buchi *b = new Buchi (5); 

int start = add_vertex(); 

int p_accept = b->add_vertex(); 

int pq_accept = b->add_vertex(); 

int q_dead = b->add_vertex(); 

int e_dead = b->add_vertex(); 

b->mark_accept (p_accept); 

b->mark_accept(pq_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_accept, labels); 

b->add_edge (pq_accept, pq_accept, labels); 

b->add_edge (p_accept, pq_accept, labels); 

b->add_edge (q_dead, pq_accept, labels); 

b->add_edge (e_dead, pq_accept, labels); 

strcpy (labels[1], ""); 

b->add_edge(start, p_accept, labels); 

b->add_edge(p_accept, p_accept, labels); 

b->add_edge(pq_accept, p_accept, labels); 

b->add_edge(q_dead, p_accept, labels); 

b->add_edge(e_dead, p_accept, labels); 

strcpy (labels[0], "q");

b->add_edge (start, q_dead, labels); 

b->add_edge(q_dead, q_dead, labels); 

b->add_edge(p_accept, start, labels); 

b->add_edge(pq_accept, start, labels); 

b->add_edge(e_dead, q_dead, labels); 

strcpy (labels[0], ""); 

b->add_edge (start, e_dead, labels); 

b->add_edge(e_dead, e_dead, labels); 

b->add_edge(p_accept, e_dead, labels); 

b->add_edge(pq_accept, e_dead, labels); 

b->add_edge(q_dead, e_dead, labels);