Skip to content

Commit

Permalink
Add DyadicRationals module.
Browse files Browse the repository at this point in the history
Closes Github issue #63
#63

Depends on
tlaplus/tlaplus@b5736cd

[Feature]
  • Loading branch information
lemmy committed Sep 19, 2022
1 parent 9a76515 commit 781d419
Showing 5 changed files with 154 additions and 3 deletions.
53 changes: 53 additions & 0 deletions modules/DyadicRationals.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
-------------------------- MODULE DyadicRationals ---------------------------
\* https://en.wikipedia.org/wiki/Dyadic_rational
LOCAL INSTANCE FiniteSets
LOCAL INSTANCE Integers
LOCAL INSTANCE Sequences
LOCAL INSTANCE FiniteSetsExt
LOCAL INSTANCE TLC

LOCAL Divides(p, q) ==
\E d \in 1..q : q = p * d

LOCAL Divisors(q) ==
{d \in 1..q : Divides(d, q)}

LOCAL GCD(n, m) ==
Max(Divisors(n) \cap Divisors(m))

------------------------------------------------------------------------------

LOCAL Rational(num, den) ==
[num |-> num, den |-> den]

LOCAL Reduce(p) ==
LET gcd == GCD(p.num, p.den)
IN IF gcd = 1 THEN p
ELSE Rational(p.num \div gcd, p.den \div gcd)

IsDyadicRational(r) ==
\E i \in 0..r.den: 2^i = r.den

Zero == Rational(0,1)

One == Rational(1,1)

Add(p, q) ==
IF p = Zero THEN q ELSE
LET lcn == Max({p.den, q.den}) \* shortcut because dyadic!
qq == Rational(q.num * (lcn \div q.den), q.den * (lcn \div q.den))
pp == Rational(p.num * (lcn \div p.den), p.den * (lcn \div p.den))
IN Reduce(Rational(qq.num + pp.num, lcn))

Half(p) ==
Reduce(Rational(p.num, p.den * 2))

PrettyPrint(p) ==
IF p = Zero THEN "0" ELSE
IF p = One THEN "1" ELSE
ToString(p.num) \o "/" \o ToString(p.den)

===============================================================================
\* Modification History
\* Last modified Mon Dec 27 17:52:54 PST 2021 by Markus Kuppe
\* Created Sun Dec 26 01:36:40 PDT 2021 by Markus Kuppe
80 changes: 80 additions & 0 deletions modules/tlc2/overrides/DyadicRationals.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
/*******************************************************************************
* Copyright (c) 2022 Microsoft Research. All rights reserved.
*
* The MIT License (MIT)
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
* of the Software, and to permit persons to whom the Software is furnished to do
* so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
* AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
* WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*
* Contributors:
* Markus Alexander Kuppe - initial API and implementation
******************************************************************************/
package tlc2.overrides;

import org.apache.commons.math3.util.ArithmeticUtils;

import tlc2.output.EC;
import tlc2.tool.EvalControl;
import tlc2.tool.EvalException;
import tlc2.value.Values;
import tlc2.value.impl.IntValue;
import tlc2.value.impl.RecordValue;
import tlc2.value.impl.StringValue;
import tlc2.value.impl.Value;
import util.UniqueString;

public class DyadicRationals {

private static final StringValue DEN = new StringValue("den");
private static final StringValue NUM = new StringValue("num");

/*
LOCAL Reduce(p) ==
LET gcd == GCD(p.num, p.den)
IN IF gcd = 1 THEN p
ELSE Rational(p.num \div gcd, p.den \div gcd)
*/
@TLAPlusOperator(identifier = "Reduce", module = "DyadicRationals", warn = false)
public static synchronized Value reduce(final Value val) {
if (!(val instanceof RecordValue)) {
throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
new String[] { "Half", "record", Values.ppr(val.toString()) });
}

final RecordValue r = (RecordValue) val;
r.normalize();

final IntValue d = (IntValue) r.apply(DEN, EvalControl.Clear);
final IntValue n = (IntValue) r.apply(NUM, EvalControl.Clear);

final int gcd = ArithmeticUtils.gcd(n.val, d.val);
if (gcd == 1) {
return r;
}

final UniqueString[] names = new UniqueString[2];
names[0] = DEN.val;
names[1] = NUM.val;

final Value[] values = new Value[2];
values[0] = IntValue.gen(d.val / gcd);
values[1] = IntValue.gen(n.val / gcd);

return new RecordValue(names, values, false);
}
}
4 changes: 2 additions & 2 deletions modules/tlc2/overrides/TLCOverrides.java
Original file line number Diff line number Diff line change
@@ -44,14 +44,14 @@ public Class[] get() {
// Remove `Json.resolves();` call when this Class is moved to `TLC`.
Json.resolves();
return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class,
FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class };
FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class };
} catch (NoClassDefFoundError e) {
// Remove this catch when this Class is moved to `TLC`.
System.out.println(
"gson dependencies of Json overrides not found, Json module won't work unless "
+ "the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC.");
}
return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class,
FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class };
FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class };
}
}
3 changes: 2 additions & 1 deletion tests/AllTests.tla
Original file line number Diff line number Diff line change
@@ -15,6 +15,7 @@ EXTENDS SequencesExtTests,
CombinatoricsTests,
FoldsTests,
GraphsTests,
BagsExtTests
BagsExtTests,
DyadicRationalsTests

===========================================
17 changes: 17 additions & 0 deletions tests/DyadicRationalsTests.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
------------------------- MODULE DyadicRationalsTests -------------------------
EXTENDS DyadicRationals

ASSUME LET T == INSTANCE TLC IN T!PrintT("DyadicRationalsTests")

ASSUME(Half(One) = [num |-> 1, den |-> 2])
ASSUME(Half([num |-> 1, den |-> 2]) = [num |-> 1, den |-> 4])
ASSUME(Half([num |-> 1, den |-> 4]) = [num |-> 1, den |-> 8])
ASSUME(Half([num |-> 1, den |-> 8]) = [num |-> 1, den |-> 16])
ASSUME(Half([num |-> 1, den |-> 16]) = [num |-> 1, den |-> 32])
ASSUME(Half([num |-> 1, den |-> 32]) = [num |-> 1, den |-> 64])
ASSUME(Half([num |-> 1, den |-> 64]) = [num |-> 1, den |-> 128])
ASSUME(Half([num |-> 1, den |-> 128]) = [num |-> 1, den |-> 256])
ASSUME(Half([num |-> 1, den |-> 256]) = [num |-> 1, den |-> 512])

ASSUME(Half([num |-> 2, den |-> 8]) = [num |-> 1, den |-> 8])
=============================================================================

0 comments on commit 781d419

Please sign in to comment.