-------------------------- MODULE serie9_4_paralel --------------------------
EXTENDS TLC, Integers, Naturals
CONSTANT n,A0,B0

I==(1..n) \X (1..n)

(*
--algorithm System{
variables A=A0,B=B0,P=[p \in I |-> 0],S=[p \in I |-> 0];
process (P \in I)
variables k=1;
{
        e:S[self[1],self[2]]:=A[self]+B[self]; \*self = self[1],self[2]
        p1:k:=1;
        p2:while (k < n+1){
            P[self]:=P[self]+ A[self[1],k]*B[k,self[2]];
            k:=k+1;
    };
h:print <<"Happy end">>;
}

}
*)
\* BEGIN TRANSLATION
\* Process P at line 10 col 1 changed to P_
VARIABLES A, B, P, S, pc, k

vars == << A, B, P, S, pc, k >>

ProcSet == (I)

Init == (* Global variables *)
        /\ A = A0
        /\ B = B0
        /\ P = [p \in I |-> 0]
        /\ S = [p \in I |-> 0]
        (* Process P_ *)
        /\ k = [self \in I |-> 1]
        /\ pc = [self \in ProcSet |-> "e"]

e(self) == /\ pc[self] = "e"
           /\ S' = [S EXCEPT ![self[1],self[2]] = A[self]+B[self]]
           /\ pc' = [pc EXCEPT ![self] = "p1"]
           /\ UNCHANGED << A, B, P, k >>

p1(self) == /\ pc[self] = "p1"
            /\ k' = [k EXCEPT ![self] = 1]
            /\ pc' = [pc EXCEPT ![self] = "p2"]
            /\ UNCHANGED << A, B, P, S >>

p2(self) == /\ pc[self] = "p2"
            /\ IF k[self] < n+1
                  THEN /\ P' = [P EXCEPT ![self] = P[self]+ A[self[1],k[self]]*B[k[self],self[2]]]
                       /\ k' = [k EXCEPT ![self] = k[self]+1]
                       /\ pc' = [pc EXCEPT ![self] = "p2"]
                  ELSE /\ pc' = [pc EXCEPT ![self] = "h"]
                       /\ UNCHANGED << P, k >>
            /\ UNCHANGED << A, B, S >>

h(self) == /\ pc[self] = "h"
           /\ PrintT(<<"Happy end">>)
           /\ pc' = [pc EXCEPT ![self] = "Done"]
           /\ UNCHANGED << A, B, P, S, k >>

P_(self) == e(self) \/ p1(self) \/ p2(self) \/ h(self)

Next == (\E self \in I: P_(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

=============================================================================
\* Modification History
\* Last modified Fri Dec 04 17:26:07 CET 2015 by garnier34u
\* Created Fri Dec 04 17:01:05 CET 2015 by garnier34u