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 9f43acd4d20a6c9b22c4a1347c4ac924bf62e50d..f9e413d003fea566937c3c35054c5caefb42317f 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/CifDataSynthesisApp.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisApp.java index f2efe522bd9e33b5da0ce9d6d965b505ba7ee751..371d64fe897936e4e3f902b235a3e34d908145bf 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/CifDataSynthesisPlantsRefsReqsChecker.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/CifDataSynthesisPlantsRefsReqsChecker.java index 9f8eaedef8312c733d63f0367031575b68b5c92f..cd89fed259ad0e81b4b1448d8ff71c6f8ec93d99 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/conversion/CifToSynthesisConverter.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/conversion/CifToSynthesisConverter.java index cb6428aab5462451ca3544b7a15c7afe3c94fe0e..946bd9a710e1f96f10c9f203ca882698b5e75da1 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()); } @@ -954,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/options/BddDcshVarOrderOption.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/options/BddDcshVarOrderOption.java new file mode 100644 index 0000000000000000000000000000000000000000..75c321a2a13b4800234ec59323bbe5403a185672 --- /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); + } +} 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 0000000000000000000000000000000000000000..7479b6a4cd412d872b674e926c79b401858df6ff --- /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 List order(VarOrdererHelper helper, List 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 (with lowest span). + List 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); + List algoOrder = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); + + // Update best order (with lowest span). + long algoSpan = helper.computeTotalSpanForVarOrder(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/DcshVarOrderer.java b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/DcshVarOrderer.java new file mode 100644 index 0000000000000000000000000000000000000000..2aa7e89878fee701c8261a1d7810006c21f2137a --- /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. + )); + } +} 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 aab5a0cf20cf27b88849defd57d999aefc0a4018..4035bdac81ad74bebd909c5e2c81f362f7d39f57 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, - int dbgLevel) + 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)); } @@ -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; @@ -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 new file mode 100644 index 0000000000000000000000000000000000000000..87a3372034e10e4aab8bce9f7c1bdd52c4d2994b --- /dev/null +++ b/cif/org.eclipse.escet.cif.datasynth/src/org/eclipse/escet/cif/datasynth/varorder/ReverseVarOrderer.java @@ -0,0 +1,60 @@ +////////////////////////////////////////////////////////////////////////////// +// 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.Collections; +import java.util.List; + +import org.eclipse.escet.cif.datasynth.spec.SynthesisVariable; +import org.eclipse.escet.cif.datasynth.varorder.helper.VarOrdererHelper; + +/** 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 List order(VarOrdererHelper helper, List inputOrder, + boolean dbgEnabled, int dbgLevel) + { + // Debug output before applying the algorithm. + if (dbgEnabled) { + helper.dbg(dbgLevel, "Applying algorithm, and reversing its result:"); + } + + // Apply the algorithm. + List order = algorithm.order(helper, inputOrder, dbgEnabled, dbgLevel + 1); + + // Reverse the order. + Collections.reverse(order); + + // Debug output after applying the algorithm. + if (dbgEnabled) { + helper.dbg(dbgLevel, "Reversed the variable order."); + helper.dbgTotalSpanForVarOrder(dbgLevel, order, "reversed"); + } + + // Return the resulting variable order. + 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 9ef8956520e98d57c7a2254d44c506284401ccb8..3feaa69b2590c1493898eab8dd6856211afc5d2c 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 b6a6e941a3c774167fbd5a6a877c11e29aa2b140..d99fe211817aefa3ed33af7161e1449957340fbc 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,14 +75,14 @@ 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); - if (windowSpan < curSpan) { + long windowSpan = helper.computeTotalSpanForNewIndices(windowIndices); + 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); @@ -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 426194caed85545ad8e5c7e1b6b0dab7afc1b05d..c05087cc3ec3fd506a31e66c74b1974c99fc17fb 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 cf004453c318b2975ba68c849fd4fb678990a649..6e487a8314212c7e9fe1a8508ca0255325cef599 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 93779185d50d15866c360654dd03913c982d1257..7acfddb93ce859e70f94485c61cd518ec5884f2b 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 da2e9cfdd8eed0982e868ec4567cdd79b7a37549..32108b17a6fdf5cea66987d0b9eabdb51ff431f7 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); } } 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 9a9d8ef5683f9fb2a1d09a9f39457e1608e3fc02..97bad42db2bd6cf411aaa522f098e2ca4406d1d6 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,24 +1103,57 @@ 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. +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 <> 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 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. ++ +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. + -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 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 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 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. @@ -1188,6 +1225,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 +1342,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] 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 3e9acfb07ddf5a77a39e77f88669a4b2ebb5cf8a..abac8da041fc329a50a73a35079f5a583ec80f5c 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,6 +14,7 @@ package org.eclipse.escet.common.java; import static org.eclipse.escet.common.java.ArrayUtils.array; +import static org.eclipse.escet.common.java.Lists.list; import static org.junit.Assert.assertEquals; import java.util.Arrays; @@ -38,7 +39,7 @@ 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));