escet merge requestshttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests2023-03-17T07:51:29Zhttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/534#364 Add swarm robotics CIF benchmark models.2023-03-17T07:51:29ZDennis Hendriks#364 Add swarm robotics CIF benchmark models.Addresses #364Addresses #364v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/524#364 Add themepark model as CIF benchmark model.2023-03-11T13:22:56ZDennis Hendriks#364 Add themepark model as CIF benchmark model.Addresses #364Addresses #364v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/834#364 Add wafer_scanner CIF benchmark model + generator2024-03-22T07:38:17ZDennis Hendriks#364 Add wafer_scanner CIF benchmark model + generator* Best to review per commit.
* Added:
* Generator to generate `wafer_scanner` benchmark models with n = 1-7 production wafers (besides 2 dummy wafers).
* Generated models for n = 1 and n = 2. The rest can be generated additionally.
...* Best to review per commit.
* Added:
* Generator to generate `wafer_scanner` benchmark models with n = 1-7 production wafers (besides 2 dummy wafers).
* Generated models for n = 1 and n = 2. The rest can be generated additionally.
* Benchmark script for n = 1 only, as that is currently difficult enough to synthesize, compared to the other benchmarks.
* Changes compared to original generator:
* Some things are in a slightly different order, due to use of ordered vs unordered sets/dicts/etc. But, for n = 1, the state spaces of the synthesized supervisors are language equivalent.
* Generated models had warnings due to having plants that refer to requirement state. The requirement is therefore split into a monitor and requirement, similar to what the synthesis tool now does under the hood. The original author agrees. The resulting supervisor state space for n = 1 is language equivalent to the one before this change.
* Other notes:
* Certain events are always disabled in the uncontrolled system or in the controlled system. This is by design. This is confirmed by the original author.
* The original first author is OK with contributing this to ESCET.
Addresses #364v3.0https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/354#364 CIF data-based synthesis performance test models: bridge2022-08-10T07:51:40ZFerdie Reijnen#364 CIF data-based synthesis performance test models: bridgeAddresses #364Addresses #364v0.7https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/355#364 CIF data-based synthesis performance test models: sudoku2022-08-10T19:46:21ZFerdie Reijnen#364 CIF data-based synthesis performance test models: sudokuAddresses #364Addresses #364v0.7https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/319#364 CIF data-based synthesis performance test models: water_lock2023-03-14T12:59:59ZFerdie Reijnen#364 CIF data-based synthesis performance test models: water_lockAddresses #364Addresses #364v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/317#364 CIF data-based synthesis performance test models: wizard + festo2022-05-19T12:13:08ZFerdie Reijnen#364 CIF data-based synthesis performance test models: wizard + festoAddresses #364
* Added benchmark import wizard.
* Added FESTO benchmark as an example.Addresses #364
* Added benchmark import wizard.
* Added FESTO benchmark as an example.v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/533#364 Small fix in lithography_init CIF benchmark model _source.txt file.2023-03-17T07:51:32ZDennis Hendriks#364 Small fix in lithography_init CIF benchmark model _source.txt file.Addresses #364Addresses #364v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/316#365 Update paper references in AsciiDoc files2022-05-06T05:05:36ZFerdie Reijnen#365 Update paper references in AsciiDoc filesCloses #365Closes #365v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/318#367 Improved website style. Cleaned up unused CSS styles.2022-05-12T07:40:40ZDennis Hendriks#367 Improved website style. Cleaned up unused CSS styles.Closes #367Closes #367v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/386#368 Extend and add checker classes for cif2dmm2022-10-14T13:16:25ZAlbert Hofkamp#368 Extend and add checker classes for cif2dmmAddresses #368Addresses #368v0.8Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/349#368 Implement cif2dmm2023-01-18T06:23:03ZAlbert Hofkamp#368 Implement cif2dmmRewritten from scratch. Extracts CIF object relations from a specification, in particular from plants and input variables to invariants and requirement automata, through shared events, and accessed locations and variables.
As the theory...Rewritten from scratch. Extracts CIF object relations from a specification, in particular from plants and input variables to invariants and requirement automata, through shared events, and accessed locations and variables.
As the theory isn't developed beyond normal automata, much of the implementation was guided by the spirit of the math and the previous attempt. As such, it would be helpful if @mgoorden7u4 could have a look at it.
Some notes about the submitted files:
- Code is in `oee.cif.multilevel` as that it is part of that application.
- The pre-checker should only check for `cif2dmm` requirements, not sure abut "locations references must be to plant locations".
- While it is no doubt a sane rule, I am not sure it is strictly a requirement. Other code simply ignores all requirement automata locations, which has the same doubts of course.
- The pre-checker is not collecting problems, it simply throws on the first found problem. The reason for that is that this checker needs to be integrated in the multilevel application eventually together with eg datasynthesis pre-conditions. Also, At the time of writing a more modular prechecker was being created, it seemed a waste of time to finish this
- `Cif2Dmm` is the main program of the sub-routine, and is also the result (the 4 DMM variables at the top).
- It collects references by searching through parts of the specification using the the `Collector` class.
- The `FoundObjects` class stores the all relevant CIF elements (events, locations, variables) in an array to obtain a unique index for each element, and keeps `BitSet`s of "referenced and possibly shared" references to such elements from "referring" elements (automata and invariants).
- All kinds of objects are all thrown into one heap, as code is working with the bitsets.
- Once the relations are found, constructing product systems is simple in `FoundObjects.partitionPlantsToProductSystems()`.
- And then it is time to construct the DMMs from the bitsets. I opted for splitting the relations so the rows and columns of a DMM have only one kind of CIF element. I didn't bother removing empty rows or columns, not sure if that is needed.
Closes #368Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/470#368 Implement `cif2dmm` computation, 3rd attempt2023-01-18T06:45:01ZAlbert Hofkamp#368 Implement `cif2dmm` computation, 3rd attemptAdds a `multilevel` application that currently only performs a cif-to-dmm conversion, with optional output of the computed DMMs.
Idea is still the same, with adjustments for the updated approach (mostly the extension with requirement gr...Adds a `multilevel` application that currently only performs a cif-to-dmm conversion, with optional output of the computed DMMs.
Idea is still the same, with adjustments for the updated approach (mostly the extension with requirement groups).
Few notes:
- The rules to compute the DMMs are documented as well.
They should be the same as discussed before in #368, except that input variables now always access themselves. The reason for the latter change is that a group needs to have at least one owning or accessing relation or it will never be merged or used.
Also added a bit more text and split the rules into the basic cases, rather than having them merged into a single sentence.
- The pre-checker only covers the needs of cif-to-dmm. In the future, a decision is needed how to add more other checks (eg to fulfill requirements of datasynthesis).
- The unit tests cover finding relations and merging of groups. The `cif.tests` project contains test cases that compare the resulting DMMs.
Addresses #368v0.9Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/330#369 Fix outdated comments in SynthesisToCifConverter regarding explicit kinds2022-06-12T18:11:05ZFerdie Reijnen#369 Fix outdated comments in SynthesisToCifConverter regarding explicit kindsCloses #369Closes #369v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/134#36 AsciiDoc multi-page HTML generation for website and Eclipse help2021-09-27T12:13:22ZDennis Hendriks#36 AsciiDoc multi-page HTML generation for website and Eclipse help - Added AsciiDoc multi-page HTML split functionality and integrated it into the build for all 5 documentation sets.
- Multi-page HTML links to both PDF and single-page HTML now.
- No more warnings on missing 'toc.xml' files if no loca... - Added AsciiDoc multi-page HTML split functionality and integrated it into the build for all 5 documentation sets.
- Multi-page HTML links to both PDF and single-page HTML now.
- No more warnings on missing 'toc.xml' files if no local build has been done. Added dummy toc.xml files.
- No more duplicated contents in documentation plugins for Eclipse help content. A development runtime will no longer contain the 5 documentation sets, even after a local build. Do a full local build and check the product instead.
- No more section anchors for Eclipse help output. Enabled section anchors for website output.
- No more 'geneclipsetoc-maven-plugin' dependency for build.
- Added jsoup and guava to the target platform.
- Fixed documentation build launch configurations to also make dependencies, not dependents.
- Chi documention: unique section name per source file.
- CIF documentation: increase TOC level to ensure all pages in TOC, simulation TOC structure fix, small capitalization improvements, link syntax fix.
- Lists.single method added.
Closes #36v0.3https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/326#370 Generalized CIF to Supremica precondition checks to reusable checks.2022-06-13T15:25:41ZDennis Hendriks#370 Generalized CIF to Supremica precondition checks to reusable checks.Model walkers:
- `ModelWalkerGenerator` now also generates composite model walkers.
- Removed unused `rootClassName` argument/variable from `ModelWalkerGenerator`.
EMF code generators
- Removed 'v1x0x0' from JavaDoc.
- Small improvement...Model walkers:
- `ModelWalkerGenerator` now also generates composite model walkers.
- Removed unused `rootClassName` argument/variable from `ModelWalkerGenerator`.
EMF code generators
- Removed 'v1x0x0' from JavaDoc.
- Small improvements and alignments for EMF code generators.
CIF (pre)condition checkers:
- Added generic CIF (pre)condition check(er) functionality.
- Added various preconditions checks. Based on the ones used by CIF to Supremica. Some more general checks as well.
- Change `CifToSupremicaPreChecker` to use generic checker, and updated CIF to Supremica expected test output. Other checkers to be done in separate branches.
CIF common:
- Added `CifTextUtils.hasName/getNamedSelfOrAncestor`.
I recommend reviewing per commit.
Addresses #370v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/324#371 Improved CIF data-based synthesis variable ordering API2022-05-31T13:00:13ZDennis Hendriks#371 Improved CIF data-based synthesis variable ordering APIThere are quite a few changes in this branch:
* `AutoVarOrderer` is now `VarOrderer` and is an interface instead of a base class. It now longer forces a representation of the specification and internal storage decisions upon the actual a...There are quite a few changes in this branch:
* `AutoVarOrderer` is now `VarOrderer` and is an interface instead of a base class. It now longer forces a representation of the specification and internal storage decisions upon the actual algorithms. The initialization and cleanup is also gone. There is now just a single method that algorithms should implement.
* `VarOrderHelper` contains the hyper-edges, which is currently the only representation of the specification. More representations can be easily added to it.
* `VarOrderHelper` also contains various utility methods, moved from `AutoVarOrderer`.
* Moved all non-algorithm-specific functionality out of `AutoVarOrderer` to `CifToSynthesisConverter`. It now determines whether to apply algorithms or not, and indicates in debug output why it is skipped. Or also prints the general debug output, such as number of hyper-edges.
* The variable ordering algorithms (through the `VarOrderer` interface), no longer reorder the variables in `SynthesisAutomaton`. They just compute new orders for the variables. `CifToSynthesisConverter` applies the final order to `SynthesisAutomaton`. This keeps the 'original order' stable. Also, it makes it easier to implement a `ChoiceVarOrderer` that applies multiple algorithms to the same input order and chooses the best order produced by various algorithms.
* The `VarOrderer` interface has `dbgLevel` to allow arbitrary trees of algorithms. For instance, atomic algorithms such as FORCE and sliding window can now easily be combined with sequence, choice, reverse, etc wrappers algorithms to form complex algorithm trees. Since we get arbitrary nesting levels, `dbgLevel` allows printing intuitive debug output matching the algorithm tree structure.
* As a result of the changes, with `CifToSynthesisConverter` handling the non-algorithm-specific things, with `dbgLevel` being introduced, and with the reason for skipping automatic variable ordering being printed, the debug output of the regression tests have changed. However, these are only debug output changes. The algorithms function as before, and produce the same variable orders. Functionality, it works as before for end users.
* I got confused several times while working on this about terminology. Terms like 'order' and 'indices' were used in different ways, which was confusing, and led to regression bugs. Hence, I now use 'order' for orders of the variables (including per variable in the new order its original 0-based index), and (new) indices when referring to per variable in its original order its new 0-based index. Previously 'order' and 'indices' where sometimes used to refer to both these meaning. I've improved and clarified in various places the naming, JavaDoc, comments, etc, to hopefully avoid such confusion in the future.
I did several iterations of changing the API, not just for the current algorithms, but also to support future extensions (#196). This is the design I ended up with, that seems to fit well.
If you want to review this, I propose to review it commit by commit. I completely reworked my final solution into smaller commits, for reviewing efficiency. Each commit message has further details on the changes. However, some things only become clear in a later commit, as the changes in different commits are somewhat intertwined, and I could not spend days on even better-reviewable commits.
Closes #371
Addresses #196v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/325#372 Updated DEPENDENCIES.txt for changed output of license check tool.2022-06-04T15:52:28ZDennis Hendriks#372 Updated DEPENDENCIES.txt for changed output of license check tool.Closes #372Closes #372v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/328#374 Use default maximum available memory for product as determined by JVM2022-06-16T13:43:07ZDennis Hendriks#374 Use default maximum available memory for product as determined by JVM- For product and product runtime launch configuration.
- Also updated product documentation.
Closes #374- For product and product runtime launch configuration.
- Also updated product documentation.
Closes #374v0.6https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/405#375 Add scripts to benchmark data-based synthesis to CIF benchmarks.2022-11-19T12:49:44ZDennis Hendriks#375 Add scripts to benchmark data-based synthesis to CIF benchmarks.I've added multiple files:
* `benchmark__base.tooldef` contains the logic to execute data-based synthesis with various settings, collect various statistics, and output it to file and stdout.
* `benchmark__settings.tooldef` allows configu...I've added multiple files:
* `benchmark__base.tooldef` contains the logic to execute data-based synthesis with various settings, collect various statistics, and output it to file and stdout.
* `benchmark__settings.tooldef` allows configuring the settings to benchmark. By default, it executes data-based synthesis once, with default settings. The comments explain how to configure it differently.
* `benchmark_*.tooldef` scripts, one per benchmarking model, allow benchmarking specific benchmarking models. Having multiple scripts allows running them in parallel. This does require disabling the 'Auto Terminate' option of the 'Applications' view. Running too much in parallel may affect timing metrics. But the maximum number of BDD nodes and the number of BDD operations are also collected and are more reproducible anyway.
These scripts are to benchmark different settings for different benchmark models, comparing the settings against each other, for instance to compare different variable ordering algorithms. They are explicitly not meant to benchmark the performance of CIF data-based synthesis against other synthesis tools. Collecting the platform-independent metrics makes synthesis much slower, and other tools likely don't do this. A fair comparison with other tools requires a completely different approach, which is out of scope here.
Closes #375v0.8