Temporal Logic / Specification Patterns.
Note: You might find the Huth and Ryan text
useful for some of these exercises:
M.R.A. Huth and M.D. Ryan. Logic in Computer Science. Second Edition. Cambridge University Press, 2004, ISBN 978-0-521-54310-1. Direct Safari Link General Safari Link (off campus)
The non-bonus part of this assignment is a paper/pencil exercise only.
Use the KSU slides covered in the lecture as
a resource to help you formulate the following
You should use the variables listed in
as your primitive propositions.
readydoes not hold.
request(of some resource) occurs, then it will eventually be
enabledinfinitely often on every computation path.
direction == up,
floor == 2, and
valueOpenis never true.
pis not true until
togglevaries between true and false on successive states.
For those interested in bonus points, consider the traffic light specification shown in class. Expand the SMV to model a more complex intersection. For example, you could consider an intersection with a left-turn arrow. Write SPEC clauses to capture the following property:
As an additional example, you might find the mutual exclusion example of interest.
Note: NuSMV requires a slightly cleaner syntax than SMV. In particular, NuSMV does not recognize "1" as a boolean constant; use "TRUE" instead. NuSMV also has deprecated processes; I'd be happy to have someone figure out the appropriate replacement.
Bonus credit (up to 3 points) only available if you demonstrate that you had SMV running.