------------------------------- MODULE ex_tab -------------------------------
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 = 0)
variables i,j,k=1,x=0;
{
a:i:=1;
b:while (i \leq n){
    c:j:=1;
    d:while (j \leq n){
        e:S[i,j]:=A[i,j]+B[i,j];
        p1:k:=1;
        p2:while (k < n+1){
            P[i,j]:=P[i,j]+ A[i,k]*B[k,j];
            k:=k+1;
        };
        f:j:=j+1;
        };
    g:i:=i+1;
    };
h:print <<"Happy end">>;
};
}

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

vars == << A, B, P, S, pc, i, j, k, x >>

ProcSet == {0}

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

a == /\ pc[0] = "a"
     /\ i' = 1
     /\ pc' = [pc EXCEPT ![0] = "b"]
     /\ UNCHANGED << A, B, P, S, j, k, x >>

b == /\ pc[0] = "b"
     /\ IF i \leq n
           THEN /\ pc' = [pc EXCEPT ![0] = "c"]
           ELSE /\ pc' = [pc EXCEPT ![0] = "h"]
     /\ UNCHANGED << A, B, P, S, i, j, k, x >>

c == /\ pc[0] = "c"
     /\ j' = 1
     /\ pc' = [pc EXCEPT ![0] = "d"]
     /\ UNCHANGED << A, B, P, S, i, k, x >>

d == /\ pc[0] = "d"
     /\ IF j \leq n
           THEN /\ pc' = [pc EXCEPT ![0] = "e"]
           ELSE /\ pc' = [pc EXCEPT ![0] = "g"]
     /\ UNCHANGED << A, B, P, S, i, j, k, x >>

e == /\ pc[0] = "e"
     /\ S' = [S EXCEPT ![i,j] = A[i,j]+B[i,j]]
     /\ pc' = [pc EXCEPT ![0] = "p1"]
     /\ UNCHANGED << A, B, P, i, j, k, x >>

p1 == /\ pc[0] = "p1"
      /\ k' = 1
      /\ pc' = [pc EXCEPT ![0] = "p2"]
      /\ UNCHANGED << A, B, P, S, i, j, x >>

p2 == /\ pc[0] = "p2"
      /\ IF k < n+1
            THEN /\ P' = [P EXCEPT ![i,j] = P[i,j]+ A[i,k]*B[k,j]]
                 /\ k' = k+1
                 /\ pc' = [pc EXCEPT ![0] = "p2"]
            ELSE /\ pc' = [pc EXCEPT ![0] = "f"]
                 /\ UNCHANGED << P, k >>
      /\ UNCHANGED << A, B, S, i, j, x >>

f == /\ pc[0] = "f"
     /\ j' = j+1
     /\ pc' = [pc EXCEPT ![0] = "d"]
     /\ UNCHANGED << A, B, P, S, i, k, x >>

g == /\ pc[0] = "g"
     /\ i' = i+1
     /\ pc' = [pc EXCEPT ![0] = "b"]
     /\ UNCHANGED << A, B, P, S, j, k, x >>

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

P_ == a \/ b \/ c \/ d \/ e \/ p1 \/ p2 \/ f \/ g \/ h

Next == P_
           \/ (* 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 16:53:16 CET 2015 by garnier34u
\* Created Fri Dec 04 16:14:27 CET 2015 by garnier34u