|
| 1 | +/******************************************************************************* |
| 2 | + * Copyright (c) 2019 Microsoft Research. All rights reserved. |
| 3 | + * |
| 4 | + * The MIT License (MIT) |
| 5 | + * |
| 6 | + * Permission is hereby granted, free of charge, to any person obtaining a copy |
| 7 | + * of this software and associated documentation files (the "Software"), to deal |
| 8 | + * in the Software without restriction, including without limitation the rights |
| 9 | + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies |
| 10 | + * of the Software, and to permit persons to whom the Software is furnished to do |
| 11 | + * so, subject to the following conditions: |
| 12 | + * |
| 13 | + * The above copyright notice and this permission notice shall be included in all |
| 14 | + * copies or substantial portions of the Software. |
| 15 | + * |
| 16 | + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR |
| 17 | + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS |
| 18 | + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR |
| 19 | + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN |
| 20 | + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION |
| 21 | + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
| 22 | + * |
| 23 | + * Contributors: |
| 24 | + * Markus Alexander Kuppe - initial API and implementation |
| 25 | + ******************************************************************************/ |
| 26 | +package tlc2.overrides; |
| 27 | + |
| 28 | +import java.util.Arrays; |
| 29 | + |
| 30 | +import tlc2.output.EC; |
| 31 | +import tlc2.tool.EvalException; |
| 32 | +import tlc2.value.Values; |
| 33 | +import tlc2.value.impl.BoolValue; |
| 34 | +import tlc2.value.impl.SetEnumValue; |
| 35 | +import tlc2.value.impl.TupleValue; |
| 36 | +import tlc2.value.impl.Value; |
| 37 | + |
| 38 | +public final class Functions { |
| 39 | + |
| 40 | + private Functions() { |
| 41 | + // no-instantiation! |
| 42 | + } |
| 43 | + |
| 44 | + @TLAPlusOperator(identifier = "IsInjective", module = "Functions", warn = false) |
| 45 | + public static BoolValue IsInjective(final Value val) { |
| 46 | + if (val instanceof TupleValue) { |
| 47 | + return isInjectiveNonDestructive(((TupleValue) val).elems); |
| 48 | + } else { |
| 49 | + final Value conv = val.toTuple(); |
| 50 | + if (conv == null) { |
| 51 | + throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, |
| 52 | + new String[] { "IsInjective", "sequence", Values.ppr(val.toString()) }); |
| 53 | + } |
| 54 | + return isInjectiveDestructive(((TupleValue) conv).elems); |
| 55 | + } |
| 56 | + } |
| 57 | + |
| 58 | + // O(n log n) runtime and O(1) space. |
| 59 | + private static BoolValue isInjectiveDestructive(final Value[] values) { |
| 60 | + Arrays.sort(values); |
| 61 | + for (int i = 1; i < values.length; i++) { |
| 62 | + if (values[i-1].equals(values[i])) { |
| 63 | + return BoolValue.ValFalse; |
| 64 | + } |
| 65 | + } |
| 66 | + return BoolValue.ValTrue; |
| 67 | + } |
| 68 | + |
| 69 | + // Assume small arrays s.t. the naive approach with O(n^2) runtime but O(1) |
| 70 | + // space is good enough. Sorting values in-place is a no-go because it |
| 71 | + // would modify the TLA+ tuple. Elements can be any sub-type of Value, not |
| 72 | + // just IntValue. |
| 73 | + private static BoolValue isInjectiveNonDestructive(final Value[] values) { |
| 74 | + for (int i = 0; i < values.length; i++) { |
| 75 | + for (int j = i + 1; j < values.length; j++) { |
| 76 | + if (values[i].equals(values[j])) { |
| 77 | + return BoolValue.ValFalse; |
| 78 | + } |
| 79 | + } |
| 80 | + } |
| 81 | + return BoolValue.ValTrue; |
| 82 | + } |
| 83 | +} |
0 commit comments