CSE307
Spring 2007
Stony Brook 		Principles of Programming Languages
Annie Liu
Assignment 6 		Handout A6
Apr. 17, 2007
Due Apr. 26

Logic Programming --- Adding Power

This assignment has two goals: (1) adding powerful analysis for our state machines, and (2) practicing programming with logic.

We have seen that state machines are quite powerful, and a lot of things could go wrong with them. We have done simple semantics analysis, such as checking determinism, for our state machines, but more powerful analysis, for checking reachability and detecting cycles, was only suggested in extra credit work. If you have tried to do a more powerful analysis, you would find that it is not easy. We will now do this by programming with logic.

Adding powerful analysis

We will do the reachability check as in the extra credit suggestion (2) in Assignment 3, and the cycle detection as in the extra credit suggestion (2) in Assignment 4. The former checks whether the trap state is ever reachable from the start state following the transitions. The latter checks whether there is a cycle in the substate nesting relationship.

To prepare for these more powerful analyses, we need a simple, clean representation of the state machine model. Relations come to rescue. For the reachability check in Assignment 3, only the top-level machine is taken. The machine consists of states, labels, transitions, and a start state, so we represent them using the following respective relations: 

state(a_state)
label(a_label)
trans(source_state, input_label, target_state)
start(the_start_state)

For the cycle detection in Assignment 4, a hierarchical state machine is taken, but only the information about substate is needed, so we represent it using the following relation: 

substate(super_state, sub_state)

Your task for this part is to write a Python program that generates these relations from the state machine model. For example, for the example machine in Assignment 3, you should generate the following facts of the relations: 

state(1).
state(2).
label(a).
label(b).
label(c).
label(d).
trans(1,a,1).
trans(1,b,2).
trans(2,c,2).
trans(2,d,1).
start(1).
and, for the example machine in Assignment 4, you should generate the following facts in addition to the facts above: 
substate(2,21).
substate(2,22).
substate(2,23).
When run, your program should take two file names from command line, for input data and output relations, respectively, (1) read data from the input data file, and (2) write the relations discussed above in the output relation file. For simplicity, you may assume that the input data passes the static semantics checking, i.e., it can be the output data file from your previous assignments (however, if you think about it, your program, with little or no change, should be able to write out the relations regardless of whether the input data passes static semantic checking).

Programming with logic

For the reachability checking, you may first define a relation that captures all the (non-trap) states reachable, similarly as in the graph reachability example discussed in class. Then you may write a rule to conclude that we fall in the state trap if a (non-trap) state is reachable and there is a label such that there is no transition from that state on that label.

For cycle detection, you may first define a relation that captures whether a state is (transitively) nested inside another state, similarly as in the transitive closure example discussed in class. Then you may write a rule to conclude that there is a cycle if a state is (transitively) nested inside itself.

Your task for this part is to write rules to do the two analyses. Don't forget to use the table directive, otherwise your query might not terminate.

For execution, you may invoke xsb with the following command line for reachability checking, and a similar one for cycle detection. 

xsb -e "[myprogfile],myreachpred,writeln('reach trap'),fail;halt."
where myprogfile is the name of the file, without .P, that contains your program, and myreachpred is name of the predicate that you defined to test whether a trap state is reachable.

Extra credit suggestions

Here are some ideas. (1) Check determinism within a table, and across tables; you just need to add one rule for each. (2) Check that the trap state is never reachable in the entire hierarchical machine, not just the top-level machine; this needs to use more relations. (3) Implement the hierarchical state machine semantics using rules; this needs to use also lists. (4) Think of other interesting and/or useful things to check and/or to do, and do them; feel free to discuss with me.

Handins

Hand in everything electronically, using Blackboard, by 5pm on the due date. Your handin should include your README file, code, test data, and anything else you have to show your work.

Grading

This assignment will be graded based on 100 points, allocated in proportion to the estimated amount of work for each part. You may do this assignment in a team of two people; the two people will receive the same points. Exceptionally well thought-out and well written work will receive appropriate extra credit. Extra credit work will be graded based on the estimated amount of extra work.