Commit 2574b3ad authored by Dennis Hendriks's avatar Dennis Hendriks
Browse files

Merge branch '362-upgrade-to-javabdd-3-0-0' into 'develop'

#362 Upgrade to JavaBDD 3.0.0

Closes #362

See merge request !313
parents d2b2d9ae 2d4edc2d
Pipeline #3885 passed with stage
in 0 seconds
......@@ -22,7 +22,7 @@ Require-Bundle: org.eclipse.escet.common.app.framework;bundle-version="0.6.0",
org.eclipse.escet.common.emf;bundle-version="0.6.0",
org.eclipse.escet.cif.cif2cif;bundle-version="0.6.0",
org.eclipse.escet.common.box;bundle-version="0.6.0",
com.github.javabdd;bundle-version="2.0.0"
com.github.javabdd;bundle-version="3.0.0"
Export-Package: org.eclipse.escet.cif.datasynth,
org.eclipse.escet.cif.datasynth.bdd,
org.eclipse.escet.cif.datasynth.conversion,
......
......@@ -68,10 +68,10 @@ import org.eclipse.escet.common.app.framework.output.OutputMode;
import org.eclipse.escet.common.app.framework.output.OutputModeOption;
import org.eclipse.escet.common.app.framework.output.OutputProvider;
import org.eclipse.escet.common.box.GridBox;
import org.eclipse.escet.common.java.Assert;
import com.github.javabdd.BDDFactory;
import com.github.javabdd.BDDFactory.CacheStats;
import com.github.javabdd.BDDFactory.ContinuousStats;
import com.github.javabdd.JFactory;
/** CIF data-based supervisory controller synthesis application. */
......@@ -223,17 +223,17 @@ public class CifDataSynthesisApp extends Application<IOutputComponent> {
Set<SynthesisStatistics> stats = SynthesisStatisticsOption.getStatistics();
boolean doGcStats = stats.contains(SynthesisStatistics.BDD_GC_COLLECT);
boolean doResizeStats = stats.contains(SynthesisStatistics.BDD_GC_RESIZE);
BddUtils.setBddCallbacks(factory, doGcStats, doResizeStats);
boolean doContinuousPerformanceStats = stats.contains(SynthesisStatistics.BDD_PERF_CONT);
List<Long> continuousOpMisses = list();
List<Integer> continuousUsedBddNodes = list();
BddUtils.registerBddCallbacks(factory, doGcStats, doResizeStats, doContinuousPerformanceStats,
continuousOpMisses, continuousUsedBddNodes);
boolean doCacheStats = stats.contains(SynthesisStatistics.BDD_PERF_CACHE);
boolean doContinuousPerformanceStats = stats.contains(SynthesisStatistics.BDD_PERF_CONT);
boolean doMaxBddNodesStats = stats.contains(SynthesisStatistics.BDD_PERF_MAX_NODES);
if (doCacheStats || doContinuousPerformanceStats) {
factory.getCacheStats().enableMeasurements();
}
if (doContinuousPerformanceStats) {
factory.getContinuousStats().enableMeasurements();
}
if (doMaxBddNodesStats) {
factory.getMaxUsedBddNodesStats().enableMeasurements();
}
......@@ -299,7 +299,7 @@ public class CifDataSynthesisApp extends Application<IOutputComponent> {
printBddCacheStats(factory.getCacheStats());
}
if (doContinuousPerformanceStats) {
printBddContinuousPerformanceStats(factory.getContinuousStats());
printBddContinuousPerformanceStats(continuousOpMisses, continuousUsedBddNodes);
}
if (doMaxBddNodesStats) {
out(fmt("Maximum used BDD nodes: %d.", factory.getMaxUsedBddNodesStats().getMaxUsedBddNodes()));
......@@ -371,13 +371,13 @@ public class CifDataSynthesisApp extends Application<IOutputComponent> {
/**
* Print the continuous BDD performance statistics to a file.
*
* @param stats The continuous BDD performance statistics to print.
* @param operationsSamples The collected continuous operation misses samples.
* @param nodesSamples The collected continuous used BDD nodes statistics samples.
*/
private void printBddContinuousPerformanceStats(ContinuousStats stats) {
// Collect the statistics.
List<Long> operations = stats.getOperationsStats();
List<Integer> nodes = stats.getNodesStats();
int numberOfDataPoints = nodes.size();
private void printBddContinuousPerformanceStats(List<Long> operationsSamples, List<Integer> nodesSamples) {
// Get number of data points.
Assert.areEqual(operationsSamples.size(), nodesSamples.size());
int numberOfDataPoints = operationsSamples.size();
// Get the file to print to.
String outPath = ContinuousPerformanceStatisticsFileOption.getPath();
......@@ -391,8 +391,8 @@ public class CifDataSynthesisApp extends Application<IOutputComponent> {
int lastNodes = -1;
for (int i = 0; i < numberOfDataPoints; i++) {
// Only print new data points.
long nextOperations = operations.get(i);
int nextNodes = nodes.get(i);
long nextOperations = operationsSamples.get(i);
int nextNodes = nodesSamples.get(i);
if (nextOperations != lastOperations || nextNodes != lastNodes) {
lastOperations = nextOperations;
lastNodes = nextNodes;
......
......@@ -18,7 +18,7 @@ import static org.eclipse.escet.common.app.framework.output.OutputProvider.doout
import static org.eclipse.escet.common.app.framework.output.OutputProvider.out;
import static org.eclipse.escet.common.java.Strings.fmt;
import java.lang.reflect.Method;
import java.util.List;
import org.eclipse.escet.cif.common.CifTextUtils;
import org.eclipse.escet.cif.datasynth.spec.SynthesisAutomaton;
......@@ -29,7 +29,6 @@ import com.github.javabdd.BDD;
import com.github.javabdd.BDDDomain;
import com.github.javabdd.BDDFactory;
import com.github.javabdd.BDDFactory.GCStats;
import com.github.javabdd.BDDFactory.ReorderStats;
/** BDD utility methods. */
public class BddUtils {
......@@ -111,83 +110,57 @@ public class BddUtils {
}
/**
* By default BDD factory callbacks print information to stdout/stderr. This method registers custom callbacks, that
* by default don't do anything. This prevents output being printed to stdout/stderr. If requested, the callbacks
* may print some statistics, using the application framework.
* If requested, register BDD factory callbacks that print some statistics.
*
* @param factory The BDD factory for which to override the default callbacks.
* @param factory The BDD factory for which to register the callbacks.
* @param doGcStats Whether to output BDD GC statistics.
* @param doResizeStats Whether to output BDD resize statistics.
* @param doContinuousPerformanceStats Whether to output continuous BDD performance statistics.
* @param continuousOpMisses The list into which to collect continuous operation misses samples.
* @param continuousUsedBddNodes The list into which to collect continuous used BDD nodes statistics samples.
*/
public static void setBddCallbacks(BDDFactory factory, boolean doGcStats, boolean doResizeStats) {
Class<?> cls = BddUtils.class;
Class<?>[] cbParams;
Method callback;
public static void registerBddCallbacks(BDDFactory factory, boolean doGcStats, boolean doResizeStats,
boolean doContinuousPerformanceStats, List<Long> continuousOpMisses, List<Integer> continuousUsedBddNodes)
{
// Register BDD garbage collection callback.
doGcStats = doGcStats && doout();
String gcMethodName = doGcStats ? "bddGcStatsCallback" : "bddGcNullCallback";
cbParams = new Class<?>[] {int.class, GCStats.class};
try {
callback = cls.getDeclaredMethod(gcMethodName, cbParams);
} catch (NoSuchMethodException | SecurityException e) {
throw new RuntimeException(e);
}
factory.registerGCCallback(null, callback);
// Register BDD variable reordering callback.
cbParams = new Class<?>[] {boolean.class, ReorderStats.class};
try {
callback = cls.getDeclaredMethod("bddReOrderNullCallback", cbParams);
} catch (NoSuchMethodException | SecurityException e) {
throw new RuntimeException(e);
if (doGcStats && doout()) {
factory.registerGcStatsCallback(BddUtils::bddGcStatsCallback);
}
factory.registerReorderCallback(null, callback);
// Register BDD internal node array resize callback.
doResizeStats = doResizeStats && doout();
String resizeMethodName = doResizeStats ? "bddResizeStatsCallback" : "bddResizeNullCallback";
cbParams = new Class<?>[] {int.class, int.class};
try {
callback = cls.getDeclaredMethod(resizeMethodName, cbParams);
} catch (NoSuchMethodException | SecurityException e) {
throw new RuntimeException(e);
if (doResizeStats && doout()) {
factory.registerResizeStatsCallback(BddUtils::bddResizeStatsCallback);
}
factory.registerResizeCallback(null, callback);
}
/**
* Callback invoked when the BDD library performs garbage collection on its internal data structures. Does not do
* anything.
*
* @param pre Whether the callback is invoked just before garbage collection ({@code 1}) or just after it
* ({@code 0}).
* @param stats The garbage collection statistics.
*/
public static void bddGcNullCallback(int pre, GCStats stats) {
// Callback that does nothing.
// Register continuous BDD performance statistics callback.
if (doContinuousPerformanceStats) {
factory.registerContinuousStatsCallback((n, o) -> {
continuousOpMisses.add(o);
continuousUsedBddNodes.add(n);
});
}
}
/**
* Callback invoked when the BDD library performs garbage collection on its internal data structures. Prints
* statistics.
*
* @param pre Whether the callback is invoked just before garbage collection ({@code 1}) or just after it
* ({@code 0}).
* @param stats The garbage collection statistics.
* @param pre Whether the callback is invoked just before garbage collection ({@code true}) or just after it
* ({@code false}).
*/
public static void bddGcStatsCallback(int pre, GCStats stats) {
private static void bddGcStatsCallback(GCStats stats, boolean pre) {
StringBuilder txt = new StringBuilder();
txt.append("BDD ");
txt.append((pre == 1) ? "pre " : "post");
txt.append(pre ? "pre " : "post");
txt.append(" garbage collection: #");
txt.append(fmt("%,d", stats.num + 1 - ((pre == 1) ? 0 : 1)));
txt.append(fmt("%,d", stats.num + 1 - (pre ? 0 : 1)));
txt.append(", ");
txt.append(fmt("%,13d", stats.freenodes));
txt.append(" of ");
txt.append(fmt("%,13d", stats.nodes));
txt.append(" nodes free");
if (pre == 0) {
if (!pre) {
txt.append(", ");
txt.append(fmt("%,13d", stats.time));
txt.append(" ms, ");
......@@ -197,34 +170,13 @@ public class BddUtils {
out(txt.toString());
}
/**
* Callback invoked when the BDD library performs variable reordering.
*
* @param pre Whether the callback is invoked just before variable reordering ({@code true}) or just after it
* ({@code false}).
* @param stats The variable reordering statistics.
*/
public static void bddReOrderNullCallback(boolean pre, ReorderStats stats) {
// Callback that does nothing.
}
/**
* Callback invoked when the BDD library resizes its internal node array. Does not do anything.
*
* @param oldSize The old size of the internal node array.
* @param newSize The new size of the internal node array.
*/
public static void bddResizeNullCallback(int oldSize, int newSize) {
// Callback that does nothing.
}
/**
* Callback invoked when the BDD library resizes its internal node array. Prints statistics.
*
* @param oldSize The old size of the internal node array.
* @param newSize The new size of the internal node array.
*/
public static void bddResizeStatsCallback(int oldSize, int newSize) {
private static void bddResizeStatsCallback(int oldSize, int newSize) {
out("BDD node table resize: from %,13d nodes to %,13d nodes", oldSize, newSize);
}
}
......@@ -34,7 +34,7 @@
<requires>
<import feature="org.eclipse.escet.common.feature" version="0.6.0.qualifier"/>
<import feature="org.eclipse.escet.setext.feature" version="0.6.0.qualifier"/>
<import feature="com.github.javabdd.feature" version="2.0.0.qualifier"/>
<import feature="com.github.javabdd.feature" version="3.0.0.qualifier"/>
<import plugin="org.apache.commons.io"/>
<import plugin="org.apache.commons.math3"/>
<import plugin="org.knowm.xchart"/>
......
......@@ -11,10 +11,10 @@
-->
<site>
<feature url="features/com.github.javabdd.feature_2.0.0.qualifier.jar" id="com.github.javabdd.feature" version="2.0.0.qualifier">
<feature url="features/com.github.javabdd.feature_3.0.0.qualifier.jar" id="com.github.javabdd.feature" version="3.0.0.qualifier">
<category name="org.eclipse.escet.thirdparty.category"/>
</feature>
<feature url="features/com.github.javabdd.feature.source_2.0.0.qualifier.jar" id="com.github.javabdd.feature.source" version="2.0.0.qualifier">
<feature url="features/com.github.javabdd.feature.source_3.0.0.qualifier.jar" id="com.github.javabdd.feature.source" version="3.0.0.qualifier">
<category name="org.eclipse.escet.thirdparty.category"/>
</feature>
<feature url="features/org.eclipse.escet.chi.feature_0.6.0.qualifier.jar" id="org.eclipse.escet.chi.feature" version="0.6.0.qualifier">
......
copyright=Copyright (c) 2001-2020 John Whaley and com.github.javabdd contributors
copyright=Copyright (c) 2001-2022 John Whaley and com.github.javabdd contributors
licenseURL=license.html
......
......@@ -2,7 +2,7 @@
<feature
id="com.github.javabdd.feature"
label="JavaBDD"
version="2.0.0.qualifier"
version="3.0.0.qualifier"
provider-name="Eclipse ESCET">
<description url="https://github.com/com-github-javabdd/com.github.javabdd">
......
......@@ -6,5 +6,5 @@
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry exported="true" kind="lib" path="lib/com.github.javabdd-2.0.0.jar" sourcepath="lib/com.github.javabdd-2.0.0-sources.jar"/>
<classpathentry exported="true" kind="lib" path="lib/com.github.javabdd-3.0.0.jar" sourcepath="lib/com.github.javabdd-3.0.0-sources.jar"/>
</classpath>
......@@ -2,10 +2,10 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: JavaBDD
Bundle-SymbolicName: com.github.javabdd;singleton:=true
Bundle-Version: 2.0.0.qualifier
Bundle-Version: 3.0.0.qualifier
Bundle-Vendor: Eclipse ESCET
Automatic-Module-Name: com.github.javabdd
Bundle-RequiredExecutionEnvironment: JavaSE-11
Bundle-ActivationPolicy: lazy
Bundle-ClassPath: lib/com.github.javabdd-2.0.0.jar
Bundle-ClassPath: lib/com.github.javabdd-3.0.0.jar
Export-Package: com.github.javabdd
......@@ -8,7 +8,7 @@
<body lang="EN-US">
<h2>About This Content</h2>
<p>October 30, 2021</p>
<p>April 28, 2022</p>
<h3>License</h3>
<p>
......@@ -44,9 +44,9 @@
<h4>JavaBDD</h4>
<p>
The Content includes JavaBDD 2.0.0, distributed by Maven Central
(<a href="https://search.maven.org/artifact/com.github.com-github-javabdd/com.github.javabdd/2.0.0/jar"
>https://search.maven.org/artifact/com.github.com-github-javabdd/com.github.javabdd/2.0.0/jar</a>).
The Content includes JavaBDD 3.0.0, distributed by Maven Central
(<a href="https://search.maven.org/artifact/com.github.com-github-javabdd/com.github.javabdd/3.0.0/jar"
>https://search.maven.org/artifact/com.github.com-github-javabdd/com.github.javabdd/3.0.0/jar</a>).
The JavaBDD source code can be found at GitHub
(<a href="https://github.com/com-github-javabdd/com.github.javabdd"
>https://github.com/com-github-javabdd/com.github.javabdd</a>).
......
bin.includes = META-INF/,\
lib/com.github.javabdd-2.0.0.jar,\
lib/com.github.javabdd-3.0.0.jar,\
about.html
src.includes = lib/com.github.javabdd-2.0.0-sources.jar,\
src.includes = lib/com.github.javabdd-3.0.0-sources.jar,\
about.html
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
File suppressed by a .gitattributes entry or the file's encoding is unsupported.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment