Commit be944d79 authored by Dennis Hendriks's avatar Dennis Hendriks
Browse files

Merge remote-tracking branch 'origin/develop' into

111-generate-railroad-diagrams-during-build-rather-than-committing-them-to-git-repo-4

Conflicts:
	releng/org.eclipse.escet.releng.tests/test-all.launch
parents 17e70e53 805e7457
......@@ -90,7 +90,7 @@ image::{ref-imgsdir}/distribution_plots/bernoulli.svg[]
Range:: `{false, true}`
Mean:: `p` (where `false` is interpreted as `0`, and `true` is interpreted as `1`)
Variance:: `1 - p` (where `false` is interpreted as `0`, and `true` is interpreted as `1`)
See also:: Bernoulli(p), <<ref-law>>, page 302
See also:: Bernoulli(p), <<ref-law07>>, page 302
* `dist` `int` *binomial*`(int n, real p)`
+
......@@ -100,7 +100,7 @@ Number of successes when performing `n` experiments `(n > 0)` with chance `p` `+
Range:: `+{0, 1, ..., n}+`
Mean:: `n * p`
Variance:: `n * p * (1 - p)`
See also:: bin(n, p), <<ref-law>>, page 304
See also:: bin(n, p), <<ref-law07>>, page 304
* `dist` `int` *geometric*`(real p)`
+
......@@ -110,7 +110,7 @@ Geometric distribution, number of failures before success for an experiment with
Range:: `+{0, 1, ...}+`
Mean:: `(1 - p) / p`
Variance:: `+(1 - p) / p^2+`
See also:: geom(p), <<ref-law>>, page 305
See also:: geom(p), <<ref-law07>>, page 305
* `dist` `int` *poisson*`(real lambda)`
+
......@@ -122,7 +122,7 @@ image::{ref-imgsdir}/distribution_plots/poisson.svg[]
Range:: `+{0, 1, ...}+`
Mean:: `lambda`
Variance:: `lambda`
See also:: Poison(lambda), <<ref-law>>, page 308
See also:: Poison(lambda), <<ref-law07>>, page 308
* `dist` `int` *uniform*`(int a, b)`
+
......@@ -134,7 +134,7 @@ image::{ref-imgsdir}/distribution_plots/disc_uni.svg[]
Range:: `+{a, a+1, ..., b-1}+`
Mean:: `+(a + b - 1) / 2+`
Variance:: `+((b - a)^2 - 1) / 12+`
See also:: DU(a, b - 1), <<ref-law>>, page 303
See also:: DU(a, b - 1), <<ref-law07>>, page 303
indexterm:[continuous distribution]
indexterm:[beta]
......@@ -161,7 +161,7 @@ image::{ref-imgsdir}/distribution_plots/beta.svg[]
Range:: `[0, 1]`
Mean:: `+p / (p + q)+`
Variance:: `+p * q / ((p + q)^2 * (p + q + 1))+`
See also:: Beta(p, q), <<ref-law>>, page 291
See also:: Beta(p, q), <<ref-law07>>, page 291
* `dist` `real` *erlang*`(double m, int k)`
+
......@@ -171,7 +171,7 @@ Equivalent to `gamma(k, m / k)`.
[horizontal]
Mean:: `m`
Variance:: `m * m / k`
See also:: ERL(m, k), <<ref-banks>>, page 153
See also:: ERL(m, k), <<ref-banks98>>, page 153
* `dist` `real` *exponential*`(real m)`
+
......@@ -183,7 +183,7 @@ image::{ref-imgsdir}/distribution_plots/exponential.svg[]
Range:: `[0, infinite)`
Mean:: `m`
Variance:: `m * m`
See also:: expo(m), <<ref-law>>, page 283
See also:: expo(m), <<ref-law07>>, page 283
* `dist` `real` *gamma*`(real a, b)`
+
......@@ -205,7 +205,7 @@ image::{ref-imgsdir}/distribution_plots/lognormal.svg[]
Range:: `[0, infinite)`
Mean:: `+exp(m + v2/2)+`
Variance:: `+exp(2*m + v2) * (exp(v2) - 1)+`
See also:: N(m, v2), <<ref-law>>, page 290
See also:: N(m, v2), <<ref-law07>>, page 290
* `dist` `real` *normal*`(real m, v2)`
+
......@@ -217,7 +217,7 @@ image::{ref-imgsdir}/distribution_plots/normal.svg[]
Range:: `(-infinite, infinite)`
Mean:: `m`
Variance:: `v2`
See also:: N(m, v2), <<ref-law>>, page 288
See also:: N(m, v2), <<ref-law07>>, page 288
* `dist` `real` *random*`()`
+
......@@ -238,7 +238,7 @@ image::{ref-imgsdir}/distribution_plots/triangle.svg[]
Range:: `[a, c]`
Mean:: `+(a + b + c) /3+`
Variance:: `+(a^2 + c^2 + b^2 - a*b - a*c - b*c) / 18+`
See also:: Triangle(a, c, b), <<ref-law>>, page 300
See also:: Triangle(a, c, b), <<ref-law07>>, page 300
* `dist` `real` *uniform*`(real a, b)`
+
......@@ -250,7 +250,7 @@ image::{ref-imgsdir}/distribution_plots/cont_uni.svg[]
Range:: `[a, b)`
Mean:: `+(a + b) / 2+`
Variance:: `+(b - a)^2 / 12+`
See also:: U(a,b), <<ref-law>>, page 282, except that distribution has an inclusive upper bound.
See also:: U(a,b), <<ref-law07>>, page 282, except that distribution has an inclusive upper bound.
* `dist` `real` *weibull*`(real a, b)`
+
......@@ -263,11 +263,11 @@ Range:: `[0, infinite)`
Mean:: `(b / a) * G(1 / a)`
Variance:: `+(b^2 / a) * (2 * G(2 / a) - (1 / a) * G(1 / a)^2)+` with `G(x)` the Gamma function,
`G(x)` `=` integral over `t` from `0` to `infinity`, for `+t^(x - 1) * exp(-t)+`
See also:: Weibull(a, b), <<ref-law>>, page 284
See also:: Weibull(a, b), <<ref-law07>>, page 284
[bibliography]
=== References
* [[[ref-banks,Banks]]] Jerry Banks, "Handbook of Simulation: Principles, Methodology, Advances, Applications, and Practice", John Wiley & Sons, Inc., 1998, doi:link:https://doi.org/10.1002/9780470172445[10.1002/9780470172445]
* [[[ref-banks98,Banks (1998)]]] Jerry Banks, "Handbook of Simulation: Principles, Methodology, Advances, Applications, and Practice", John Wiley & Sons, Inc., 1998, doi:link:https://doi.org/10.1002/9780470172445[10.1002/9780470172445]
* [[[ref-law,Law]]] Averill M. Law, "Simulation Modeling and Analysis", fourth edition, McGraw-Hill, 2007
* [[[ref-law07,Law (2007)]]] Averill M. Law, "Simulation Modeling and Analysis", fourth edition, McGraw-Hill, 2007
......@@ -109,7 +109,7 @@ image::{tut-imgsdir}/../reference-manual/distribution_plots/bernoulli.svg[]
Range:: `{false, true}`
Mean:: `p` (where `false` is interpreted as `0`, and `true` is interpreted as `1`)
Variance:: `1 - p` (where `false` is interpreted as `0`, and `true` is interpreted as `1`)
See also:: Bernoulli(p), <<tut-law>>, page 302
See also:: Bernoulli(p), <<tut-law07>>, page 302
* `dist` `int` *uniform*`(int a, b)`
+
......@@ -121,7 +121,7 @@ image::{tut-imgsdir}/../reference-manual/distribution_plots/disc_uni.svg[]
Range:: `+{a, a+1, ..., b-1}+`
Mean:: `(a + b - 1) / 2`
Variance:: `+((b - a)\^2 - 1) / 12+`
See also:: DU(a, b - 1), <<tut-law>>, page 303
See also:: DU(a, b - 1), <<tut-law07>>, page 303
indexterm:[distribution,continuous]
indexterm:[continuous,distribution]
......@@ -140,7 +140,7 @@ image::{tut-imgsdir}/../reference-manual/distribution_plots/cont_uni.svg[]
Range:: `[a, b)`
Mean:: `(a + b) / 2`
Variance:: `+(b - a)^2 / 12+`
See also:: U(a,b), <<tut-law>>, page 282, except that distribution has an
See also:: U(a,b), <<tut-law07>>, page 282, except that distribution has an
inclusive upper bound.
* `dist` `real` *gamma*`(real a, b)`
......@@ -156,7 +156,7 @@ Variance:: `+a * b^2+`
[bibliography]
==== References
* [[[tut-law,Law]]] Averill M. Law, "Simulation Modeling and Analysis", fourth edition, McGraw-Hill, 2007
* [[[tut-law07,Law (2007)]]] Averill M. Law, "Simulation Modeling and Analysis", fourth edition, McGraw-Hill, 2007
[[tut-simulating-stochastic-behavior]]
=== Simulating stochastic behavior
......
......@@ -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);
}
}
......@@ -23,7 +23,7 @@ Finite response assures that there are no loops consisting of controllable event
The assumption is that uncontrollable events are generated by the environment and the controller reacts to these with controllable events.
If the controller has finite response, the controller will only generate a finite number of controllable events, before it waits for new (uncontrollable) events from the environment.
The algorithm for finite response is based on <<reijnen>>.
The algorithm for finite response is based on <<reijnen19>>.
indexterm:[controller property checker,start]
......@@ -239,4 +239,4 @@ Alternatively, the <<tools-chapter-cif-explorer,CIF explorer>> may be used to ve
[bibliography]
=== References
* [[[reijnen,Reijnen et al.]]] Ferdie F.H. Reijnen, Albert T. Hofkamp, Joanna M. van de Mortel-Fronczak, Michel A. Reniers and Jacobus E. Rooda, "Finite Response and Confluence of State-based Supervisory Controllers", In: Proceedings of the 15th International Conference on Automation Science and Engineering, pages 509-516, 2019, doi:link:https://doi.org/10.1109/COASE.2019.8843335[10.1109/COASE.2019.8843335]
* [[[reijnen19,Reijnen et al. (2019)]]] Ferdie F.H. Reijnen, Albert T. Hofkamp, Joanna M. van de Mortel-Fronczak, Michel A. Reniers and Jacobus E. Rooda, "Finite Response and Confluence of State-based Supervisory Controllers", In: Proceedings of the 15th International Conference on Automation Science and Engineering, pages 509-516, 2019, doi:link:https://doi.org/10.1109/COASE.2019.8843335[10.1109/COASE.2019.8843335]
......@@ -41,7 +41,7 @@ That is, the controlled system permits all safe, controllable, and non-blocking
Note that <<lang-tut-time-deadlock,deadlock>> is not prevented for marked states.
The synthesis algorithm is based on <<ouedraogo>>.
The synthesis algorithm is based on <<ouedraogo11>>.
indexterm:[data-based supervisory controller synthesis,start]
......@@ -878,7 +878,7 @@ This excludes the trivial cases where the cache is not checked.
Prints continuously collected platform and machine independent BDD performance related metrics.
+
This statistic continuously collects the platform and machine independent BDD performance metrics described in the table below.
These metrics are discussed in more detail in <<thuijsman>>.
These metrics are discussed in more detail in <<thuijsman19>>.
+
The information is printed to a CSV file that can be configured using the _Continuous performance statistics file_ <<tools-datasynth-options,option>>.
The file is written after execution, just before termination of the tool.
......@@ -904,7 +904,7 @@ The size of a BDD, expressed as the number of nodes used, is a platform and mach
Prints the maximum number of BDD nodes used during synthesis.
+
The size of a BDD, expressed as the number of nodes used, is a platform and machine independent measure of the amount of memory needed to store it.
This metric is discussed in more detail in <<thuijsman>>.
This metric is discussed in more detail in <<thuijsman19>>.
+
This metric is printed to the console, after execution, just before termination of the tool.
It prints the maximum number of BDD nodes used during synthesis.
......@@ -970,7 +970,7 @@ For the initial variable ordering, it is possible to order the BDD variables per
This can significantly influences the performance of synthesis.
Generally, strongly related synthesis variables should be interleaved.
For more information on ordering and its influence on performance, see Chapter 3 of <<minato>>.
For more information on ordering and its influence on performance, see Chapter 3 of <<minato96>>.
For each CIF variable and location pointer, two synthesis variables are created, one storing the old/current value (before a transition), and one storing the new value (after a transition).
For a single CIF variable or location pointer, the old and new synthesis variables are always kept together, and interleaved.
......@@ -1103,7 +1103,7 @@ The following algorithms are available:
* _FORCE_
+
The FORCE algorithm of <<aloul>> is enabled by default, but can be disabled using the _BDD FORCE variable ordering algorithm_ option (see <<tools-datasynth-options,options>> section above).
The FORCE algorithm of <<aloul03>> is enabled by default, but can be disabled using the _BDD FORCE variable ordering algorithm_ option (see <<tools-datasynth-options,options>> 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.
......@@ -1283,10 +1283,10 @@ The supervisor can then only guarantee safe, non-blocking behavior if the system
[bibliography]
=== References
* [[[aloul,Aloul et al.]]] 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]
* [[[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]
* [[[minato,Minato]]] 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]
* [[[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]
* [[[ouedraogo,Ouedraogo et al.]]] 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]
* [[[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]
* [[[thuijsman,Thuijsman et al.]]] Sander Thuijsman, Dennis Hendriks, Rolf Theunissen, Michel Reniers and Ramon Schiffelers, "Computational Effort of BDD-Based Supervisor Synthesis of Extended Finite Automata", In: Proceedings of the IEEE Conference on Automation Science and Engineering, pages 486-493, 2019, doi:link:https://doi.org/10.1109/COASE.2019.8843327[10.1109/COASE.2019.8843327]
* [[[thuijsman19,Thuijsman et al. (2019)]]] Sander Thuijsman, Dennis Hendriks, Rolf Theunissen, Michel Reniers and Ramon Schiffelers, "Computational Effort of BDD-Based Supervisor Synthesis of Extended Finite Automata", In: Proceedings of the IEEE Conference on Automation Science and Engineering, pages 486-493, 2019, doi:link:https://doi.org/10.1109/COASE.2019.8843327[10.1109/COASE.2019.8843327]
......@@ -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"/>
......
<?xml version="1.0" encoding="UTF-8"?>
<fileset-config file-format-version="1.2.0" simple-config="false" sync-formatter="false">
<local-check-config name="Eclipse ESCET Checkstyle" location="/org.eclipse.escet.releng.configuration/checkstyle.xml" type="project" description="Eclipse ESCET Checkstyle.
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">
<additional-data name="protect-config-file" value="false"/>
</local-check-config>
<fileset name="all" enabled="true" check-config-name="Eclipse ESCET Checkstyle" local="true">
<file-match-pattern match-pattern="^(src.*|asciidoc)/" include-pattern="true"/>
</fileset>
<filter name="NonSrcDirs" enabled="false"/>
</fileset-config>
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-11">
<attributes>
<attribute name="module" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="output" path="target/classes"/>
</classpath>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.eclipse.escet.common.dsm.app</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.ManifestBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.SchemaBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>net.sf.eclipsecs.core.CheckstyleBuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.pde.PluginNature</nature>
<nature>org.eclipse.jdt.core.javanature</nature>
<nature>net.sf.eclipsecs.core.CheckstyleNature</nature>
</natures>
</projectDescription>
eclipse.preferences.version=1
org.eclipse.jdt.core.builder.cleanOutputFolder=clean
org.eclipse.jdt.core.builder.duplicateResourceTask=warning
org.eclipse.jdt.core.builder.invalidClasspath=abort
org.eclipse.jdt.core.builder.recreateModifiedClassFileInOutputFolder=ignore
org.eclipse.jdt.core.builder.resourceCopyExclusionFilter=*.launch
org.eclipse.jdt.core.circularClasspath=error
org.eclipse.jdt.core.classpath.exclusionPatterns=enabled
org.eclipse.jdt.core.classpath.mainOnlyProjectHasTestOnlyDependency=error
org.eclipse.jdt.core.classpath.multipleOutputLocations=enabled
org.eclipse.jdt.core.classpath.outputOverlappingAnotherSource=error
org.eclipse.jdt.core.compiler.annotation.inheritNullAnnotations=disabled
org.eclipse.jdt.core.compiler.annotation.missingNonNullByDefaultAnnotation=ignore
org.eclipse.jdt.core.compiler.annotation.nonnull=org.eclipse.jdt.annotation.NonNull
org.eclipse.jdt.core.compiler.annotation.nonnull.secondary=
org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=org.eclipse.jdt.annotation.NonNullByDefault
org.eclipse.jdt.core.compiler.annotation.nonnullbydefault.secondary=
org.eclipse.jdt.core.compiler.annotation.nullable=org.eclipse.jdt.annotation.Nullable
org.eclipse.jdt.core.compiler.annotation.nullable.secondary=
org.eclipse.jdt.core.compiler.annotation.nullanalysis=disabled
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.methodParameters=generate
org.eclipse.jdt.core.compiler.codegen.targetPlatform=11
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=11
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
org.eclipse.jdt.core.compiler.doc.comment.support=enabled
org.eclipse.jdt.core.compiler.maxProblemPerUnit=100
org.eclipse.jdt.core.compiler.problem.APILeak=warning