you can run the nifty interface to SPIN by typing: ~jones/bin/xspin. Or if you have ~jones/bin in our path, you can just type xspin. There are some promela models in ~jones/Test/. Have fun!
It appears that my license for JPF does not permit use by third parties. Which, I believe, means I can't release it to the class. So we'll learn SPIN, and cover the "inline C" parts of the new spin. I'll demo JPF in class and we can discuss it, but I can't just dump it into the open labs for free use.
[Promela Language Reference , SPIN docs root]
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);
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.
[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.
Don't forget that there's no class today! Class will meet Wednesday to watch the video. We'll meet Friday when I get back to discuss the discussion questions from the video worksheet.
As you know, I'll be at Super Computing in Phoenix part of next week. Here's the plan:
Monday: No class.
Wednesday: Watch first 1/2 of E. Dijkstra video and fill out worksheet. Be prepared to discuss how to do program verification, as described by Dijkjstra, using a model checker on Friday.
Friday: Discuss Dijkstra video and discuss last project.
The last project, project 6, will be due Tuesday 11/25 (which really means the 11/26 by 8am) which is the day before the break.
I will only have office hours from 10 to 1030 this morning. If you'd like to see me this afternoon, drop me an email at jones@cs.byu.edu
Mike.
[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.
[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.
I've updated the online gradebook on routeY. With the exception of homework, which I seem to have nuked. I'll rebuild those grades from records.
The midterm will be in class this Friday. It will be closed book and you may bring in upto 2 pages of notes. The midterm will cover everything up to and including symbolic CTL model checking with fairness (so that's temporal logic, Kripke structures, BDDs, and symbolic CTL model checking). There will be a combination of "work out a small problem" and essay type questions. We'll even do a review Wednesday in class.