escet merge requestshttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests2023-12-09T20:05:01Zhttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/709#698 Fix CIF explorer state annotation argument value type creation2023-12-09T20:05:01ZDennis Hendriks#698 Fix CIF explorer state annotation argument value type creationCloses #698Closes #698v2.0https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/350#398 Various checks for CIF checker crash for violations in the root of the s...2022-09-11T18:09:55ZFerdie Reijnen#398 Various checks for CIF checker crash for violations in the root of the specificationCloses #398Closes #398v0.7https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/183Draft: Resolve "SVG viewer save as suggested file name/path doesn't work as e...2021-11-09T06:05:18ZFerdie ReijnenDraft: Resolve "SVG viewer save as suggested file name/path doesn't work as expected"Closes #221Closes #221v0.4Ferdie ReijnenFerdie Reijnenhttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/797#269 CIF BDD and data-based synthesis: Use collectEvents/collectAutomata from...2024-02-06T18:59:28ZDennis Hendriks#269 CIF BDD and data-based synthesis: Use collectEvents/collectAutomata from CifCollectUtils.* Best to review per commit.
* Additional change in `CifCollectUtils`: one implementation for `getComplexComponentsStream`.
Addresses #269* Best to review per commit.
* Additional change in `CifCollectUtils`: one implementation for `getComplexComponentsStream`.
Addresses #269v3.0https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/722#715 CIF code generator: Add HTML and JavaScript target language for export.2023-12-20T07:06:12ZRik Lubking#715 CIF code generator: Add HTML and JavaScript target language for export.#715 - Add export target Language HTML and JavaScript.
- Moves css into html template.
- Moved JavaScript out of html template.
- Added JavaScript/HTML export options as target languages.
- Added write method/logic for merging JavaScrip...#715 - Add export target Language HTML and JavaScript.
- Moves css into html template.
- Moved JavaScript out of html template.
- Added JavaScript/HTML export options as target languages.
- Added write method/logic for merging JavaScript into HTML export.
Addresses #715v2.0https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/716#272 CIF code generator: add SVG boilerplate code to JavaScript code generator2023-12-20T23:20:38ZRik Lubking#272 CIF code generator: add SVG boilerplate code to JavaScript code generator- Added boilerplate code for SVG implementation, remaining implementation to be added in the next merge.
Addresses #272- Added boilerplate code for SVG implementation, remaining implementation to be added in the next merge.
Addresses #272v2.0Dennis HendriksRik LubkingDennis Hendrikshttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/683#679 PLCgen: Add formal invoke options2023-11-13T09:36:37ZAlbert Hofkamp#679 PLCgen: Add formal invoke optionsAdds the formal invoke options.
- `FormalInvokeArg*` was actually about `FormalInvokeParam*` (the number of parameters of the function rather than the number of supplied arguments).
- `ModelTextGenerator` is now an instance taking the v...Adds the formal invoke options.
- `FormalInvokeArg*` was actually about `FormalInvokeParam*` (the number of parameters of the function rather than the number of supplied arguments).
- `ModelTextGenerator` is now an instance taking the values of the invoke option settings.
- Comparing against `cif2plc` was messy as generated output is hugely different. In the end if grabbed function-like text of the form `NAME(......`, that is an all-uppercase name and a parenthesis, and then some text behind it to get the tell-tale `:=` and then sorted on function use. See the attached output file for all combinations of the new option values. Also added the python script just in case.
text[output.txt](/uploads/97b7c300b09bfe2dd370ff4eabcc10eb/output.txt)
[find_funcs.py](/uploads/1f3e4ee30b56a2a296c766d0c1e62fc3/find_funcs.py)
- It seems complicated to get the result I'd like. Possibly the notion of "std" differs between both programs, and/or the collection of allowed forms of expressions. Also how to decide between infix / non-formal prefix / formal prefix is likely different.
- My current guess is that we need more precise options to better express the desired result. I'd like to do that not now though.
Addresses #679v2.0Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/680#272 JavaScript code generation step 1: add export menu option2023-10-30T08:49:18ZRik Lubking#272 JavaScript code generation step 1: add export menu option- Added JavaScript export option to export menu.
- Added empty search/replace template (to be filled in later).
- Created empty stub methods for most implementations (to be filled in
later).
* Export feature works without problems/error...- Added JavaScript export option to export menu.
- Added empty search/replace template (to be filled in later).
- Created empty stub methods for most implementations (to be filled in
later).
* Export feature works without problems/errors, but currently only
generates an empty .html file.
For discussion, see: https://gitlab.eclipse.org/riklubking/escet/-/issues/27
Addresses #272v2.0https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/675#676 PLCgen: Postpone remaining options to after the first release2023-10-31T15:57:42ZAlbert Hofkamp#676 PLCgen: Postpone remaining options to after the first releaseDropped PlcMaxIterOption PlcFormalFuncInvokeArgOption
and PlcFormalFuncInvokeFuncOption for now.
Addresses #676Dropped PlcMaxIterOption PlcFormalFuncInvokeArgOption
and PlcFormalFuncInvokeFuncOption for now.
Addresses #676v2.0Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/662#443 Add zooming to SVG viewer/visualizer2023-11-25T10:15:47ZPatrick van Berkel#443 Add zooming to SVG viewer/visualizerThis merge request implements:
1. Zooming of the SVG document by Ctrl+- and Ctrl+=.
2. ~~Panning of the SVG document by dragging the document using the mouse.~~
3. ~~Resizing of the canvas by resizing the parent window.~~
I added de de...This merge request implements:
1. Zooming of the SVG document by Ctrl+- and Ctrl+=.
2. ~~Panning of the SVG document by dragging the document using the mouse.~~
3. ~~Resizing of the canvas by resizing the parent window.~~
I added de demo video to show wat it looks like ~~(see [demo.mp4](/uploads/9c0148707ad5ade461430a93d4f86c0b/demo.mp4))~~, [demo-zoom.mp4](/uploads/32de4fd5e9b7abae5afed1108ecf4d6b/demo-zoom.mp4).
I am however having one issue. Because images are painted in memory and then passed via a queue there exists a short moment during resize in which the preprinted image does not match de size of the resized canvas. To handle this situation this implementation does not paint the image during resizing. The resulting behavior can be seen in the video ~~[issue.mp4](/uploads/3ce5d479fb67d363648918ba97c5f4ab/issue.mp4)~~, [missing-frames](/uploads/c0774a37ba666fb7582d48eef2f19830/missing-frames.mp4).
This behavior is also enabled in the Chi Visualizer als wel as the SVG viewer.
Closes #443v2.0https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/600#596 PLCgen: differentiate between reading and writing CIF variables.2023-06-05T09:48:59ZAlbert Hofkamp#596 PLCgen: differentiate between reading and writing CIF variables.A few shortcuts for simplifying PLC statement construction, and a bigger extension to the expression generator. The latter is explained in more detail below (same as in the commit message).
Reading a value should return a `PlcExpression...A few shortcuts for simplifying PLC statement construction, and a bigger extension to the expression generator. The latter is explained in more detail below (same as in the commit message).
Reading a value should return a `PlcExpression`, while writing a value should be a `PlcVarExpression`.
While the difference is small, adding a type parameter for the "value" field in the `ExprGenResult` class causes havoc throughout the expression code, due to type erasure and my desire not to have to write `ExprGenResult<PlcExpression>` everywhere so I can have a handful of `ExprGenResult<PlcVarExpression>`.
In the end I created two specializations of the `ExprGenResulr` class:
- `ExprValueResult` for results that read the expression value, and
- `ExprAddressableResult` for results that modify the expression value.
- `ExprGenResult` is now a base-class without "value" field, with two derived classes `ExprValueResult` and `ExprAddressableResult`.
The `ExpressionGenerator` external interface now has `ExprValueResult convertValue(Expression)` instead of the old `convertExpr` method and `ExprAddressableResult convertAdressable(Expression)` for the modifiable variant.
- The `ExpressionGenerator.convertAdressable(Expression)` variabnt doesn't handle the `f().field` case, but that is fine as it is not addressable in CIF either.
- `CifDataProvider` methods now has "Value" prefixes (for the existing methods) if the data is meant for reading, and additional "Addressable" variants for modifying discrete and continuous variables.
For simplicity I assumed derivative are writable, this may have to change at some point.
`DefaultVariableStorage` returns the same PLC variables for CIF variables but that is all still testing code currently.
- `ExprGeneratorTest` existing `runTest` is now `runValueTest`, and an additional `runAdddressableTest` has been added for testing writing to discrete and continuous variables.
Addresses #596v0.10Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/595Draft: #520 Add algorithm by Fei et al. (2014) to compute edge dependency sets2023-05-29T14:40:45ZDennis HendriksDraft: #520 Add algorithm by Fei et al. (2014) to compute edge dependency sets* This merge quest is based on a somewhat outdated version of !587, and includes the changes of that older version of !587 as well. The relevant commits are f6612fc387e8fabd2b49fab6e7cf1319b22d3f78 and later. If we want to keep this merg...* This merge quest is based on a somewhat outdated version of !587, and includes the changes of that older version of !587 as well. The relevant commits are f6612fc387e8fabd2b49fab6e7cf1319b22d3f78 and later. If we want to keep this merge request and merge it, I'll recreate it based on the latest version, and then I'll also clean up the history. However, I propose not to ever merge it, see below.
* Getting a working solution:
* I tried to implement the algorithm from Fei et al. (2014) that I summarized [here](https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/520#note_1114569).
* I found that it has [a bug](https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/520#note_1140352) that I fixed, at the cost of significantly larger dependency sets, which will reduce the performance of the workset algorithm. But, correctness is more important than performance.
* The `FeiEdgeDependencySetCreator` now includes various additions compared to the orginal algorithm of Fei et al. (2014), to fix the bug, but also to account for various features of the CIF language that we support in data-based synthesis, but that were not in the EFAs as defined by Fei et al.
* This modified algorithm works for our entire regression test set, where I temporarily enabled the workset algorithm for all tests. Thus, I'm not aware of any issues in this implementation.
* But it has become complex:
* The `FeiEdgeDependencySetCreator` has 576 lines.
* Several parts of the algorithm now have long sections with comments that explain why certain modifications of the algorithm are needed. It is not exactly simple anymore.
* The order in which various concepts are considered needs to be exactly right, or things go wrong. I made mistakes several times while working on it. I can't be sure there are more issues in it.
* Getting the dependencies right, such that they work for our regression tests required quite some trial and error. I can't be sure it works for all models, only that it works for the ones in the current regression test set.
* Fundamentally, what I don't like about the algorithm is that it tries to compute when things can follow. However, as the bug showed, this is both difficult to determine statically. It requires that sufficient dependencies are found and unioned together. But how do we now that we didn't miss some dependency that only in some rare situations is needed. Guaranteeing that we don't have an under-approximation seems practically impossible.
* It seems the whole algorithm is now useless:
* The unit tests were adapted in a separate commit after the fix, to show how much the depencies increase. In fact, all unit tests now have the full/maximal dependency set.
* Similarly, for all integration tests, the dependency sets are full/maximal dependency sets.
* Thus, we could just as well use `AllEdgesEdgeDependencySetCreator`, which gives the same dependency sets, which much simpler code.
* I created a merge request for two reasons:
* I think it is good to keep this attempt archived. However, in the current state I don't propose to merge it.
* @ahofkamp is working on something similar, for the PLC code generator, in #595. It may be useful to be aware of all this, to take it into account there as well.
* I've come up with an alternative, see #602.
Addresses #520v0.10https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/562#418 PLCgen: add default initial values to the converted state variable decla...2023-04-30T07:46:58ZAlbert Hofkamp#418 PLCgen: add default initial values to the converted state variable declarations.Short patch, can be read by individual commit, which looks like the better approach for reviewing.
Addresses #418Short patch, can be read by individual commit, which looks like the better approach for reviewing.
Addresses #418v0.10Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/472Draft: #378 CIF data-based synthesis variable ordering and reordering in one go.2023-03-12T11:23:27ZDennis HendriksDraft: #378 CIF data-based synthesis variable ordering and reordering in one go.* The main idea is that the initial variable order and subsequent algorithms applied to it, are now one configuration, and they are applied in one go. This is a step in #378, towards also adding a new option that can create more complex ...* The main idea is that the initial variable order and subsequent algorithms applied to it, are now one configuration, and they are applied in one go. This is a step in #378, towards also adding a new option that can create more complex such configurations, but that can be applied in the same way.
* Probably easiest to review per commit, but there is some shuffling involved that in hindsight I could have maybe done in more separate commits.
* The variable ordering helper is now always created from the model order. This may change the variable order. For the test models, I checked each change manually, and found it to be different but equivalent. I'm running the benchmark models now, to see if/how it affects them. I'll post a separate comment about it. But the merge request can be reviewed already.
* Some other smaller changes, see commit messages of separate commits.
Addresses #378v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/464Draft: #454 New output for CIF checks2023-02-21T19:00:44ZDennis HendriksDraft: #454 New output for CIF checks* This merge request is not ready by any means. It serves to allow discussion on this attempt at new output.
* I had to move all CIF checks to a new plugin to prevent a cyclic dependency.
* The design for checks is much simpler, as there...* This merge request is not ready by any means. It serves to allow discussion on this attempt at new output.
* I had to move all CIF checks to a new plugin to prevent a cyclic dependency.
* The design for checks is much simpler, as there are no message classes anymore. Just (formatted) strings.
* I got rid of reporting on ancestors or named objects, requiring `PositionObject` objects with a position. It turns out not all expressions and types have a position, even after re-parsing. I haven't looked into why that is yet. Let's see what we want as output first.
* No more reporting on `null` specifications. Just supply the `Specification` object instead. Typically, this is used in `preprocessSpecification` or `postprocessSpecification`, which have that already anyway. Can use `CifScopeUtils.getSpecification` otherwise.
* For the new output, I opted to first categorize by message, and then sort per line, and then for all violations on the same line report them with the text of the line and markers.
Addresses #454v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/399#424 Generalize allowed invariants check.2022-12-07T12:19:19ZAlbert Hofkamp#424 Generalize allowed invariants check.Addresses #424
Just supervisor kind checking for invariants wasn't sufficient for cif2plc, so generalized the invariants check to place, supervisor kind and invariant kind.Addresses #424
Just supervisor kind checking for invariants wasn't sufficient for cif2plc, so generalized the invariants check to place, supervisor kind and invariant kind.Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/357Draft: #382 (take 2) Make plcgen0 accessible in ESCET.2023-12-22T13:44:51ZAlbert HofkampDraft: #382 (take 2) Make plcgen0 accessible in ESCET.Making previous art available for testing and reference.
**This branch should not be merged**.
An improved version is being created in #397.
## Restrictions:
``` text
// 1. no external functions
// 2. no tau events
...Making previous art available for testing and reference.
**This branch should not be merged**.
An improved version is being created in #397.
## Restrictions:
``` text
// 1. no external functions
// 2. no tau events
// 3. no types: Set, Func, CompParamWrap, CompInstWrap, ComponentDef, Dist, Dict, Void.
// 4. no automaton reference (or self) child isn't allowed
// 5. no exprs: slice, tau, event, set, time, self, component, compParamWrap, compInstWrap, dict
// 6. no urgent locations/edges
// 7. must have trivially true initial location and expressions.
// 8. no empty lists/arrays
// 9. no variable length lists
// 10. no continue function statement (from FuncGen.java:186, even though funcs are not allowed)
// 11. no function parameter names that are are keywords, including EN and ENO. (from renameNames:393)
// 12. no string projection
// 13. no multiple initial values
// 14. no stdLibFuncs: ACOSH ASINH ATANH BERNOULLI BETA BINOMIAL CEIL CONSTANT COSH DELETE EMPTY ERLANG EXPONENTIAL FLOOR FORMAT GAMMA GEOMETRIC LOG_NORMAL NORMAL POISSON POP RANDOM ROUND SCALE SIGN SINH SIZE TANH TRIANGLE UNIFORM WEIBULL
// 15. no unary expression SAMPLE
// 16. no binary expression ELEMENT_OF SUBSET
// 17. no internal functions with cyclic dependencies (there should not be functions)
// 18. no an event must have at least one non-monitoring automaton. (-> finite response)
// 19. no list/array of empty tuples
// 20. no constants may not use functions (both internal and stdlib).
```
CIF code that will cause crashes/incorrect PLC code:
``` text
- Using tuples in updates creates incorrect PLC code, eg "edge a do x:=(1,2);"
- Events that are declared within an automaton but not used anywhere result in an AssertionError.
- Multi-assignments result in a java.lang.NullPointerException. eg "edge a do (x,y) := (y,x);"
```
## Using the generator:
- Make an empty IO table named `empty.csv`.
- Make a `.tooldef` file with the following text:
``` tooldef
// Defines the 'plcgen0 tool.
tool int plcgen0(list string args = [], string stdin = "-", string stdout = "-", string stderr = "-",
bool appendOut = false, bool appendErr = false, bool errToOut = false, bool ignoreNonZeroExitCode = false):
return app("org.eclipse.escet.cif.plcgen0", "org.eclipse.escet.cif.plcgen0.app.PlcGen2App", args, stdin, stdout, stderr,
appendOut, appendErr, errToOut, ignoreNonZeroExitCode);
end
// Run the plcgen0 program.
// - Replace "abb" by "siemens-7-1500" to get siemens output, (Other targets will likely fail.)
// - Replace "model.cif" by the name of the cif model to convert,
// - stdout and stderr settings may be added to get the output at the console.
plcgen0(["--io-table-name=empty.csv", "--target-type=abb", "model.cif"]);
// With output redirection: plcgen0(["--io-table-name=empty.csv", "--target-type=abb", "model.cif"], stdout="out_file", stderr="err_file");
// For a non-empty IO table, the following fields are required for each line in the .CSV file:
// - PLC address,
// - PLC typename,
// - Full path to CIF input-variable or output location/disc-variable/alg-variable
//
// For example for "input bool input1" and "alg bool output1 = ..." in the root of the specification, the following is accepted.
// %I1,BOOLEAN,input1
// %Q2,BOOLEAN,output1
```
- Adjust the `plcgen0` line to your liking, `plcgen0(["-h"]);` will dump the accepted options.v3.0Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/352Draft: #382 Make plcgen0 accessible in ESCET.2022-08-11T10:50:09ZAlbert HofkampDraft: #382 Make plcgen0 accessible in ESCET.Making previous art available for testing and reference.
An improved version is being created in #397.
## Restrictions:
``` text
// 1. no external functions
// 2. no tau events
// 3. no types: Set, Func, Comp...Making previous art available for testing and reference.
An improved version is being created in #397.
## Restrictions:
``` text
// 1. no external functions
// 2. no tau events
// 3. no types: Set, Func, CompParamWrap, CompInstWrap, ComponentDef, Dist, Dict, Void.
// 4. no automaton reference (or self) child isn't allowed
// 5. no exprs: slice, tau, event, set, time, self, component, compParamWrap, compInstWrap, dict
// 6. no urgent locations/edges
// 7. must have trivially true initial location and expressions.
// 8. no empty lists/arrays
// 9. no variable length lists
// 10. no continue function statement (from FuncGen.java:186, even though funcs are not allowed)
// 11. no function parameter names that are are keywords, including EN and ENO. (from renameNames:393)
// 12. no string projection
// 13. no multiple initial values
// 14. no stdLibFuncs: ACOSH ASINH ATANH BERNOULLI BETA BINOMIAL CEIL CONSTANT COSH DELETE EMPTY ERLANG EXPONENTIAL FLOOR FORMAT GAMMA GEOMETRIC LOG_NORMAL NORMAL POISSON POP RANDOM ROUND SCALE SIGN SINH SIZE TANH TRIANGLE UNIFORM WEIBULL
// 15. no unary expression SAMPLE
// 16. no binary expression ELEMENT_OF SUBSET
// 17. no internal functions with cyclic dependencies (there should not be functions)
// 18. no an event must have at least one non-monitoring automaton. (-> finite response)
// 19. no list/array of empty tuples
// 20. no constants may not use functions (both internal and stdlib).
```
CIF code that will cause crashes/incorrect PLC code:
``` text
- Using tuples in updates creates incorrect PLC code, eg "edge a do x:=(1,2);"
- Events that are declared within an automaton but not used anywhere result in an AssertionError.
- Multi-assignments result in a java.lang.NullPointerException. eg "edge a do (x,y) := (y,x);"
```
## Using the generator:
- Make an empty IO table named `empty.csv`.
- Make a `.tooldef` file with the following text:
``` tooldef
// Defines the 'plcgen0 tool.
tool int plcgen0(list string args = [], string stdin = "-", string stdout = "-", string stderr = "-",
bool appendOut = false, bool appendErr = false, bool errToOut = false, bool ignoreNonZeroExitCode = false):
return app("org.eclipse.escet.cif.plcgen0", "org.eclipse.escet.cif.plcgen0.app.PlcGen2App", args, stdin, stdout, stderr,
appendOut, appendErr, errToOut, ignoreNonZeroExitCode);
end
// Run the plcgen0 program.
// - Replace "abb" by "siemens-7-1500" to get siemens output, (Other targets will likely fail.)
// - Replace "model.cif" by the name of the cif model to convert,
// - stdout and stderr settings may be omitted to get the output at the console.
plcgen0(["--io-table=empty.csv", "--target-type=abb", "model.cif"], stdout="out_file", stderr="err_file");
// For a non-empty IO table, the following fields are required for each line in the .CSV file:
// - PLC address,
// - PLC typename,
// - Full path to CIF input-variable or output location/disc-variable/alg-variable
//
// For example for "input bool input1" and "alg bool output1 = ..." in the root of the specification, the following is accepted.
// %I1,BOOLEAN,input1
// %Q2,BOOLEAN,output1
```
- Adjust the `plcgen0` line to your liking, `plcgen0(["-h"]);` will dump the accepted options.https://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/327#196 Add DCSH variable ordering algorithm to data-based synthesis.2022-06-27T19:51:45ZDennis Hendriks#196 Add DCSH variable ordering algorithm to data-based synthesis.Variable ordering changes/additions:
- Prepared `VarOrdererHelper` for more metrics besides total span.
- Reduced space used for printing total span metric.
- Variable amount of space based on initial metric value.
- Added WES to `Va...Variable ordering changes/additions:
- Prepared `VarOrdererHelper` for more metrics besides total span.
- Reduced space used for printing total span metric.
- Variable amount of space based on initial metric value.
- Added WES to `VarOrdererHelper` as additional variable ordering metric.
Graph related additions:
- Added `Graph` and `Node` classes to represent graphs for data-based synthesis variable ordering algorithms to use.
- Added graph representation support to `VarOrdererHelper`.
- For now, graphs are created from the existing hyper-edges, ensuring consistency between the different representations.
- We could later opt for other ways to create the hyper-edges/graphs.
- Added extra utility methods for use by variable ordering algorithms.
- Updated `CifToSynthesisConverter` for the added graph representation.
DCSH algorithm related additions:
- Added rooted level structure constructor for graphs.
- Added pseudo-peripheral node finder algorithms.
- I tried to stay as close as possible to the original papers.
- We have multiple algorithms here.
- These are the ones which are needed for the node ordering heuristic algorithms.
- We could experiment later which ones work best. (see below)
- For now, node ordering algorithms use the ones from their corresponding papers.
- Added node ordering heuristic algorithms.
- I tried to stay as close as possible to the original papers.
- These are the ones we need for the DCSH variable ordering algorithm.
- Weighted Cuthill-McKee has been improved wrt the original paper: it works also for multiple unconnected partitions with >1 node.
- Added variable ordering algorithms.
- Added Sloan and Weighted Cuthill-McKee variable ordering algorithms, using the corresponding node ordering algorithms.
- Added 'choice' and 'reverse' wrapper variable ordering algorithms.
- Add DCSH variable ordering algorithm.
- Is for now based on graphs constructed from the existing hyper-edges, ensuring consistency between the different representtations.
- Could later create DMSs/hyper-edges based on the paper's approach.
Data-based synthesis tool additions:
- Added new option for enabling DCSH variable ordering.
- Is disabled by default, as I consider it experimental for now.
- The 'experimental' label here is for end users. It does not concern the implementation.
Data-based synthesis variable ordering documentation additions/changes:
- Added DCSH algorithm/option.
- Extended explanation of heuristic algorithms in general.
- Extended explanation of when algorithms are not applied.
- Extended descriptions of the FORCE and sliding window algorithms.
Data-based synthesis tests additions/changes:
- Renamed data-based synthesis test cases relating to `force`.
- The `force` tests were about FORCE and sliding window, so were wrongly named.
- Changed `_force_` to `_algos_`.
- Also extracted the related common options in the test ToolDef script to variables.
- Added DCSH to variable ordering integration tests, to be applied with all the other algorithms for the `algos` tests.
- Resulting metrics are the same or better for all these tests with DCSH added to it.
- Added single variable ordering algorithm integration tests, besides the ones that test all the algorithms at once.
- But only for a single initial random order, not for all the other initial orders, to avoid an explosion of tests.
Regarding reviewing:
- I tried to keep the stack of commits reviewable one by one, although there are a few fixes/changes at the end that could potentially have been integrated into earlier commits.
- Still, reviewing this per commit can be useful, as otherwise the totality of changes can be overwhelming, and the commits build towards the end result nicely.
I stopped here with this branch, as it is quite extensive already. The following are left as future work. I've created issues for the most relevant ones:
- #375 It would be good to have some scripts to benchmark the benchmark models, comparing for instance FORCE + sliding window against DCSH + FORCE + sliding window, in an automated fashion. I partly put something together for this already.
- #376 I think more testing is needed. I don't yet know whether the improvements we get in terms of better variable orderings and reduced synthesis effort match what the DCSH paper indicates. That would be good to check before lifting the 'experimental' label for end users to use it.
- The choice variable orderer could support reverse orders as well, natively, to avoid applying the algorithms twice. However, that leads to more code, and a less modular design. I hope execution times are very short already anyway. But, I still want to measure those times to be sure. Otherwise we may want to look into this optimization.
- #374 I found that our `product-escet` launch configuration is configured with only 4 GB of memory. That seems very low for todays systems.
- #377 Hyper-edge creation has a bug, where for location invariants actually the component invariants are used. I'm a bit hesitant to change this now though, as it makes comparing the performance of DCSH against the paper more difficult. Also, what if it reduces synthesis performance. We have no good benchmarking set yet to test this.
- #378 Data-based synthesis now only allows DCSH to be applied before FORCE and FORCE before sliding window. The order is fixed. I think the options should be generalized, to allow for instance `choice(dcsh, sequence(force, sliding-window(9)))` etc. This gives more flexibility for testing different configurations. Actual testing would require more benchmark models though.
- #379 There are several places where choices can be made. We can choose the current hyper-edges vs the ones defined in the DCSH paper. We can enable DCSH by default or not. We can choose per algorithm (DCSH, FORCE, sliding window), to base it on the total span or WES metric. For the node ordering algorithms, we can choose which pseudo-peripheral node finding algorithm to use. All of this requires that we can determine what is better, hence we need ways to specify these choices, scripts to easily test the differences, and enough benchmarking models to conclude what is really better in general.
- Variable ordering seems to lack cancellation checking. If the code runs for longer times (see other point), then we may need to add more of it. For now, this does not seem needed.
- #380 We currently use the original hyper-edges. We could implement the hyper-edges defined in the DCSH paper, which may perform better.
Closes #196v0.6