Checking matrix multiplication correctness

[christin...@gmail.com]

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!

[Andrew Helwer]

Have you considered using rationals? There's a module called DyadicRationals in the community modules: https://github.com/tlaplus/CommunityModules/blob/master/modules/DyadicRationals.tla

Andrew

[christin...@gmail.com]

Thanks Andrew! I've added the most recent version of the community modules to my TLA+ Toolbox (and I'm using v 1.7.1 of the toolbox), and I get the error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NoClassDefFoundError
: tlc2/value/impl/KSubsetValue

What am I doing wrong?

[Markus Kuppe]

Unfortunately, the latest version of the CommunityModules is only compatible with the most recent version of TLC. You will have to download a nightly build of the Toolbox from https://nightly.tlapl.us/products/

Markus

[christin...@gmail.com]

Thanks! That fixed it :) I have one further (and very silly) question - how do I actually use the functions defined in the community modules, the toolbox doesn't recognise, for example Divides, from the DyadicRadtionals module. I have added an EXTENDS DyadicRationals to my spec, but this hasn't helped. Is it because Divides is "LOCAL"? But then how could you use it at all? I can't seem to find the answer anywhere else!

[Markus Kuppe]

https://www.youtube.com/watch?v=w9t6JnmxV2E (more details at https://github.com/tlaplus/CommunityModules/?tab=readme-ov-file#how-to-use-it)

Markus