escet merge requestshttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests2022-12-11T08:10:12Zhttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/422#457 Update CIF to PLC precondition checker to new checker framework2022-12-11T08:10:12ZAlbert Hofkamp#457 Update CIF to PLC precondition checker to new checker frameworkCloses #457
EDIT: Addresses #424Closes #457
EDIT: Addresses #424v0.8Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/428#457 Generalize invariants checking2022-12-07T10:45:14ZAlbert Hofkamp#457 Generalize invariants checkingAdresses #457 #368 #424
I was wrong in thinking I didn't need the generalized invariant check in cif2plc, as we found out in !422 .
Thus I moved implementing the check forward to allow finishing the cif2plc pre checker issue.
This patc...Adresses #457 #368 #424
I was wrong in thinking I didn't need the generalized invariant check in cif2plc, as we found out in !422 .
Thus I moved implementing the check forward to allow finishing the cif2plc pre checker issue.
This patch is built bottom up.
* It starts with adding a `PlaceKind` to express place of an invariant, together with `ReportPriority` that defines a relevance notion.
* Next the `NoKindInterface` is defined to form a common ground for the `NoInvariant...Kind` enumerations that define what the user can specify for the check.
If you read commits, I made the error here of adding a `size`(?) notion to the interface which doesn't work as it's not a member function.
The interface is not strictly needed, but I think it's good to have it anyway as it reduces duplication of function docs, and forces consistency.
* On top of the `NoInvariant...Kind` enumerations comes the `DisallowedSubset` class that stores a specified invariants subset that should be reported when found.
* The main check class `InvNoSpecificInvsCheck` stores all the disallowed subsets for all combinations of `SupKind`, `InvKind`, and `PlaceKind`. It silently discards checks that are not relevant enough to get reported for each combination individually.
Checking is then a simple "grab the disallowed subsets for the concrete invariant that we find, and report it if disallowed subsets are indeed found".
* The check class is extended with the "ignore harmless invariants" extension (`invariant true`, `needs true`, `disables false`).
* A tests to check the harmless extension works, and a test with 2 disallowed subsets.
Three further points:
* I don't know how to fix the `- Unsupported "named_invs.I2" (File "...": line 72, columns 15 .. 16): invariant is invariant.` error. The message is stupid. The first `invariant` is the named object (generated by the framework), the second `invariant` is generated by my check.
* There are other invariant checks and tests in the pre-checker framework, the simplest to do is perhaps remove those after merging this.
* There is also a previous branch for this check that was deemed too complicated or wrong (branch `424-more-general-invariants-checker`).
EDIT: Added the proper issue number in the title.v0.8Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/423#456 Fixed a typo in ToolDef 'filenewer' tool JavaDoc and documentation.2022-11-24T20:27:16ZDennis Hendriks#456 Fixed a typo in ToolDef 'filenewer' tool JavaDoc and documentation.Closes #456Closes #456v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/420#455 Add script to generate overview of synthesis benchmarking results.2022-11-24T14:44:38ZDennis Hendriks#455 Add script to generate overview of synthesis benchmarking results.- Also added README to explain the steps.
- Added note explaining why synthesis takes longer when benchmarking.
Closes #455- Also added README to explain the steps.
- Added note explaining why synthesis takes longer when benchmarking.
Closes #455v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/482#454 New plugin for the CIF checkers.2023-01-24T07:22:55ZDennis Hendriks#454 New plugin for the CIF checkers.- Functionality has grown, and deserves a separate plugin.
- Prevents pretty printer vs common dependency cycle, in next steps for #454.
Addresses #454- Functionality has grown, and deserves a separate plugin.
- Prevents pretty printer vs common dependency cycle, in next steps for #454.
Addresses #454v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/511#454 New output for CIF checks (2nd attempt)2023-03-03T13:20:41ZDennis Hendriks#454 New output for CIF checks (2nd attempt)* This merge request replaces the previous one, !464. It was quite some work, but I think I've addressed all the issues. I'm quite happy with the output that is now produced.
* Checks API:
* The design for checks is much simpler, as th...* This merge request replaces the previous one, !464. It was quite some work, but I think I've addressed all the issues. I'm quite happy with the output that is now produced.
* Checks API:
* 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.
* 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 sorted message, then by sorted context, and then by sorted line nr.
* All violations (for that message and context) on the same line are reported with the text of that line, and markers that indicate where the violations are within the line.
* Violations reported on the specification have only a message, no context, no lines, no markers.
* Various checks have improvements beyond pure API adaptations:
* Automaton only with one initial location: reports evaluation failures per initialization predicate.
* Component no initialization predicates: report per initialization predicate.
* No specific expressions: no more info than needed in violation messages.
* No specific expressions: specific relevant information in violation messages.
* No specific expressions: some other small improvements.
* No specific binary expressions: no more info than needed in violation messages.
* No specific unary expressions: no more info than needed in violation messages.
* Locations only statically evaluable marker predicates: report violations per marker predicate.
* Other changes:
* Various type checker and position information fixes, to ensure position information on types is from where the type is used, not from where the type is defined or copied from.
* CIF parser: standard library function calls now has position info on the `(` symbol for the function call, and position information on the standard library function reference itself only for the standard library function reference. Previously, both had the position information from the standard library function reference. This makes that we can distinguish between the two. It also makes standard library function calls consistent with other function calls.
* Removed some unnecessary super calls from test class constructors.
* Merge request is ready to be reviewed. Probably best to review per commit, as there are quite a few of them, with quite some changes, as the whole checker framework is essentially redesigned. I reworked the commits to hopefully make it easy to review.
* Potential follow-ups:
* Explain the output in the end user documentation, such that users can read how to interpret the output, how to work with, etc.
* Adapt the pretty printer to use a keyword for each line, e.g., for each initialization and marker predicate.
Closes #454v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/415#453 Update release process for GitLab tag and release creation.2022-11-15T17:08:24ZDennis Hendriks#453 Update release process for GitLab tag and release creation.Closes #453Closes #453v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/411#452 Updated DEPENDENCIES.txt.2022-11-14T20:16:19ZDennis Hendriks#452 Updated DEPENDENCIES.txt.Closes #452Closes #452v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/404#451 Add dining philosophers as CIF benchmark model.2022-11-10T07:50:01ZDennis Hendriks#451 Add dining philosophers as CIF benchmark model.I've opted to adapt the model from four forks and philosophers in the current test model to the traditional number of five forks and philosophers. For the synthesis time this barely makes a difference.
Closes #451I've opted to adapt the model from four forks and philosophers in the current test model to the traditional number of five forks and philosophers. For the synthesis time this barely makes a difference.
Closes #451v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/459#450 Rename 'path separator' to 'file separator'2022-12-31T13:55:31ZDennis Hendriks#450 Rename 'path separator' to 'file separator'Closes #450Closes #450v0.9https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/78#44 Improve EMF constructor generator generated JavaDoc.2021-05-25T07:09:16ZFerdie Reijnen#44 Improve EMF constructor generator generated JavaDoc.- Improved generator
- Generated new constructors for Chi, CIF and tooldef- Improved generator
- Generated new constructors for Chi, CIF and tooldefhttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/407#449 Extend cast-expression pre-checking2022-11-14T05:42:31ZAlbert Hofkamp#449 Extend cast-expression pre-checkingAdd more precise checks in disallowing casts.
Closes #449
Addresses #424
EDIT: Added an explanation what has changed.Add more precise checks in disallowing casts.
Closes #449
Addresses #424
EDIT: Added an explanation what has changed.v0.8Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/403#448 Improve CopyFilesNewProjectWizard.2022-11-09T20:09:59ZDennis Hendriks#448 Improve CopyFilesNewProjectWizard.- Derived classes now specify single source and target folder paths.
- Target folder path is specified by default as '.'.
- Supports copying files and folders from the source folder path.
- CIF examples/benchmark wizards require no chang...- Derived classes now specify single source and target folder paths.
- Target folder path is specified by default as '.'.
- Supports copying files and folders from the source folder path.
- CIF examples/benchmark wizards require no changes for new examples.
Closes #448v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/418#446 CIF: Equal/Unequal on combination of ints and reals is inconsistent2022-12-15T19:43:03ZFerdie Reijnen#446 CIF: Equal/Unequal on combination of ints and reals is inconsistentCloses #446Closes #446https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/402#444 Configure JDT formatter preferences per project2022-11-07T20:29:46ZDennis Hendriks#444 Configure JDT formatter preferences per project- Moved JDT formatter settings from Oomph setup to project settings.
- Apply formatter settings to all projects. For metamodel projects, used a limited subset only.
- Reformatted all projects
- `TwinCatWriter`: also rewrapped.
- `Twi...- Moved JDT formatter settings from Oomph setup to project settings.
- Apply formatter settings to all projects. For metamodel projects, used a limited subset only.
- Reformatted all projects
- `TwinCatWriter`: also rewrapped.
- `TwinCatWriter`: also fixed a duplicate 'may' word in the comment.
- Updated Eclipse upgrade instructions.
- Updated and improved/fixed formatter settings part.
- Improved/fixed error/warning settings part.
I recommend reviewing per commit.
Closes #444v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/416#442 Include textual position info in CIF check violation messages.2022-11-19T14:00:07ZDennis Hendriks#442 Include textual position info in CIF check violation messages.This uses the suggestion from https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/442#note_1038341 to still have position information for `null` specifications as report object. It does lead to a change in `CifPreconditionChecker`, t...This uses the suggestion from https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/442#note_1038341 to still have position information for `null` specifications as report object. It does lead to a change in `CifPreconditionChecker`, two `toString` overloads and a more complicated implementation of `toString(Specification spec)` than in https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/442#note_1038279. Let me know whether you prefer this implementation or the simpler one.
Also let me know what you think of the result for users, as visible in the changed test output.
Closes #442v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/396#441 DEPENDENCIES.txt update.2022-10-22T10:17:53ZDennis Hendriks#441 DEPENDENCIES.txt update.Closes #441Closes #441v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/393#440 Add CifCheckNoCompDefInst check baseclass.2022-10-19T10:49:27ZAlbert Hofkamp#440 Add CifCheckNoCompDefInst check baseclass.Closes #440Closes #440v0.8Albert HofkampAlbert Hofkamphttps://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/391#439 Get rid of references to 'receive(d) variables'.2022-10-17T06:34:42ZDennis Hendriks#439 Get rid of references to 'receive(d) variables'.Closes #439Closes #439v0.8https://gitlab.eclipse.org/eclipse/escet/escet/-/merge_requests/390#438 Various small JavaDoc/documentation fixes/improvements.2022-10-17T06:33:55ZDennis Hendriks#438 Various small JavaDoc/documentation fixes/improvements.- `{link` -> `{@link`
- `{code` -> `{@code`
- `Whether the evaluate` -> `Whether to evaluate`
- `positiveCount: count >= 0` -> `nonNegativeCount: count >= 0`
- `<code>...</code>` -> `{@code ...}` where possible.
Closes #438- `{link` -> `{@link`
- `{code` -> `{@code`
- `Whether the evaluate` -> `Whether to evaluate`
- `positiveCount: count >= 0` -> `nonNegativeCount: count >= 0`
- `<code>...</code>` -> `{@code ...}` where possible.
Closes #438v0.8