[tlaplus] Checking matrix multiplication correctness

["christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>]

Hi!

I have a spec which fails because of TLA+'s inability to handle real numbers, but I don't know how to re-state it to avoid this:

------------------------------- MODULE matmul -------------------------------
EXTENDS Integers, Sequences, TLC
CONSTANT n, S

  
(*
--algorithm matmul { 
   variables i=1, j=1, row \in S \X S \X S, A= [k \in 1..n |-> row], b \in S \X S \X S,x= [k \in 1..n |-> 0], d= [k \in 1..n |-> 0], test=b;
   { 
   
\* set lower triangular of matrix (excluding diagonal) to zero
Triangular:
    i := 1;
    loopi:
    while (i<=n){         
         j:= 1;
         loopj:
         while (j<=n) {
          if (i>j) {    
            A[i][j]:=0;
          };
          j := j+1;
         };
         i := i+1;
    };
    
Calc: 
\* Solve Ax = b for x via back substitution.
\* last element.
    x[n] := b[n] \div A[n][n];
\* the rest
    i := n-1;
    loopi1:
    while (i>=1){
         x[i] := b[i];         
         j:= n;
         loopj1:
         while (j>i) {
             x[i] := x[i]-x[j]*A[i][j];
             j := j-1;
         };
         x[i] := x[i] \div A[i][i];
         i := i-1;
    };

Check:
\* check correctness by calculating Ax=d , setting test=d and set test =b in the model checker (do this way so test always equals b unless d incorrect)
  i := 1;
  loopi2:
  while (i <= n) {
    j := 1;
    loopj2:
    while (j <= n) {   
     d[i] := d[i] + (x[j]*A[i][j]);
     j := j+1;
    };
   i := i+1;
  };
  test:=d;
   }
}

I initialise A and b to contain integers, so of course, sometimes x should contain non-integer values, which means that d (the check) does not equal b. How can I check this algorithm without initialising the arrays using integers? I see that there must be a fault in my thinking somewhere! Thanks in advance!

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d4b8a84a-4296-4583-85a5-76cfec10ffacn%40googlegroups.com.