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
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!