From 781d419ca3b3a6dcaccec439cf07740fe73047ad Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Sun, 18 Sep 2022 19:34:03 -0700 Subject: [PATCH] Add DyadicRationals module. Closes Github issue #63 https://github.com/tlaplus/CommunityModules/issues/63 Depends on https://github.com/tlaplus/tlaplus/commit/b5736cd6c6944a01dd719ee05ab81bf95a6fa371 [Feature] --- modules/DyadicRationals.tla | 53 ++++++++++++++ modules/tlc2/overrides/DyadicRationals.java | 80 +++++++++++++++++++++ modules/tlc2/overrides/TLCOverrides.java | 4 +- tests/AllTests.tla | 3 +- tests/DyadicRationalsTests.tla | 17 +++++ 5 files changed, 154 insertions(+), 3 deletions(-) create mode 100644 modules/DyadicRationals.tla create mode 100644 modules/tlc2/overrides/DyadicRationals.java create mode 100644 tests/DyadicRationalsTests.tla diff --git a/modules/DyadicRationals.tla b/modules/DyadicRationals.tla new file mode 100644 index 0000000..68dcd8e --- /dev/null +++ b/modules/DyadicRationals.tla @@ -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 \ No newline at end of file diff --git a/modules/tlc2/overrides/DyadicRationals.java b/modules/tlc2/overrides/DyadicRationals.java new file mode 100644 index 0000000..c555b9b --- /dev/null +++ b/modules/tlc2/overrides/DyadicRationals.java @@ -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); + } +} diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java index afa763b..e0df076 100644 --- a/modules/tlc2/overrides/TLCOverrides.java +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -44,7 +44,7 @@ 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( @@ -52,6 +52,6 @@ public Class[] get() { + "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 }; } } diff --git a/tests/AllTests.tla b/tests/AllTests.tla index c4770fd..44ecdd5 100644 --- a/tests/AllTests.tla +++ b/tests/AllTests.tla @@ -15,6 +15,7 @@ EXTENDS SequencesExtTests, CombinatoricsTests, FoldsTests, GraphsTests, - BagsExtTests + BagsExtTests, + DyadicRationalsTests =========================================== diff --git a/tests/DyadicRationalsTests.tla b/tests/DyadicRationalsTests.tla new file mode 100644 index 0000000..4730719 --- /dev/null +++ b/tests/DyadicRationalsTests.tla @@ -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]) +=============================================================================