Tasks you will need to do before starting:
Resources you will need:
Do exercise 4.3 in back of chapter 4.
Turn-in: Turn in lts.
Do exercise 4.4 in back of chapter 4.
Turn-in: Java source code plus jar file that I can double-click. Might want a README file that says what I can expect to happen. Don't need GUI interface - can use terminal I/O if you want. (Althought GUI interface might be easier in Java than terminal I/O!)
Do exercise 6.1 in back of chapter 6. Hint: parameterize your maze to allow starting in any square as follows.
BTW: I think this is a cute use of deadlock analysis to actually solve a search problem. You are relying on LTSA to find the shortest path to a deadlock. Then set the search problem up to make the deadlock state the goal state.
Turn-in: lts code.
Look at slide 12 in .../cis650/10W-slides/ch4ext.ppt. This will give you your starting model for this problem. Instead of taking the oracle route, as this chapter does, I'd like to see if we can use fluents and asserts to define a logical property. You will need to review material from my ch14ext.ppt slides, as well as chapter 14. In particular, you should study section 14.2.1. The example used in this section is quite similar to our interference problem. There is a critical section in the TURNSTILE process. And we would like to assert that east and west are not in that section at the same time. Your task is to define the fluents that describe the critical section, and then define an assert that uses those fluents similar to what is seen in the MUTEX example.
Once you have this set up, you can do a CHECK of LTL properties and you should get a trace to a violation. Pretty cool. We have replaced the need for the oracle test code with a more elegant logical property.
As a final note, think about how to use concepts from chapter 14 when defining the Deschutes front door on Wednesday in class.