diff --git a/build.xml b/build.xml index 84f60be..f7d3123 100644 --- a/build.xml +++ b/build.xml @@ -31,6 +31,7 @@ diff --git a/modules/tlc2/overrides/BagsExt.java b/modules/tlc2/overrides/BagsExt.java index cdd9565..97d387a 100644 --- a/modules/tlc2/overrides/BagsExt.java +++ b/modules/tlc2/overrides/BagsExt.java @@ -1,5 +1,6 @@ /******************************************************************************* * Copyright (c) 2022 Inria. All rights reserved. + * Copyright (c) 2023, Oracle and/or its affiliates. * * The MIT License (MIT) * @@ -64,7 +65,7 @@ public static Value foldBag(final OpValue op, final Value base, final Value bag) + Values.ppr(domain[i].toString()) + ":>" + Values.ppr(values[i].toString()) + ")" }); } for (int j = 0; j < ((IntValue) values[i]).val; j++) { - acc[0] = op.apply(acc, EvalControl.Clear); + acc[0] = op.eval(acc, EvalControl.Clear); } } diff --git a/modules/tlc2/overrides/FiniteSetsExt.java b/modules/tlc2/overrides/FiniteSetsExt.java index 101579e..33c04cf 100644 --- a/modules/tlc2/overrides/FiniteSetsExt.java +++ b/modules/tlc2/overrides/FiniteSetsExt.java @@ -1,5 +1,6 @@ /******************************************************************************* * Copyright (c) 2020 Microsoft Research. All rights reserved. + * Copyright (c) 2023, Oracle and/or its affiliates. * * The MIT License (MIT) * @@ -30,7 +31,6 @@ import tlc2.tool.EvalException; import tlc2.value.IBoolValue; import tlc2.value.Values; -import tlc2.value.impl.Applicable; import tlc2.value.impl.BoolValue; import tlc2.value.impl.Enumerable; import tlc2.value.impl.EnumerableValue; @@ -49,25 +49,19 @@ private FiniteSetsExt() { } @TLAPlusOperator(identifier = "Quantify", module = "FiniteSetsExt", warn = false) - public static Value quantify(final Value set, final Value pred) { + public static Value quantify(final Value set, final OpValue test) { if (!(set instanceof EnumerableValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "first", "Quantify", "set", Values.ppr(set.toString()) }); } - if (!(pred instanceof Applicable)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { "second", "Quantify", "boolean-valued operator", Values.ppr(pred.toString()) }); - } - int size = 0; - final Applicable test = (Applicable) pred; final ValueEnumeration enumSet = ((SetEnumValue) set.toSetEnum()).elements(); Value elem; final Value[] args = new Value[1]; while ((elem = enumSet.nextElement()) != null) { args[0] = elem; - Value val = test.apply(args, EvalControl.Clear); + Value val = test.eval(args, EvalControl.Clear); if (val instanceof IBoolValue) { if (((BoolValue) val).val) { size++; @@ -112,10 +106,10 @@ public static Value foldSet(final OpValue op, final Value base, final Enumerable final ValueEnumeration ve = set.elements(); - Value v = null; + Value v; while ((v = ve.nextElement()) != null) { args[0] = v; - args[1] = op.apply(args, EvalControl.Clear); + args[1] = op.eval(args, EvalControl.Clear); } return args[1]; diff --git a/modules/tlc2/overrides/Functions.java b/modules/tlc2/overrides/Functions.java index 626faa7..106c00f 100644 --- a/modules/tlc2/overrides/Functions.java +++ b/modules/tlc2/overrides/Functions.java @@ -1,5 +1,6 @@ /******************************************************************************* * Copyright (c) 2019 Microsoft Research. All rights reserved. + * Copyright (c) 2023, Oracle and/or its affiliates. * * The MIT License (MIT) * @@ -31,10 +32,10 @@ import tlc2.tool.EvalControl; import tlc2.tool.EvalException; import tlc2.value.Values; -import tlc2.value.impl.Applicable; import tlc2.value.impl.BoolValue; import tlc2.value.impl.Enumerable; import tlc2.value.impl.FcnRcdValue; +import tlc2.value.impl.FunctionValue; import tlc2.value.impl.OpValue; import tlc2.value.impl.SetOfRcdsValue; import tlc2.value.impl.TupleValue; @@ -123,11 +124,11 @@ public static Value foldFunction(final OpValue op, final Value base, final Value // Can assume type of OpValue because tla2sany.semantic.Generator.java will // make sure that the first parameter is a binary operator. - if (!(fun instanceof Applicable)) { + if (!(fun instanceof FunctionValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "FoldFunction", "function", Values.ppr(fun.toString()) }); } - return foldFunctionOnSet(op, base, fun, ((Applicable) fun).getDomain()); + return foldFunctionOnSet(op, base, fun, ((FunctionValue) fun).getDomain()); } @TLAPlusOperator(identifier = "FoldFunctionOnSet", module = "Functions", warn = false) @@ -135,11 +136,11 @@ public static Value foldFunctionOnSet(final OpValue op, final Value base, final // Can assume type of OpValue because tla2sany.semantic.Generator.java will // make sure that the first parameter is a binary operator. - if (!(v3 instanceof Applicable)) { + if (!(v3 instanceof FunctionValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "FoldFunctionOnSet", "function", Values.ppr(v3.toString()) }); } - final Applicable fun = (Applicable) v3; + final FunctionValue fun = (FunctionValue) v3; if (!(v4 instanceof Enumerable)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "fourth", "FoldFunctionOnSet", "set", Values.ppr(v4.toString()) }); @@ -152,10 +153,10 @@ public static Value foldFunctionOnSet(final OpValue op, final Value base, final final ValueEnumeration ve = subdomain.elements(); - Value v = null; + Value v; while ((v = ve.nextElement()) != null) { - args[0] = fun.select(v); - args[1] = op.apply(args, EvalControl.Clear); + args[0] = fun.apply(v, EvalControl.Clear); + args[1] = op.eval(args, EvalControl.Clear); } return args[1]; diff --git a/modules/tlc2/overrides/GraphViz.java b/modules/tlc2/overrides/GraphViz.java index 30fb1aa..caf8263 100644 --- a/modules/tlc2/overrides/GraphViz.java +++ b/modules/tlc2/overrides/GraphViz.java @@ -1,5 +1,6 @@ /******************************************************************************* * Copyright (c) 2023 Microsoft Research. All rights reserved. + * Copyright (c) 2023, Oracle and/or its affiliates. * * The MIT License (MIT) * @@ -27,7 +28,7 @@ import tlc2.tool.EvalControl; import tlc2.util.FP64; -import tlc2.value.impl.Applicable; +import tlc2.value.impl.OpValue; import tlc2.value.impl.RecordValue; import tlc2.value.impl.SetEnumValue; import tlc2.value.impl.StringValue; @@ -38,24 +39,12 @@ public class GraphViz { @TLAPlusOperator(identifier = "DotDiGraph", module = "GraphViz", warn = false) - public static Value dotDiGraph(final Value v1, final Value v2, final Value v3) throws Exception { + public static Value dotDiGraph(final Value v1, final OpValue vl, final OpValue el) throws Exception { if (!(v1 instanceof RecordValue) || v1.toRcd() == null) { throw new Exception("An DiGraph must be a record. Value given is of type: " + v1.getClass().getName()); } final RecordValue g = (RecordValue) v1.toRcd(); - if (!(v2 instanceof Applicable)) { - throw new Exception( - "Second parameter must be an Applicable. Value given is of type: " + v2.getClass().getName()); - } - final Applicable vl = (Applicable) v2; - - if (!(v3 instanceof Applicable)) { - throw new Exception( - "Third parameter must be an Applicable. Value given is of type: " + v2.getClass().getName()); - } - final Applicable el = (Applicable) v3; - String dotString = "digraph MyGraph {"; // Nodes @@ -65,7 +54,7 @@ public static Value dotDiGraph(final Value v1, final Value v2, final Value v3) t Value val = null; while ((val = elements.nextElement()) != null) { dotString += String.format("%s[label=%s];", val.fingerPrint(FP64.New()), - vl.apply(new Value[] { val }, EvalControl.Clear)); + vl.eval(new Value[] { val }, EvalControl.Clear)); } // Edges @@ -75,7 +64,7 @@ public static Value dotDiGraph(final Value v1, final Value v2, final Value v3) t while ((val = elements.nextElement()) != null) { TupleValue tv = (TupleValue) val.toTuple(); dotString += String.format("%s->%s[label=%s];", tv.elems[0].fingerPrint(FP64.New()), - tv.elems[1].fingerPrint(FP64.New()), el.apply(new Value[] { tv }, EvalControl.Clear)); + tv.elems[1].fingerPrint(FP64.New()), el.eval(new Value[] { tv }, EvalControl.Clear)); } dotString += "}"; diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java index a01e6c0..4c6cb19 100644 --- a/modules/tlc2/overrides/SequencesExt.java +++ b/modules/tlc2/overrides/SequencesExt.java @@ -1,6 +1,7 @@ package tlc2.overrides; /******************************************************************************* * Copyright (c) 2019 Microsoft Research. All rights reserved. + * Copyright (c) 2023, Oracle and/or its affiliates. * * The MIT License (MIT) * @@ -40,7 +41,6 @@ import tlc2.value.IBoolValue; import tlc2.value.IValue; import tlc2.value.Values; -import tlc2.value.impl.Applicable; import tlc2.value.impl.BoolValue; import tlc2.value.impl.FcnRcdValue; import tlc2.value.impl.IntValue; @@ -275,7 +275,7 @@ public static Value foldLeft(final OpValue op, final Value base, final Value val final Value[] elems = tv.elems; for (int i = 0; i < elems.length; i++) { args[1] = elems[i]; - args[0] = op.apply(args, EvalControl.Clear); + args[0] = op.eval(args, EvalControl.Clear); } return args[0]; @@ -299,7 +299,7 @@ public static Value foldRight(final OpValue op, final Value val, final Value bas final Value[] elems = tv.elems; for (int i = elems.length - 1; i >= 0; i--) { args[0] = elems[i]; - args[1] = op.apply(args, EvalControl.Clear); + args[1] = op.eval(args, EvalControl.Clear); } return args[1]; @@ -381,25 +381,20 @@ public static Value isPrefix(final Value v1, final Value v2) { } @TLAPlusOperator(identifier = "SelectInSeq", module = "SequencesExt", warn = false) - public static Value selectInSeq(final Value s, final Value test) { + public static Value selectInSeq(final Value s, final OpValue test) { final TupleValue seq = (TupleValue) s.toTuple(); if (seq == null) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "first", "SelectInSeq", "sequence", Values.ppr(s.toString()) }); } - if (!(test instanceof Applicable)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { "third", "SelectInSeq", "function", Values.ppr(test.toString()) }); - } final int len = seq.size(); - final Applicable ftest = (Applicable) test; final Value[] args = new Value[1]; for (int i = 0; i < len; i++) { args[0] = seq.elems[i]; - final Value val = ftest.apply(args, EvalControl.Clear); + final Value val = test.eval(args, EvalControl.Clear); if (!(val instanceof IBoolValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "SelectInSeq", - "boolean-valued function", Values.ppr(test.toString()) }); + "boolean-valued operator", Values.ppr(test.toString()) }); } if (((BoolValue) val).val) { return IntValue.gen(i + 1); @@ -409,7 +404,7 @@ public static Value selectInSeq(final Value s, final Value test) { } @TLAPlusOperator(identifier = "SelectInSubSeq", module = "SequencesExt", warn = false) - public static Value SelectInSubSeq(final Value s, final Value f, final Value t, final Value test) { + public static Value SelectInSubSeq(final Value s, final Value f, final Value t, final OpValue test) { final TupleValue seq = (TupleValue) s.toTuple(); if (seq == null) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, @@ -423,10 +418,6 @@ public static Value SelectInSubSeq(final Value s, final Value f, final Value t, throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "SelectInSubSeq", "natural", Values.ppr(t.toString()) }); } - if (!(test instanceof Applicable)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { "fourth", "SelectInSubSeq", "function", Values.ppr(test.toString()) }); - } int from = ((IntValue) f).val; final int to = ((IntValue) t).val; @@ -442,15 +433,14 @@ public static Value SelectInSubSeq(final Value s, final Value f, final Value t, throw new EvalException(EC.TLC_MODULE_ARGUMENT_NOT_IN_DOMAIN, new String[] { "third", "SelectInSubSeq", "first", Values.ppr(s.toString()), Values.ppr(t.toString()) }); } - - final Applicable ftest = (Applicable) test; + final Value[] args = new Value[1]; for (; from <= to; from++) { args[0] = seq.elems[from - 1]; - final Value val = ftest.apply(args, EvalControl.Clear); + final Value val = test.eval(args, EvalControl.Clear); if (!(val instanceof IBoolValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "fourth", "SelectInSubSeq", - "boolean-valued function", Values.ppr(test.toString()) }); + "boolean-valued operator", Values.ppr(test.toString()) }); } if (((BoolValue) val).val) { return IntValue.gen(from); @@ -460,22 +450,17 @@ public static Value SelectInSubSeq(final Value s, final Value f, final Value t, } @TLAPlusOperator(identifier = "SelectLastInSeq", module = "SequencesExt", warn = false) - public static Value selectLastInSeq(final Value s, final Value test) { + public static Value selectLastInSeq(final Value s, final OpValue test) { final TupleValue seq = (TupleValue) s.toTuple(); if (seq == null) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "first", "SelectLastInSeq", "sequence", Values.ppr(s.toString()) }); } - if (!(test instanceof Applicable)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { "third", "SelectLastInSeq", "function", Values.ppr(test.toString()) }); - } int i = seq.size() - 1; - final Applicable ftest = (Applicable) test; final Value[] args = new Value[1]; for (; i >= 0; i--) { args[0] = seq.elems[i]; - final Value val = ftest.apply(args, EvalControl.Clear); + final Value val = test.eval(args, EvalControl.Clear); if (!(val instanceof IBoolValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "SelectLastInSeq", "boolean-valued function", Values.ppr(test.toString()) }); @@ -488,7 +473,7 @@ public static Value selectLastInSeq(final Value s, final Value test) { } @TLAPlusOperator(identifier = "SelectLastInSubSeq", module = "SequencesExt", warn = false) - public static Value SelectLastInSubSeq(final Value s, final Value f, final Value t, final Value test) { + public static Value SelectLastInSubSeq(final Value s, final Value f, final Value t, final OpValue test) { final TupleValue seq = (TupleValue) s.toTuple(); if (seq == null) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, @@ -502,10 +487,6 @@ public static Value SelectLastInSubSeq(final Value s, final Value f, final Value throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "SelectLastInSubSeq", "natural", Values.ppr(t.toString()) }); } - if (!(test instanceof Applicable)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { "fourth", "SelectLastInSubSeq", "function", Values.ppr(test.toString()) }); - } final int from = ((IntValue) f).val; int to = ((IntValue) t).val; @@ -521,12 +502,11 @@ public static Value SelectLastInSubSeq(final Value s, final Value f, final Value throw new EvalException(EC.TLC_MODULE_ARGUMENT_NOT_IN_DOMAIN, new String[] { "third", "SelectLastInSubSeq", "first", Values.ppr(s.toString()), Values.ppr(t.toString()) }); } - - final Applicable ftest = (Applicable) test; + final Value[] args = new Value[1]; for (; to >= from; to--) { args[0] = seq.elems[to - 1]; - final Value val = ftest.apply(args, EvalControl.Clear); + final Value val = test.eval(args, EvalControl.Clear); if (!(val instanceof IBoolValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "fourth", "SelectLastInSubSeq", "boolean-valued function", Values.ppr(test.toString()) }); @@ -561,17 +541,12 @@ public static Value removeFirst(final Value s, final Value e) { } @TLAPlusOperator(identifier = "RemoveFirstMatch", module = "SequencesExt", warn = false) - public static Value removeFirstMatch(final Value s, final Value test) { + public static Value removeFirstMatch(final Value s, final OpValue test) { final TupleValue seq = (TupleValue) s.toTuple(); if (seq == null) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "first", "RemoveFirstMatch", "sequence", Values.ppr(s.toString()) }); } - if (!(test instanceof Applicable)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { "second", "RemoveFirstMatch", "function", Values.ppr(test.toString()) }); - } - final Applicable ftest = (Applicable) test; final Value[] args = new Value[1]; final ArrayList val = new ArrayList<>(seq.elems.length); @@ -580,7 +555,7 @@ public static Value removeFirstMatch(final Value s, final Value test) { for (int i = 0; i < seq.elems.length; i++) { if (!found) { args[0] = seq.elems[i]; - final Value bval = ftest.apply(args, EvalControl.Clear); + final Value bval = test.eval(args, EvalControl.Clear); if (!(bval instanceof IBoolValue)) { throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "second", "RemoveFirstMatch", "boolean-valued function", Values.ppr(test.toString()) }); diff --git a/modules/tlc2/overrides/VectorClocks.java b/modules/tlc2/overrides/VectorClocks.java index 97d573d..1bc1565 100644 --- a/modules/tlc2/overrides/VectorClocks.java +++ b/modules/tlc2/overrides/VectorClocks.java @@ -1,5 +1,6 @@ /******************************************************************************* * Copyright (c) 2023 Microsoft Research. All rights reserved. + * Copyright (c) 2023, Oracle and/or its affiliates. * * The MIT License (MIT) * @@ -35,9 +36,9 @@ import java.util.Set; import tlc2.tool.EvalControl; -import tlc2.value.impl.Applicable; import tlc2.value.impl.Enumerable; import tlc2.value.impl.IntValue; +import tlc2.value.impl.OpValue; import tlc2.value.impl.TupleValue; import tlc2.value.impl.Value; import tlc2.value.impl.ValueEnumeration; @@ -96,18 +97,18 @@ public Value delete() { * ff02d48ed2bcda065f326aa25409cb317be9feb9/js/model/modelGraph.js */ @TLAPlusOperator(identifier = "CausalOrder", module = "VectorClocks", warn = false) - public static Value causalOrder(final TupleValue v, final Applicable opClock, final Applicable opNode, - final Applicable opDomain) { + public static Value causalOrder(final TupleValue v, final OpValue opClock, final OpValue opNode, + final OpValue opDomain) { // A1) Sort each node's individual log which can be totally ordered. final Map> n2l = new HashMap<>(); for (int j = 0; j < v.elems.length; j++) { final Value val = v.elems[j]; - final Value nodeId = opNode.apply(new Value[] { val }, EvalControl.Clear); - final Value vc = opClock.apply(new Value[] { val }, EvalControl.Clear); + final Value nodeId = opNode.eval(new Value[] { val }, EvalControl.Clear); + final Value vc = opClock.eval(new Value[] { val }, EvalControl.Clear); final Value nodeTime = vc.select(new Value[] { nodeId }); - final Enumerable dom = (Enumerable) opDomain.apply(new Value[] { vc }, EvalControl.Clear).toSetEnum(); + final Enumerable dom = (Enumerable) opDomain.eval(new Value[] { vc }, EvalControl.Clear).toSetEnum(); final LinkedList list = n2l.computeIfAbsent(nodeId, k -> new LinkedList()); list.add(new GraphNode(vc, nodeTime, dom, val));