# [tlaplus] Re: Checking matrix multiplication correctness

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?
On Tuesday, January 9, 2024 at 2:38:29 AM UTC Andrew Helwer wrote:
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

On Tuesday, January 9, 2024 at 8:58:23 AM UTC+8 christin...@xxxxxxxxx wrote:
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.