Goal:
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.
Although this text is no longer available through the university libarary
services, enterprising students may be able to locate this document.
Relevant material begins on page 183.
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
in CTL.
You should use the variables listed in typewriter font
as your primitive propositions.
Start by drawing an appropriate computational tree, and only
then capturing that tree with CTL.
The computational tree will count as part of the grading.
started
holds, but
ready
does not hold.
request
(of some resource) occurs,
then it will eventually be
acknowledged
.
deadlocked
.
enabled
.
restart
state.
doors == closed
,
floor == 3
,
switchClosed
becomes true,
valveOpen
is never true.
toggle
alternates between true and false on successive states.
For those interested in bonus points, consider the traffic light specification. 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 look at a mutual exclusion example or the example from the class slides
Note: NuSMV 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.