From 987b74c09bcb7872ada9b2dc1fc698e7cf73d697 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Fri, 27 May 2022 19:34:43 +0200 Subject: [PATCH 1/8] #196 Add choice/reverse wrapper variable ordering algorithms. --- .../datasynth/varorder/ChoiceVarOrderer.java | 95 +++++++++++++++++++ .../datasynth/varorder/ReverseVarOrderer.java | 58 +++++++++++ .../escet/common/java/ArrayUtilsTest.java | 40 +++++++- .../eclipse/escet/common/java/ArrayUtils.java | 19 ++++ 4 files changed, 211 insertions(+), 1 deletion(-) create mode 100644 cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java create mode 100644 cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java new file mode 100644 index 000000000..8e02f8e0b --- /dev/null +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java @@ -0,0 +1,95 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2022 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.datasynth.varorder; + +import java.util.List; + +import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; +import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; +import org.eclipse.escet.common.java.Assert; + +/** Variable ordering algorithm that applies multiple other algorithms, and picks the one with the lowest total span. */ +public class ChoiceVarOrderer implements VarOrderer { + /** The name of the choice-based algorithm, or {@code null} if no name is given. */ + private final String name; + + /** The algorithms to apply. At least two algorithms. */ + private final List algorithms; + + /** + * Constructor for the {@link ChoiceVarOrderer} class. Does not name the choice-based algorithm. + * + * @param algorithms The sequence of algorithms to apply. Must be at least two algorithms. + */ + public ChoiceVarOrderer(List algorithms) { + this(null, algorithms); + } + + /** + * Constructor for the {@link ChoiceVarOrderer} class. + * + * @param name The name of the choice-based algorithm. + * @param algorithms The sequence of algorithms to apply. Must be at least two algorithms. + */ + public ChoiceVarOrderer(String name, List algorithms) { + this.name = name; + this.algorithms = algorithms; + Assert.check(algorithms.size() >= 2); + } + + @Override + public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, + int dbgLevel) + { + // Debug output before applying the algorithms. + if (dbgEnabled) { + if (name == null) { + helper.dbg(dbgLevel, "Applying multiple algorithms, and choosing the best result:"); + } else { + helper.dbg(dbgLevel, "Applying %s algorithm:", name); + } + } + + // Initialize best order. + SynthesisVariable[] bestOrder = null; + long bestSpan = Long.MAX_VALUE; + + // Apply each algorithm. + for (int i = 0; i < algorithms.size(); i++) { + // Separate debug output of this algorithm from that of the previous one. + if (i > 0 && dbgEnabled) { + helper.dbg(); + } + + // Apply algorithm. Each algorithm is independently applied to the input variable order. + VarOrderer algorithm = algorithms.get(i); + SynthesisVariable[] algoOrder = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); + + // Update best order. + long algoSpan = helper.computeTotalSpan(algoOrder); + if (algoSpan < bestSpan) { + bestOrder = algoOrder; + bestSpan = algoSpan; + + if (dbgEnabled) { + helper.dbg(dbgLevel + 1, "Found new best variable order."); + } + } + } + + // Return the best variable order. + Assert.notNull(bestOrder); + return bestOrder; + } +} diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java new file mode 100644 index 000000000..1a0d07606 --- /dev/null +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java @@ -0,0 +1,58 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2022 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.datasynth.varorder; + +import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; +import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; +import org.eclipse.escet.common.java.ArrayUtils; + +/** Variable ordering algorithm that returns the reverse order of another algorithm. */ +public class ReverseVarOrderer implements VarOrderer { + /** The algorithm to apply. */ + private final VarOrderer algorithm; + + /** + * Constructor for the {@link ReverseVarOrderer} class. + * + * @param algorithm The algorithm to apply. + */ + public ReverseVarOrderer(VarOrderer algorithm) { + this.algorithm = algorithm; + } + + @Override + public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, + int dbgLevel) + { + // Debug output before applying the algorithms. + if (dbgEnabled) { + helper.dbg(dbgLevel, "Applying algorithm, and reversing its result:"); + } + + // Apply the algorithm. + SynthesisVariable[] order = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); + + // Reverse the order. + SynthesisVariable[] reverseOrder = ArrayUtils.reverse(order); + + // Debug output after applying the algorithms. + if (dbgEnabled) { + helper.dbg(dbgLevel, "Reversed the variable order."); + helper.dbgTotalSpan(dbgLevel, reverseOrder, "reversed"); + } + + // Return the resulting variable order. + return reverseOrder; + } +} diff --git a/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java b/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java index 3e9acfb07..12a608069 100644 --- a/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java +++ b/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java @@ -14,7 +14,11 @@ package org.eclipse.escet.common.java; import static org.eclipse.escet.common.java.ArrayUtils.array; +import static org.eclipse.escet.common.java.ArrayUtils.reverse; +import static org.eclipse.escet.common.java.Lists.list; import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotSame; +import static org.junit.Assert.assertSame; import java.util.Arrays; import java.util.List; @@ -38,10 +42,44 @@ public class ArrayUtilsTest { assertEquals("[a, b]", Arrays.deepToString(as1)); assertEquals("[]", Arrays.deepToString(as2)); - List[] al1 = array(Lists.list(1, 2), Lists.list()); + List[] al1 = array(list(1, 2), list()); List[] al2 = array(); assertEquals("[[1, 2], []]", Arrays.deepToString(al1)); assertEquals("[]", Arrays.deepToString(al2)); } + + @Test + @SuppressWarnings("javadoc") + public void testReverse() { + String[] empty = array(); + Integer[] i123 = array(1, 2, 3); + List[] list = array(list(1, 2), list()); + + String[] reverseEmpty = reverse(empty); + Integer[] reverseI123 = reverse(i123); + List[] reverseList = reverse(list); + + assertNotSame(empty, reverseEmpty); + assertNotSame(i123, reverseI123); + assertNotSame(list, reverseList); + + assertEquals(0, reverseEmpty.length); + assertEquals(3, reverseI123.length); + assertEquals(2, reverseList.length); + + assertEquals(3, (int)reverseI123[0]); + assertEquals(2, (int)reverseI123[1]); + assertEquals(1, (int)reverseI123[2]); + + assertEquals(list(), reverseList[0]); + assertEquals(list(1, 2), reverseList[1]); + + assertSame(i123[0], reverseI123[2]); + assertSame(i123[1], reverseI123[1]); + assertSame(i123[2], reverseI123[0]); + + assertSame(list[0], reverseList[1]); + assertSame(list[1], reverseList[0]); + } } diff --git a/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java b/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java index 5af06d728..f5e3fd114 100644 --- a/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java +++ b/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java @@ -13,6 +13,8 @@ package org.eclipse.escet.common.java; +import java.lang.reflect.Array; + /** Array helper methods. */ public class ArrayUtils { /** Constructor for the {@link ArrayUtils} class. */ @@ -31,4 +33,21 @@ public class ArrayUtils { public static T[] array(T... elems) { return elems; } + + /** + * Reverses the given arrow. + * + * @param The type of the elements of the array. + * @param array The array to reverse. Is not modified. + * @return The reverse array. + */ + public static T[] reverse(T[] array) { + int n = array.length; + @SuppressWarnings("unchecked") + T[] reversed = (T[])Array.newInstance(array.getClass().getComponentType(), n); + for (int i = 0; i < n; i++) { + reversed[n - i - 1] = array[i]; + } + return reversed; + } } -- GitLab From b36e3a872861b36b77dfb0ee4461005471443735 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Fri, 27 May 2022 19:39:55 +0200 Subject: [PATCH 2/8] #196 Add DCSH variable ordering heuristic. - Is for now based on graphs constructed from the original hyper-edges. - Could later create DMSs/hyper-edges based on the paper's approach. - Is for now based on total span. - Could later also adopt the WES metric. - Until we adopt the WES metric, the reverse orders are never chosen. - Reversing the order has no effect on the total span. --- .../datasynth/varorder/DcshVarOrderer.java | 37 +++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/DcshVarOrderer.java diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/DcshVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/DcshVarOrderer.java new file mode 100644 index 000000000..2aa7e8987 --- /dev/null +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/DcshVarOrderer.java @@ -0,0 +1,37 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2022 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.datasynth.varorder; + +import static org.eclipse.escet.common.java.Lists.list; + +/** + * DSM-based Cuthill-McKee/Sloan variable ordering Heuristic (DCSH). + * + *

+ * This algorithm is based on: Sam Lousberg, Sander Thuijsman and Michel Reniers, "DSM-based variable ordering heuristic + * for reduced computational effort of symbolic supervisor synthesis", IFAC-PapersOnLine, volume 53, issue 4, pages + * 429-436, 2020, doi:10.1016/j.ifacol.2021.04.058. + *

+ */ +public class DcshVarOrderer extends ChoiceVarOrderer { + /** Constructor for the {@link DcshVarOrderer} class. */ + public DcshVarOrderer() { + super("DCSH", list( // + new WeightedCuthillMcKeeVarOrderer(), // First algorithm. + new SloanVarOrderer(), // Second algorithm. + new ReverseVarOrderer(new WeightedCuthillMcKeeVarOrderer()), // Reverse first algorithm. + new ReverseVarOrderer(new SloanVarOrderer()) // Reverse second algorithm. + )); + } +} -- GitLab From d2d32292810dfaa305423122f7f1858d1d8d22b9 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Tue, 31 May 2022 21:49:21 +0200 Subject: [PATCH 3/8] #196 Add option to data-based synthesis tool for DCSH variable ordering. --- .../cif/datasynth/CifDataSynthesisApp.java | 2 + .../conversion/CifToSynthesisConverter.java | 5 ++ .../options/BddDcshVarOrderOption.java | 61 +++++++++++++++++++ 3 files changed, 68 insertions(+) create mode 100644 cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/options/BddDcshVarOrderOption.java diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisApp.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisApp.java index f2efe522b..371d64fe8 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisApp.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisApp.java @@ -28,6 +28,7 @@ import org.eclipse.escet.cif.cif2cif.RemoveIoDecls; import org.eclipse.escet.cif.datasynth.bdd.BddUtils; import org.eclipse.escet.cif.datasynth.conversion.CifToSynthesisConverter; import org.eclipse.escet.cif.datasynth.conversion.SynthesisToCifConverter; +import org.eclipse.escet.cif.datasynth.options.BddDcshVarOrderOption; import org.eclipse.escet.cif.datasynth.options.BddDebugMaxNodesOption; import org.eclipse.escet.cif.datasynth.options.BddDebugMaxPathsOption; import org.eclipse.escet.cif.datasynth.options.BddForceVarOrderOption; @@ -422,6 +423,7 @@ public class CifDataSynthesisApp extends Application { bddOpts.add(Options.getInstance(BddOutputOption.class)); bddOpts.add(Options.getInstance(BddOutputNamePrefixOption.class)); bddOpts.add(Options.getInstance(BddVariableOrderOption.class)); + bddOpts.add(Options.getInstance(BddDcshVarOrderOption.class)); bddOpts.add(Options.getInstance(BddForceVarOrderOption.class)); bddOpts.add(Options.getInstance(BddSlidingWindowVarOrderOption.class)); bddOpts.add(Options.getInstance(BddSlidingWindowSizeOption.class)); diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java index cb6428aab..373537fec 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java @@ -82,6 +82,7 @@ import org.eclipse.escet.cif.common.CifValueUtils; import org.eclipse.escet.cif.datasynth.bdd.BddUtils; import org.eclipse.escet.cif.datasynth.bdd.CifBddBitVector; import org.eclipse.escet.cif.datasynth.bdd.CifBddBitVectorAndCarry; +import org.eclipse.escet.cif.datasynth.options.BddDcshVarOrderOption; import org.eclipse.escet.cif.datasynth.options.BddDebugMaxNodesOption; import org.eclipse.escet.cif.datasynth.options.BddDebugMaxPathsOption; import org.eclipse.escet.cif.datasynth.options.BddForceVarOrderOption; @@ -96,6 +97,7 @@ import org.eclipse.escet.cif.datasynth.spec.SynthesisInputVariable; import org.eclipse.escet.cif.datasynth.spec.SynthesisLocPtrVariable; import org.eclipse.escet.cif.datasynth.spec.SynthesisTypedVariable; import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; +import org.eclipse.escet.cif.datasynth.varorder.DcshVarOrderer; import org.eclipse.escet.cif.datasynth.varorder.ForceVarOrderer; import org.eclipse.escet.cif.datasynth.varorder.SequentialVarOrderer; import org.eclipse.escet.cif.datasynth.varorder.SlidingWindowVarOrderer; @@ -896,6 +898,9 @@ public class CifToSynthesisConverter { // Get algorithms to apply. List orderers = list(); + if (BddDcshVarOrderOption.isEnabled()) { + orderers.add(new DcshVarOrderer()); + } if (BddForceVarOrderOption.isEnabled()) { orderers.add(new ForceVarOrderer()); } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/options/BddDcshVarOrderOption.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/options/BddDcshVarOrderOption.java new file mode 100644 index 000000000..75c321a2a --- /dev/null +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/options/BddDcshVarOrderOption.java @@ -0,0 +1,61 @@ +////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 2010, 2022 Contributors to the Eclipse Foundation +// +// See the NOTICE file(s) distributed with this work for additional +// information regarding copyright ownership. +// +// This program and the accompanying materials are made available +// under the terms of the MIT License which is available at +// https://opensource.org/licenses/MIT +// +// SPDX-License-Identifier: MIT +////////////////////////////////////////////////////////////////////////////// + +package org.eclipse.escet.cif.datasynth.options; + +import org.eclipse.escet.common.app.framework.options.BooleanOption; +import org.eclipse.escet.common.app.framework.options.Options; + +/** BDD DCSH variable ordering option. */ +public class BddDcshVarOrderOption extends BooleanOption { + /** Constructor for the {@link BddDcshVarOrderOption} class. */ + public BddDcshVarOrderOption() { + super( + // name + "BDD DCSH variable ordering algorithm", + + // description + "Whether to apply the DCSH variable ordering algorithm to improve the initial variable ordering " + + "(BOOL=yes), or not apply it (BOOL=no). [DEFAULT=no]", + + // cmdShort + null, + + // cmdLong + "dcsh-order", + + // cmdValue + "BOOL", + + // defaultValue + false, + + // showInDialog + true, + + // optDialogDescr + "Whether to apply the DCSH variable ordering algorithm to improve the initial variable ordering.", + + // optDialogLabelText + "Apply DCSH variable ordering algorithm"); + } + + /** + * Should the DCSH variable ordering algorithm be applied? + * + * @return {@code true} to apply the algorithm, {@code false} otherwise. + */ + public static boolean isEnabled() { + return Options.get(BddDcshVarOrderOption.class); + } +} -- GitLab From 04edb068247852b45e1f31697a96dc2bfd438e22 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Tue, 31 May 2022 22:59:57 +0200 Subject: [PATCH 4/8] #196 Data-based synthesis variable ordering documentation improvements. - Added DCSH algorithm/option. - Extended explanation of heuristic algorithms in general. - Extended explanation of when algorithms are not applied. - Extended descriptions of the FORCE and sliding window algorithms. --- .../asciidoc/tools/datasynth.asciidoc | 46 +++++++++++++++++-- 1 file changed, 42 insertions(+), 4 deletions(-) diff --git a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc index 9a9d8ef56..c5852b0a9 100644 --- a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc +++ b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc @@ -121,6 +121,10 @@ For more information, see the <> section below. The initial order of the boolean variables is determined by this option. For more information, see the <> section below. +* _BDD DCSH variable ordering algorithm_: CIF variables and automata are represented using one or more boolean variables. +The initial order of the boolean variables can be improved by enabling this option. +For more information, see the <> section below. + * _BDD FORCE variable ordering algorithm_: CIF variables and automata are represented using one or more boolean variables. The initial order of the boolean variables can be improved by enabling this option. For more information, see the <> section below. @@ -1099,26 +1103,52 @@ Manually specifying a custom order often requires specialist knowledge and can t Luckily, there are algorithms that can automatically compute a decent variable order. The algorithms all take an initial variable ordering, and try to improve it using a fast heuristic. -A better initial variable ordering may result in a better final variable ordering (a better local optimum), and may speed up the automatic variable ordering algorithm (reaching an optimum faster). +Some algorithms search for a local optimum. +A better initial variable ordering may then result in a better final variable ordering (a better local optimum), and may also speed up the automatic variable ordering algorithm itself (reaching an optimum faster). +Other algorithms search for a global optimum. +However, the algorithms are all based on heuristics. +The guarantees that they provide differ, but none of them guarantees that synthesis will actually be quicker. +In practice however, they typically do improve synthesis performance, especially for larger and more complex models. For the initial variable ordering, the CIF variables and location pointers may be arbitrarily interleaved. If an automatic variable ordering algorithm changes the initial order, no synthesis variables are interleaved, except for each old variable with its corresponding new variable. -The automatic variable ordering algorithms are not applied if the CIF model has less than two synthesis variables. -They are also not applied if the model has no guards, updates, or other predicates to use as input for the algorithms, i.e. there are no _hyperedges_ to which to apply the algorithms. +The automatic variable ordering algorithms are not applied if the CIF model has less than two synthesis variables, as with zero variables there is nothing to order, and with one variable there is only one possible order. +They are also not applied if the model has no guards, updates, or other predicates from which to derive relations between the variables. +Such relations are encoded in various representations, such as _hyper-edges_ and _graph edges_, and serve as input for the algorithms. +Without such information, the algorithms lack the required input to search for improved variable orders. The following algorithms are available: +* _DCSH_ ++ +The DCSH algorithm of <> is currently considered experimental. +It is therefore disabled by default, but can be enabled using the _BDD DCSH variable ordering algorithm_ option (see <> section above). ++ +The DCSH algorithm applies two algorithms, the Weighted Cuthill-McKee bandwidth-reducing algorithm and the Sloan profile/wavefront-reducing algorithm. +It chooses the best order out of the orders produced by these two algorithms as well as their reverse orders, based on the total span metric. +DCSH aims to find good global variable orders. + * _FORCE_ + The FORCE algorithm of <> is enabled by default, but can be disabled using the _BDD FORCE variable ordering algorithm_ option (see <> section above). + -At most 10 * ceil(log~e~(n)) iterations of the FORCE algorithm are performed, with `n` the number of current/old BDD/boolean variables. +The FORCE algorithm iteratively computes new variable orders by considering gravity-force-like relations between the variables. +Each new order is promoted as the new best order, if it is better than the current best order, based on the total span metric. +The iterative algorithm stops once a fixed point has been reached, or after at most 10 * ceil(log~e~(n)) iterations of the algorithm have been performed, with `n` the number of synthesis variables. +FORCE aims to optimize an existing variable order, but may get stuck in a local optimum. * _Sliding window_ + The sliding window algorithm is enabled by default, but can be disabled using the _BDD sliding window variable ordering algorithm_ option (see <> section above). + +The sliding window algorithm 'slides' over the variable order, from left to right, one variable at a time, using a fixed-length _window_. +A window is a part of the entire order. +For instance, for a variable order `a;b;c;d;e` and windows length 3, the window at index 0 would be `a;b;c`, at index 1 it would be `b;c;d`, and at index 2 it would be `c;d;e`. +For each window, it computes all possible variable permutations, and selects the best one based on the total span metric. +It then replaces the window by the best permutation of that window, before moving on to the next window. +The sliding window algorithm aims to locally optimize an existing variable order for each window. ++ The default maximum length of the window that is used is 4. The actual window may be smaller, if less than 4 variables and/or location pointers are present in the model. The maximum length of the window can be configured using the _BDD sliding window size_ option (see <> section above). @@ -1188,6 +1218,12 @@ The following <> have an effect on the performa | Better order for smaller BDD representations | Choose the best order, depends on the model, (reversed) model/sorted usually good choices, custom order allows for best performance +| Order +| BDD DCSH variable ordering algorithm +| <> +| Better order for smaller BDD representations +| Enable for automatic ordering + | Order | BDD FORCE variable ordering algorithm | <> @@ -1299,6 +1335,8 @@ The supervisor can then only guarantee safe, non-blocking behavior if the system * [[[aloul03,Aloul et al. (2003)]]] Fadi A. Aloul, Igor L. Markov and Karem A. Sakallah, "FORCE: A Fast and Easy-To-Implement Variable-Ordering Heuristic", In: Proceedings of the 13th ACM Great Lakes symposium on VLSI, pages 116-119, 2003, doi:link:https://doi.org/10.1145/764808.764839[10.1145/764808.764839] +* [[[lousberg20,Lousberg et al. (2020)]]] Sam Lousberg, Sander Thuijsman and Michel Reniers, "DSM-based variable ordering heuristic for reduced computational effort of symbolic supervisor synthesis", IFAC-PapersOnLine, volume 53, issue 4, pages 429-436, 2020, doi:link:https://doi.org/10.1016/j.ifacol.2021.04.058[10.1016/j.ifacol.2021.04.058] + * [[[minato96,Minato (1996)]]] Shin-ichi Minato, "Binary Decision Diagrams and Applications for VLSI CAD", The Kluwer International Series in Engineering and Computer Science, volume 342, Springer, 1996, doi:link:https://doi.org/10.1007/978-1-4613-1303-8[10.1007/978-1-4613-1303-8] * [[[ouedraogo11,Ouedraogo et al. (2011)]]] Lucien Ouedraogo, Ratnesh Kumar, Robi Malik and Knut Åkesson, "Nonblocking and Safe Control of Discrete-Event Systems Modeled as Extended Finite Automata", IEEE Transactions on Automation Science and Engineering, volume 8, issue 3, pages 560-569, 2011, doi:link:https://doi.org/10.1109/TASE.2011.2124457[10.1109/TASE.2011.2124457] -- GitLab From 0dbe7508c70ae39a858b21b9a27709fc4f5a6d29 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Sat, 18 Jun 2022 13:50:34 +0200 Subject: [PATCH 5/8] #196 Data-synthesis variable ordering documentation improvements. --- .../asciidoc/tools/datasynth.asciidoc | 33 +++++++++++-------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc index c5852b0a9..97bad42db 100644 --- a/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc +++ b/cif/org.eclipse.escet.cif.documentation/asciidoc/tools/datasynth.asciidoc @@ -1115,39 +1115,46 @@ If an automatic variable ordering algorithm changes the initial order, no synthe The automatic variable ordering algorithms are not applied if the CIF model has less than two synthesis variables, as with zero variables there is nothing to order, and with one variable there is only one possible order. They are also not applied if the model has no guards, updates, or other predicates from which to derive relations between the variables. -Such relations are encoded in various representations, such as _hyper-edges_ and _graph edges_, and serve as input for the algorithms. -Without such information, the algorithms lack the required input to search for improved variable orders. +Without such relations, the algorithms lack the required input to search for improved variable orders. -The following algorithms are available: +The variable relations serve as input for the algorithms. +Different algorithms may use different representations of the variable relations, such as _hyper-edges_ or _graph edges_. +Further information about these representations may be obtained by enabling <>. + +The following variable ordering algorithms are available: * _DCSH_ + -The DCSH algorithm of <> is currently considered experimental. -It is therefore disabled by default, but can be enabled using the _BDD DCSH variable ordering algorithm_ option (see <> section above). +The DCSH algorithm of <> aims to find good global variable orders. ++ +DCSH applies two algorithms, the Weighted Cuthill-McKee bandwidth-reducing algorithm and the Sloan profile/wavefront-reducing algorithm. +It then chooses the best order out of the orders produced by these two algorithms as well as their reverse orders, based on the total span metric. + -The DCSH algorithm applies two algorithms, the Weighted Cuthill-McKee bandwidth-reducing algorithm and the Sloan profile/wavefront-reducing algorithm. -It chooses the best order out of the orders produced by these two algorithms as well as their reverse orders, based on the total span metric. -DCSH aims to find good global variable orders. +The DCSH algorithm is currently considered experimental. +It is therefore disabled by default, but can be enabled using the _BDD DCSH variable ordering algorithm_ option (see <> section above). * _FORCE_ + -The FORCE algorithm of <> is enabled by default, but can be disabled using the _BDD FORCE variable ordering algorithm_ option (see <> section above). +The FORCE algorithm of <> aims to optimize an existing variable order, but may get stuck in a local optimum. + -The FORCE algorithm iteratively computes new variable orders by considering gravity-force-like relations between the variables. +FORCE iteratively computes new variable orders by considering relations between the variables. +Conceptually, highly related variables 'pull' each other closer with more force than less related variables do. Each new order is promoted as the new best order, if it is better than the current best order, based on the total span metric. The iterative algorithm stops once a fixed point has been reached, or after at most 10 * ceil(log~e~(n)) iterations of the algorithm have been performed, with `n` the number of synthesis variables. -FORCE aims to optimize an existing variable order, but may get stuck in a local optimum. ++ +The FORCE algorithm is enabled by default, but can be disabled using the _BDD FORCE variable ordering algorithm_ option (see <> section above). * _Sliding window_ + -The sliding window algorithm is enabled by default, but can be disabled using the _BDD sliding window variable ordering algorithm_ option (see <> section above). +The sliding window algorithm aims to locally optimize an existing variable order for each window. + The sliding window algorithm 'slides' over the variable order, from left to right, one variable at a time, using a fixed-length _window_. A window is a part of the entire order. For instance, for a variable order `a;b;c;d;e` and windows length 3, the window at index 0 would be `a;b;c`, at index 1 it would be `b;c;d`, and at index 2 it would be `c;d;e`. For each window, it computes all possible variable permutations, and selects the best one based on the total span metric. It then replaces the window by the best permutation of that window, before moving on to the next window. -The sliding window algorithm aims to locally optimize an existing variable order for each window. ++ +The sliding window algorithm is enabled by default, but can be disabled using the _BDD sliding window variable ordering algorithm_ option (see <> section above). + The default maximum length of the window that is used is 4. The actual window may be smaller, if less than 4 variables and/or location pointers are present in the model. -- GitLab From 1fb99508ce0b28e437a8fcfd74f645221007afe5 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Sat, 18 Jun 2022 14:11:53 +0200 Subject: [PATCH 6/8] #196 Use List instead of SynthesisVariable[]. - Required renaming some methods in VarOrdererHelper to avoid duplicate overloads after type erasure. - Some other methods in that class also renamed, for consistency. --- .../varorder/helper/VarOrdererHelperTest.java | 16 +++--- .../conversion/CifToSynthesisConverter.java | 12 ++--- .../datasynth/varorder/ChoiceVarOrderer.java | 10 ++-- .../datasynth/varorder/ForceVarOrderer.java | 12 ++--- .../datasynth/varorder/ReverseVarOrderer.java | 20 ++++---- .../varorder/SequentialVarOrderer.java | 6 +-- .../varorder/SlidingWindowVarOrderer.java | 16 +++--- .../datasynth/varorder/SloanVarOrderer.java | 10 ++-- .../cif/datasynth/varorder/VarOrderer.java | 6 ++- .../WeightedCuthillMcKeeVarOrderer.java | 10 ++-- .../varorder/helper/VarOrdererHelper.java | 51 ++++++++++--------- 11 files changed, 89 insertions(+), 80 deletions(-) diff --git a/cif/org.eclipse.escet.cif.datasynth/src-test/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelperTest.java b/cif/org.eclipse.escet.cif.datasynth/src-test/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelperTest.java index 9f43acd4d..f9e413d00 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src-test/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelperTest.java +++ b/cif/org.eclipse.escet.cif.datasynth/src-test/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelperTest.java @@ -18,6 +18,8 @@ import static org.eclipse.escet.cif.metamodel.java.CifConstructors.newIntType; import static org.eclipse.escet.cif.metamodel.java.CifConstructors.newSpecification; import static org.junit.Assert.assertSame; +import java.util.List; + import org.eclipse.escet.cif.datasynth.spec.SynthesisInputVariable; import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; import org.eclipse.escet.cif.metamodel.cif.Specification; @@ -53,13 +55,13 @@ public class VarOrdererHelperTest { // Reorder the variables. int[] newIndices = {0, 4, 1, 2, 3}; // For each variable in 'variables', its new 0-based index. VarOrdererHelper helper = new VarOrdererHelper(spec, variables); - SynthesisVariable[] ordered = helper.reorder(newIndices); // Invariant: ordered[newIndices[i]] == variables[i] + List ordered = helper.reorderForNewIndices(newIndices); - // Check the result. - assertSame(a, ordered[0]); - assertSame(c, ordered[1]); - assertSame(d, ordered[2]); - assertSame(e, ordered[3]); - assertSame(b, ordered[4]); + // Check the result. Invariant: ordered[newIndices[i]] == variables[i]. + assertSame(a, ordered.get(0)); + assertSame(c, ordered.get(1)); + assertSame(d, ordered.get(2)); + assertSame(e, ordered.get(3)); + assertSame(b, ordered.get(4)); } } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java index 373537fec..946bd9a71 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java @@ -959,20 +959,20 @@ public class CifToSynthesisConverter { dbg(); } VarOrderer orderer = (orderers.size() == 1) ? first(orderers) : new SequentialVarOrderer(orderers); - SynthesisVariable[] curOrder = synthAut.variables; - SynthesisVariable[] newOrder = orderer.order(helper, synthAut.variables, dbgEnabled, 1); + List curOrder = Arrays.asList(synthAut.variables); + List newOrder = orderer.order(helper, Arrays.asList(synthAut.variables), dbgEnabled, 1); // If the new order differs from the current order, reorder. - boolean orderChanged = !Arrays.equals(curOrder, newOrder); + boolean orderChanged = !curOrder.equals(newOrder); if (dbgEnabled) { dbg(); dbg("Variable order %schanged.", orderChanged ? "" : "un"); } if (orderChanged) { - Assert.areEqual(curOrder.length, newOrder.length); // Same length. - Assert.areEqual(list2set(Arrays.asList(curOrder)), list2set(Arrays.asList(newOrder))); // Same variables. - synthAut.variables = newOrder; + Assert.areEqual(curOrder.size(), newOrder.size()); // Same length. + Assert.areEqual(list2set(curOrder), list2set(newOrder)); // Same variables. + synthAut.variables = newOrder.toArray(n -> new SynthesisVariable[n]); for (int i = 0; i < synthAut.variables.length; i++) { synthAut.variables[i].group = i; } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java index 8e02f8e0b..5f4a1ab4e 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java @@ -49,8 +49,8 @@ public class ChoiceVarOrderer implements VarOrderer { } @Override - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, - int dbgLevel) + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) { // Debug output before applying the algorithms. if (dbgEnabled) { @@ -62,7 +62,7 @@ public class ChoiceVarOrderer implements VarOrderer { } // Initialize best order. - SynthesisVariable[] bestOrder = null; + List bestOrder = null; long bestSpan = Long.MAX_VALUE; // Apply each algorithm. @@ -74,10 +74,10 @@ public class ChoiceVarOrderer implements VarOrderer { // Apply algorithm. Each algorithm is independently applied to the input variable order. VarOrderer algorithm = algorithms.get(i); - SynthesisVariable[] algoOrder = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); + List algoOrder = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); // Update best order. - long algoSpan = helper.computeTotalSpan(algoOrder); + long algoSpan = helper.computeTotalSpanForVarOrder(algoOrder); if (algoSpan < bestSpan) { bestOrder = algoOrder; bestSpan = algoSpan; diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java index aab5a0cf2..caa2a7cda 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java @@ -36,11 +36,11 @@ import org.eclipse.escet.common.java.BitSets; */ public class ForceVarOrderer implements VarOrderer { @Override - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, + public List order(VarOrdererHelper helper, List inputOrder, boolean dbgEnabled, int dbgLevel) { // Get hyper-edges. - int varCnt = inputOrder.length; + int varCnt = inputOrder.size(); BitSet[] hyperEdges = helper.getHyperEdges(); // Debug output before applying the algorithm. @@ -72,7 +72,7 @@ public class ForceVarOrderer implements VarOrderer { // Initialize variable indices: for each variable (in their original order), its new 0-based index. int[] curIndices; // Current indices computed by the algorithm. int[] bestIndices; // Best indices computed by the algorithm. - curIndices = helper.getNewIndices(inputOrder); + curIndices = helper.getNewIndicesForVarOrder(inputOrder); bestIndices = curIndices.clone(); // Determine maximum number of iterations. @@ -83,7 +83,7 @@ public class ForceVarOrderer implements VarOrderer { } // Initialize total span. - long curTotalSpan = helper.computeTotalSpan(curIndices); + long curTotalSpan = helper.computeTotalSpanForNewIndices(curIndices); long bestTotalSpan = curTotalSpan; if (dbgEnabled) { helper.dbgTotalSpan(dbgLevel, curTotalSpan, "before"); @@ -125,7 +125,7 @@ public class ForceVarOrderer implements VarOrderer { } // Get new total span. - long newTotalSpan = helper.computeTotalSpan(curIndices); + long newTotalSpan = helper.computeTotalSpanForNewIndices(curIndices); if (dbgEnabled) { helper.dbgTotalSpan(dbgLevel, newTotalSpan, fmt("iteration %,d", curIter + 1)); } @@ -155,7 +155,7 @@ public class ForceVarOrderer implements VarOrderer { } // Return the best order. - return helper.reorder(bestIndices); + return helper.reorderForNewIndices(bestIndices); } /** diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java index 1a0d07606..87a337203 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java @@ -13,9 +13,11 @@ package org.eclipse.escet.cif.datasynth.varorder; +import java.util.Collections; +import java.util.List; + import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; -import org.eclipse.escet.common.java.ArrayUtils; /** Variable ordering algorithm that returns the reverse order of another algorithm. */ public class ReverseVarOrderer implements VarOrderer { @@ -32,27 +34,27 @@ public class ReverseVarOrderer implements VarOrderer { } @Override - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, - int dbgLevel) + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) { - // Debug output before applying the algorithms. + // Debug output before applying the algorithm. if (dbgEnabled) { helper.dbg(dbgLevel, "Applying algorithm, and reversing its result:"); } // Apply the algorithm. - SynthesisVariable[] order = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); + List order = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); // Reverse the order. - SynthesisVariable[] reverseOrder = ArrayUtils.reverse(order); + Collections.reverse(order); - // Debug output after applying the algorithms. + // Debug output after applying the algorithm. if (dbgEnabled) { helper.dbg(dbgLevel, "Reversed the variable order."); - helper.dbgTotalSpan(dbgLevel, reverseOrder, "reversed"); + helper.dbgTotalSpanForVarOrder(dbgLevel, order, "reversed"); } // Return the resulting variable order. - return reverseOrder; + return order; } } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SequentialVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SequentialVarOrderer.java index 9ef895652..3feaa69b2 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SequentialVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SequentialVarOrderer.java @@ -38,8 +38,8 @@ public class SequentialVarOrderer implements VarOrderer { } @Override - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, - int dbgLevel) + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) { // Debug output before applying the algorithms. if (dbgEnabled) { @@ -47,7 +47,7 @@ public class SequentialVarOrderer implements VarOrderer { } // Initialize variable order to the input variable order. - SynthesisVariable[] order = inputOrder; + List order = inputOrder; // Apply each algorithm, in order, to the result of the previous algorithm. for (int i = 0; i < algorithms.size(); i++) { diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java index b6a6e941a..11d7bef4e 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java @@ -15,6 +15,8 @@ package org.eclipse.escet.cif.datasynth.varorder; import static org.eclipse.escet.common.java.Strings.fmt; +import java.util.List; + import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; import org.eclipse.escet.common.java.PermuteUtils; @@ -34,11 +36,11 @@ public class SlidingWindowVarOrderer implements VarOrderer { } @Override - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, - int dbgLevel) + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) { // Get variable count. - int varCnt = inputOrder.length; + int varCnt = inputOrder.size(); // Debug output before applying the algorithm. if (dbgEnabled) { @@ -52,8 +54,8 @@ public class SlidingWindowVarOrderer implements VarOrderer { } // Initialize current indices and total span. - int[] curIndices = helper.getNewIndices(inputOrder); - long curSpan = helper.computeTotalSpan(curIndices); + int[] curIndices = helper.getNewIndicesForVarOrder(inputOrder); + long curSpan = helper.computeTotalSpanForNewIndices(curIndices); if (dbgEnabled) { helper.dbgTotalSpan(dbgLevel, curSpan, "before"); } @@ -73,7 +75,7 @@ public class SlidingWindowVarOrderer implements VarOrderer { for (int i = 0; i < windowPerms.length; i++) { int[] windowPerm = windowPerms[i]; System.arraycopy(windowPerm, 0, windowIndices, offset, length); - long windowSpan = helper.computeTotalSpan(windowIndices); + long windowSpan = helper.computeTotalSpanForNewIndices(windowIndices); if (windowSpan < curSpan) { curSpan = windowSpan; bestIdx = i; @@ -96,6 +98,6 @@ public class SlidingWindowVarOrderer implements VarOrderer { } // Return the resulting order. - return helper.reorder(curIndices); + return helper.reorderForNewIndices(curIndices); } } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SloanVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SloanVarOrderer.java index 426194cae..c05087cc3 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SloanVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SloanVarOrderer.java @@ -28,8 +28,8 @@ import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; */ public class SloanVarOrderer implements VarOrderer { @Override - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, - int dbgLevel) + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) { // Get graph. Graph graph = helper.getGraph(); @@ -37,7 +37,7 @@ public class SloanVarOrderer implements VarOrderer { // Debug output before applying the algorithm. if (dbgEnabled) { helper.dbg(dbgLevel, "Applying Sloan algorithm."); - helper.dbgTotalSpan(dbgLevel, inputOrder, "before"); + helper.dbgTotalSpanForVarOrder(dbgLevel, inputOrder, "before"); } // Apply algorithm. @@ -45,10 +45,10 @@ public class SloanVarOrderer implements VarOrderer { // Debug output after applying the algorithm. if (dbgEnabled) { - helper.dbgTotalSpan(dbgLevel, order, "after"); + helper.dbgTotalSpanForNodeOrder(dbgLevel, order, "after"); } // Return the resulting order. - return helper.reorder(order); + return helper.reorderForNodeOrder(order); } } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/VarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/VarOrderer.java index cf004453c..6e487a831 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/VarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/VarOrderer.java @@ -13,6 +13,8 @@ package org.eclipse.escet.cif.datasynth.varorder; +import java.util.List; + import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; @@ -32,6 +34,6 @@ public interface VarOrderer { * @param dbgLevel The debug indentation level. * @return The new variable order, as produced by the algorithm. */ - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, - int dbgLevel); + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel); } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/WeightedCuthillMcKeeVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/WeightedCuthillMcKeeVarOrderer.java index 93779185d..7acfddb93 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/WeightedCuthillMcKeeVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/WeightedCuthillMcKeeVarOrderer.java @@ -28,8 +28,8 @@ import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; */ public class WeightedCuthillMcKeeVarOrderer implements VarOrderer { @Override - public SynthesisVariable[] order(VarOrdererHelper helper, SynthesisVariable[] inputOrder, boolean dbgEnabled, - int dbgLevel) + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) { // Get graph. Graph graph = helper.getGraph(); @@ -37,7 +37,7 @@ public class WeightedCuthillMcKeeVarOrderer implements VarOrderer { // Debug output before applying the algorithm. if (dbgEnabled) { helper.dbg(dbgLevel, "Applying Weighted Cuthill-McKee algorithm."); - helper.dbgTotalSpan(dbgLevel, inputOrder, "before"); + helper.dbgTotalSpanForVarOrder(dbgLevel, inputOrder, "before"); } // Apply algorithm. @@ -45,10 +45,10 @@ public class WeightedCuthillMcKeeVarOrderer implements VarOrderer { // Debug output after applying the algorithm. if (dbgEnabled) { - helper.dbgTotalSpan(dbgLevel, order, "after"); + helper.dbgTotalSpanForNodeOrder(dbgLevel, order, "after"); } // Return the resulting order. - return helper.reorder(order); + return helper.reorderForNodeOrder(order); } } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelper.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelper.java index da2e9cfdd..32108b17a 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelper.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/helper/VarOrdererHelper.java @@ -16,6 +16,7 @@ package org.eclipse.escet.cif.datasynth.varorder.helper; import static org.eclipse.escet.common.java.Maps.mapc; import static org.eclipse.escet.common.java.Pair.pair; +import java.util.Arrays; import java.util.BitSet; import java.util.List; import java.util.Map; @@ -172,9 +173,9 @@ public class VarOrdererHelper { * @param order The variable order. * @return The total span. */ - public long computeTotalSpan(SynthesisVariable[] order) { - int[] newIndices = getNewIndices(order); - return computeTotalSpan(newIndices); + public long computeTotalSpanForVarOrder(List order) { + int[] newIndices = getNewIndicesForVarOrder(order); + return computeTotalSpanForNewIndices(newIndices); } /** @@ -183,9 +184,9 @@ public class VarOrdererHelper { * @param order The node order. * @return The total span. */ - public long computeTotalSpan(List order) { - int[] newIndices = getNewIndices(order); - return computeTotalSpan(newIndices); + public long computeTotalSpanForNodeOrder(List order) { + int[] newIndices = getNewIndicesForNodeOrder(order); + return computeTotalSpanForNewIndices(newIndices); } /** @@ -194,7 +195,7 @@ public class VarOrdererHelper { * @param newIndices For each variable, its new 0-based index. * @return The total span. */ - public long computeTotalSpan(int[] newIndices) { + public long computeTotalSpanForNewIndices(int[] newIndices) { // Total span is the sum of the span of the edges. long totalSpan = 0; for (BitSet edge: hyperEdges) { @@ -221,9 +222,9 @@ public class VarOrdererHelper { * @param order The variable order. * @param annotation A human-readable text indicating the reason for printing the total span. */ - public void dbgTotalSpan(int dbgLevel, SynthesisVariable[] order, String annotation) { - int[] newIndices = getNewIndices(order); - dbgTotalSpan(dbgLevel, newIndices, annotation); + public void dbgTotalSpanForVarOrder(int dbgLevel, List order, String annotation) { + int[] newIndices = getNewIndicesForVarOrder(order); + dbgTotalSpanForNewIndices(dbgLevel, newIndices, annotation); } /** @@ -233,9 +234,9 @@ public class VarOrdererHelper { * @param order The node order. * @param annotation A human-readable text indicating the reason for printing the total span. */ - public void dbgTotalSpan(int dbgLevel, List order, String annotation) { - int[] newIndices = getNewIndices(order); - dbgTotalSpan(dbgLevel, newIndices, annotation); + public void dbgTotalSpanForNodeOrder(int dbgLevel, List order, String annotation) { + int[] newIndices = getNewIndicesForNodeOrder(order); + dbgTotalSpanForNewIndices(dbgLevel, newIndices, annotation); } /** @@ -245,8 +246,8 @@ public class VarOrdererHelper { * @param newIndices For each variable, its new 0-based index. * @param annotation A human-readable text indicating the reason for printing the total span. */ - public void dbgTotalSpan(int dbgLevel, int[] newIndices, String annotation) { - long totalSpan = computeTotalSpan(newIndices); + public void dbgTotalSpanForNewIndices(int dbgLevel, int[] newIndices, String annotation) { + long totalSpan = computeTotalSpanForNewIndices(newIndices); dbgTotalSpan(dbgLevel, totalSpan, annotation); } @@ -268,10 +269,10 @@ public class VarOrdererHelper { * @param order The new variable order. * @return For each variable, its new 0-based index. */ - public int[] getNewIndices(SynthesisVariable[] order) { - int[] newIndices = new int[order.length]; - for (int i = 0; i < order.length; i++) { - newIndices[origIndices.get(order[i])] = i; + public int[] getNewIndicesForVarOrder(List order) { + int[] newIndices = new int[order.size()]; + for (int i = 0; i < order.size(); i++) { + newIndices[origIndices.get(order.get(i))] = i; } return newIndices; } @@ -282,7 +283,7 @@ public class VarOrdererHelper { * @param order The new node order. * @return For each variable/node, its new 0-based index. */ - public int[] getNewIndices(List order) { + public int[] getNewIndicesForNodeOrder(List order) { int[] newIndices = new int[order.size()]; for (int i = 0; i < order.size(); i++) { newIndices[order.get(i).index] = i; @@ -296,9 +297,9 @@ public class VarOrdererHelper { * @param order The new variable/node order. * @return The synthesis variables, in their new order. */ - public SynthesisVariable[] reorder(List order) { - int[] varOrder = getNewIndices(order); - return reorder(varOrder); + public List reorderForNodeOrder(List order) { + int[] varOrder = getNewIndicesForNodeOrder(order); + return reorderForNewIndices(varOrder); } /** @@ -307,12 +308,12 @@ public class VarOrdererHelper { * @param newIndices For each variable, its new 0-based index. * @return The synthesis variables, in their new order. */ - public SynthesisVariable[] reorder(int[] newIndices) { + public List reorderForNewIndices(int[] newIndices) { Assert.areEqual(variables.length, newIndices.length); SynthesisVariable[] result = new SynthesisVariable[variables.length]; for (int i = 0; i < newIndices.length; i++) { result[newIndices[i]] = variables[i]; } - return result; + return Arrays.asList(result); } } -- GitLab From 9d4a9abd8b2052f86710a6ad620c80c117fe0235 Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Sat, 18 Jun 2022 14:12:14 +0200 Subject: [PATCH 7/8] #196 Removed ArrayUtils.reverse. --- .../escet/common/java/ArrayUtilsTest.java | 37 ------------------- .../eclipse/escet/common/java/ArrayUtils.java | 19 ---------- 2 files changed, 56 deletions(-) diff --git a/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java b/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java index 12a608069..abac8da04 100644 --- a/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java +++ b/common/org.eclipse.escet.common.java/src-test/org/eclipse/escet/common/java/ArrayUtilsTest.java @@ -14,11 +14,8 @@ package org.eclipse.escet.common.java; import static org.eclipse.escet.common.java.ArrayUtils.array; -import static org.eclipse.escet.common.java.ArrayUtils.reverse; import static org.eclipse.escet.common.java.Lists.list; import static org.junit.Assert.assertEquals; -import static org.junit.Assert.assertNotSame; -import static org.junit.Assert.assertSame; import java.util.Arrays; import java.util.List; @@ -48,38 +45,4 @@ public class ArrayUtilsTest { assertEquals("[[1, 2], []]", Arrays.deepToString(al1)); assertEquals("[]", Arrays.deepToString(al2)); } - - @Test - @SuppressWarnings("javadoc") - public void testReverse() { - String[] empty = array(); - Integer[] i123 = array(1, 2, 3); - List[] list = array(list(1, 2), list()); - - String[] reverseEmpty = reverse(empty); - Integer[] reverseI123 = reverse(i123); - List[] reverseList = reverse(list); - - assertNotSame(empty, reverseEmpty); - assertNotSame(i123, reverseI123); - assertNotSame(list, reverseList); - - assertEquals(0, reverseEmpty.length); - assertEquals(3, reverseI123.length); - assertEquals(2, reverseList.length); - - assertEquals(3, (int)reverseI123[0]); - assertEquals(2, (int)reverseI123[1]); - assertEquals(1, (int)reverseI123[2]); - - assertEquals(list(), reverseList[0]); - assertEquals(list(1, 2), reverseList[1]); - - assertSame(i123[0], reverseI123[2]); - assertSame(i123[1], reverseI123[1]); - assertSame(i123[2], reverseI123[0]); - - assertSame(list[0], reverseList[1]); - assertSame(list[1], reverseList[0]); - } } diff --git a/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java b/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java index f5e3fd114..5af06d728 100644 --- a/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java +++ b/common/org.eclipse.escet.common.java/src/org/eclipse/escet/common/java/ArrayUtils.java @@ -13,8 +13,6 @@ package org.eclipse.escet.common.java; -import java.lang.reflect.Array; - /** Array helper methods. */ public class ArrayUtils { /** Constructor for the {@link ArrayUtils} class. */ @@ -33,21 +31,4 @@ public class ArrayUtils { public static T[] array(T... elems) { return elems; } - - /** - * Reverses the given arrow. - * - * @param The type of the elements of the array. - * @param array The array to reverse. Is not modified. - * @return The reverse array. - */ - public static T[] reverse(T[] array) { - int n = array.length; - @SuppressWarnings("unchecked") - T[] reversed = (T[])Array.newInstance(array.getClass().getComponentType(), n); - for (int i = 0; i < n; i++) { - reversed[n - i - 1] = array[i]; - } - return reversed; - } } -- GitLab From 6bec5e75981813f2f06947d943f67ded398a6f6f Mon Sep 17 00:00:00 2001 From: Dennis Hendriks Date: Mon, 20 Jun 2022 10:46:39 +0200 Subject: [PATCH 8/8] #196 Explain 'best' in variable ordering algorithm comments. --- .../datasynth/CifDataSynthesisPlantsRefsReqsChecker.java | 4 ++-- .../escet/cif/datasynth/varorder/ChoiceVarOrderer.java | 4 ++-- .../escet/cif/datasynth/varorder/ForceVarOrderer.java | 6 +++--- .../cif/datasynth/varorder/SlidingWindowVarOrderer.java | 4 ++-- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisPlantsRefsReqsChecker.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisPlantsRefsReqsChecker.java index 9f8eaedef..cd89fed25 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisPlantsRefsReqsChecker.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisPlantsRefsReqsChecker.java @@ -219,8 +219,8 @@ public class CifDataSynthesisPlantsRefsReqsChecker { // Check equations. for (Equation equation: loc.getEquations()) { if (referencesReq(equation.getValue())) { - warn("Plant equation \"%s\" in %s references requirement state.", - equationToStr(equation), getLocationText2(loc)); + warn("Plant equation \"%s\" in %s references requirement state.", equationToStr(equation), + getLocationText2(loc)); } } diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java index 5f4a1ab4e..7479b6a4c 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ChoiceVarOrderer.java @@ -61,7 +61,7 @@ public class ChoiceVarOrderer implements VarOrderer { } } - // Initialize best order. + // Initialize best order (with lowest span). List bestOrder = null; long bestSpan = Long.MAX_VALUE; @@ -76,7 +76,7 @@ public class ChoiceVarOrderer implements VarOrderer { VarOrderer algorithm = algorithms.get(i); List algoOrder = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); - // Update best order. + // Update best order (with lowest span). long algoSpan = helper.computeTotalSpanForVarOrder(algoOrder); if (algoSpan < bestSpan) { bestOrder = algoOrder; diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java index caa2a7cda..4035bdac8 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ForceVarOrderer.java @@ -36,8 +36,8 @@ import org.eclipse.escet.common.java.BitSets; */ public class ForceVarOrderer implements VarOrderer { @Override - public List order(VarOrdererHelper helper, List inputOrder, boolean dbgEnabled, - int dbgLevel) + public List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) { // Get hyper-edges. int varCnt = inputOrder.size(); @@ -139,7 +139,7 @@ public class ForceVarOrderer implements VarOrderer { break; } - // Update best order, if new order is better than the current best order. + // Update best order, if new order is better than the current best order (has lower total span). if (newTotalSpan < bestTotalSpan) { System.arraycopy(curIndices, 0, bestIndices, 0, varCnt); bestTotalSpan = newTotalSpan; diff --git a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java index 11d7bef4e..d99fe2118 100644 --- a/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/SlidingWindowVarOrderer.java @@ -76,13 +76,13 @@ public class SlidingWindowVarOrderer implements VarOrderer { int[] windowPerm = windowPerms[i]; System.arraycopy(windowPerm, 0, windowIndices, offset, length); long windowSpan = helper.computeTotalSpanForNewIndices(windowIndices); - if (windowSpan < curSpan) { + if (windowSpan < curSpan) { // Check for better order (with lower total span). curSpan = windowSpan; bestIdx = i; } } - // Update order if improved by this window. + // Update order if improved by this window (has lower total span). if (bestIdx >= 0) { System.arraycopy(windowPerms[bestIdx], 0, curIndices, offset, length); -- GitLab