Dear students,

I have posted (partial) solutions to the exercises to the Web page.

There have been several difficulties, partially apparently caused by too
undetailed descriptions, partially because some of you started too late to get
used to Spin and elaborate the exercises (however, to say it explicitly: some
of you did *very* well).

I hope, the additional explanations will clarify things to everyone. Please
study them on your own and ask me, if you have questions. I will not repeat
the explanations in class unless there is some concrete question.

Best regards, WS

1. Dining Philosophers
----------------------
The file "philosopher.txt" contains a sample solution to the exercise
based on a shared variable model (which is the easiest one for this problem).
The solution is not the shortest one, but it should be simple to understand.

The "atomic" statements used in the model are to ensure that between
chosing a fork and taking it (and setting the status variable waitingL/R),
there is no way for another philosopher to interfere.

Unfortunately, the description of the property to be checked was ambiguous. It
should have read "... it is never the case that every philosopher is waiting
for a fork *that is not available*" (for the consequence of this, see below).

This property can be formalized as

[]!(w0 && w1 && w2 && w3 && w4 && f0 && f1 && f2 && f3 && f4)

#define w(i) (waitingL[i] || waitingR[i])
#define w0 w(0)
#define w1 w(1)
#define w2 w(2)
#define w3 w(3)
#define w4 w(4)
#define f0 (fork[0])
#define f1 (fork[1])
#define f2 (fork[2])
#define f3 (fork[3])
#define f4 (fork[4])

This property is violated in 1.1 (five philosophers "philosopherLR"), 
but holds in 1.2 (one philosopher "philosopherRL", four philosophers
"philosopherLR"). If you checked the formula requested in the exercise

[]!(w0 && w1 && w2 && w3 && w4)

then in both cases the formula is violated, so you do not see a difference
between both models.

The next property (if a philosopher is hungry, he eventually is eating)
can be formulated as

[](h0 -> <>!h0) && [](h1 -> <>!h1) && [](h2 -> <>!h2) && 
[](h3 -> <>!h3) && [](h4 -> <>!h4)

This property does not hold in the system, because of the lacking
fairness requirements.

This fairness requirement can be stated with the following
definitions

#define e0l (waitingL[0] && !fork[left(0)])
#define x0l (!waitingL[0])
#define e0r (waitingR[0] && !fork[right(0)])
#define x0r (!waitingR[0])
#define e1l (waitingL[1] && !fork[left(1)])
#define x1l (!waitingL[1])
#define e1r (waitingR[1] && !fork[right(1)])
#define x1r (!waitingR[1])
#define e2l (waitingL[2] && !fork[left(2)])
#define x2l (!waitingL[2])
#define e2r (waitingR[2] && !fork[right(2)])
#define x2r (!waitingR[2])
#define e3l (waitingL[3] && !fork[left(3)])
#define x3l (!waitingL[3])
#define e3r (waitingR[3] && !fork[right(3)])
#define x3r (!waitingR[3])
#define e4l (waitingL[4] && !fork[left(4)])
#define x4l (!waitingL[4])
#define e4r (waitingR[4] && !fork[right(4)])
#define x4r (!waitingR[4])

as

((<>[]e0l) -> (<>[]x0l)) && ((<>[]e0r) -> (<>[]x0r)) &&
((<>[]e1l) -> (<>[]x1l)) && ((<>[]e1r) -> (<>[]x1r)) &&
((<>[]e2l) -> (<>[]x2l)) && ((<>[]e2r) -> (<>[]x2r)) &&
((<>[]e3l) -> (<>[]x3l)) && ((<>[]e3r) -> (<>[]x3r)) &&
((<>[]e4l) -> (<>[]x4l)) && ((<>[]e4r) -> (<>[]x4r))

(if it is infinitely often the case that a philosopher is waiting for a fork
which is available, the philosopher infinitely often gets that fork).

That is, the formula to be checked is (Fairness Property -> Checked Property)

(((<>[]e0l) -> (<>[]x0l)) && ((<>[]e0r) -> (<>[]x0r)) &&
 ((<>[]e1l) -> (<>[]x1l)) && ((<>[]e1r) -> (<>[]x1r)) &&
 ((<>[]e2l) -> (<>[]x2l)) && ((<>[]e2r) -> (<>[]x2r)) &&
 ((<>[]e3l) -> (<>[]x3l)) && ((<>[]e3r) -> (<>[]x3r)) &&
 ((<>[]e4l) -> (<>[]x4l)) && ((<>[]e4r) -> (<>[]x4r)))
->
([](h0 -> <>!h0) && [](h1 -> <>!h1) && [](h2 -> <>!h2) && 
 [](h3 -> <>!h3) && [](h4 -> <>!h4))

Unfortunately, this formula is too big to be checked in Spin, since already the
creation of the property automaton runs forever (and eventually aborts since
the system runs out of memory).  I am sorry, I did not realize this in advance.
Thus I did not subtract points, if you tried to check this and failed.

2. Asynchronous Systems
-----------------------

Apparently, it was not clear to everyone that the protocol is appropriately
described by a *shared variable* model, since it describes how two components
can reliably transmit sequences of bits by reading and writing the states of
three wires. I should have clarified this, most of you modeled the system
using messages (if you have already high-level message passing available, this
low-level bit protocol does not make much sense any more).

A sample solution is posted as "protocol.txt" on the Web site.

Using the definitions

#define received (a == 1)
#define equal (y == x)
#define r0 (r == 0)

the two requested properties can be stated as

 [](received -> equal)

and

!([](r0 -> <>!r0) && [](!r0 -> <>r0))

The system model can be formalized as a shared variable model with the
transitions coming from both components. How this can be done, and how an
appropriate invariant for proving the first property looks like, I will
present in the last part of the course (see the slides "Verifying Concurrent
Systems with PVS" posted on the Web site).

However, I noticed that there are also fundamental unclarities what a system
*invariant* actually is. It is a *state formula* F, which describes the
relationship among variables in a *single* state, such that this formula is
true for every state of the system, i.e. []F holds. It is *not* a temporal
formula, describing relationships among different states. So it can look like
   
  Invariant(p, q, x, y, v, r, a) :<=>
    ...
    (p = 1 => q = 1 AND r = 0 AND a = 0) AND
    ...

if <p, q, x, y, v, r, a> are the variables describing the state
of the system but the formula cannot contain variables referring
to the successor state (p') and cannot contain temporal operators (U).