Problem 1:

EF(!Ack)
= E(true U !Ack)

AX(Ack)
= !(EX(!Ack))

AG(EF(Reset))
= !(EF!(EF(Reset)))
= !(E(true U !E( true U Reset)))

AG(Req) => AG(Ack)
= !(AG(Req)) v AG(Ack)
= EF!Req v !(EF(!Ack))
= E(true U !Req) v !(E(true U !Ack))

Problem 2:

* mutual exclusion: G(!@p2 v !@q2)

* Mutual exclusion is respected.

Suppose mutex is not respected.

Assume a shortest sequence that violates it "c0 e1 c1 e2 c2 ... en cn"
where ei are transitions in t1, t2, t3, s1, s2, s3 and ci are
configurations describing the states of the processes and the values
of i and u.

Because the sequence is a shortest sequence, then any configuration ci
with i < n statisfies mutual exclusion.

Observe u=0 initially and it is set to 1 on entry to p2 or q2 and back
to 0 on exit. Because mutual exclusion is respected in any ci for i <
n, then, for any ci for i < n, we have u=1 iff a process is at its
critical section. 

Now the step en of the sequence violated mutual exclusion.  Suppose it
was p @p1 who took t2 when q was @q2. (the case where s takes s2 is
similar). So en is t2 and cn-1 has p at p1 with i=1.

The fact that i=1 requires p to have crossed t1 after the last time q
crossed s1. (otherwise i would be 2 not 1).

So q crossed s1 before p crossed t1.

Since q managed to access q2, it should have taken s2 before p took t1
(as if it would have waited for p to come to p1, it would not be able
to take s2).

But then u must have been 1 and t1 should not have been fired.

------------------------------------------------------------

* G(@p1 => F @p2)

* automaton:

 s0 -- @p1 and !@p2 --> s1

 s1 -- @p2 --> s0

 s1 -- true --> s1

 s0 -- !@p1 --> s0

 s0 initial and accepting.



* No becuase p could move to p1, then q moves to q1 then q2 and then p
  is stuck at p1.

Problem 3:

* x1 has to be 2 and x2 has to be 3, so f(x1)=f(2) and hence
rd(wr(arr,3,x3),3)=x3 has to be x1+x3 which is unsat.

* (v0 xor v1) = (v2 v v3).

       v0
    0/   \1
    v1   v1
   0| \1/ |0
    | / \ |
    v2   v2
   / |0  0| \
  /  v3   v3  \
1|  1|\0/ |1  |1 
  \  |/ \ |  /
   \ 0   1  /

Problem 4:

Inv: r = (q^p - 1) / (q - 1) and p <= n

-----------------
* Q => Inv?

assume r=1, p=1, n>=1 and q>=2

show r = (q^p - 1) / (q - 1) and p <= n.

since p=1 and n>=1 then p <= n.

since p = 1 then q^p-1 = q-1. Since q >= 2 then q-1 != 0 and q-1/q-1 = 1.

since r=1 then r = (q^p - 1) / (q-1)

-----------------

* {Inv and B} stmt {Inv} ?

We compute wp(r:= r+q^p; p:= p+1; r = (q^p - 1) / (q - 1) and p <= n) and
show it is implied by (Inv and B).

wp(r:= r+q^p; p:= p+1; r = (q^p - 1) / (q - 1) and p <= n)
= 
wp(r:= r+q^p; r = (q^(p+1) - 1) / (q - 1) and (p+1) <= n)
=
r+q^p = (q^(p+1) - 1) / (q - 1) and (p+1) <= n

We assume (Inv and B), i.e., r = (q^p - 1) / (q - 1) and p <= n and p < n
and show r+q^p = (q^(p+1) - 1) / (q - 1) and (p+1) <= n.

Since p < n then (p+1) <= n holds
since r = (q^p - 1) / (q - 1) then

r+q^p 
= (q^p - 1) / (q - 1)+q^p 
= (q^p - 1 + q^(p+1) - q^p) / (q-1)
= (q^(p+1) - 1) / (q-1)

Hence r+q^p = (q^(p+1) - 1) / (q - 1)

--------------

* Inv and !B => R ?

We assume (Inv and !B),
i.e., r = (q^p - 1) / (q - 1) and p <= n and !(p < n)
and show r = (q^n - 1) / (q - 1)

Since p<=n and !(p<n) we get p=n
Since r = (q^p - 1) / (q - 1) and p = n we get r= (q^n - 1) / (q - 1)

------------------

A suitable variant function would be v=n-p.
You need to show
* {Inv and B} => v>0
* {Inv and B and v=v0} r:= r+q^p; p := p+1 {v < v0}

------------------------