Refactor for query results and failures, new protobuf protocol, fixing simulation/reachability #147
Conversation
…lObjects and their conversions into proto
…convenient from<T> conversions
…ionPoint and its 3 variants
… them with better ones)
…re confusing than helpful)
…g (only Simple or Special locations can be Universal/Inconsistent)
…oesn't improve performance)
There was a problem hiding this comment.
I have a few comments, not much.
I noticed a few things that I think should be fixed/implemented/changed, but may be out of scope for this PR, such as the LocationTuple. Unless I have misunderstood it, I think we should rename it to LocationTree.
This is something I have noticed throughou Reveaal, some naming could be better. For example, if I'm not misunderstanding, a Componenent is the representation of the automaton? So why not just call it an Automaton? This way it would translate better to/from j-Ecdar. I think we should let it "slip" for this PR, and make a refactor issue.
Beyond that, I think it would be beneficial to have some documentation. Again, this is an issue throughout Reveaal, so maybe just make an issue? Personally, I think it's necessary to have documentation for public structs, enums, and functions, as well as "large", private helper functions, but I am not sure how much. Do you have any input?
Overall, very nice PR! 💪
|
I have resolved the conversations that I have fixed with these commits. I have now added issues for documentation in general and for consistent naming of |
* clock reduction fix * removed component * fmt * rename * Added tests, along with refactor * refactored unwrap * Fixed error with locations
* started advanced cases * start_find_redundant_clocks * test setup, needs test examples * test setup, needs test examples * added test component * added get_transition * added test component for composition * added test component, and refactored file system for test components * Added find transition * Refactor * Name refactor * Where implementations * Some impl * Fixed compile error * Changed reduce_clocks prototype * Miss merge * added get_children_mut * Hardcoded clock reduction of clock y * Hardcoded clock reduction of clock y * merge * heights * compile * Test refactor * Warnings * working on clock reduction analyzer * Some debugging * Fixed Simon Deleuran Laursen's mistake * Fixed tests * Reduces * updated tests * Naming * can make graph from cyclic components, and cyclic component added. Updated .gitignore to ignore .ds_store file (generated by macos) * added guard dependencies to edges * Refactor * Test fix-ish * Removes from updates * Added invariant_dependencies to nodes and converted graph.nodes to a Hashmap instead of a Vec * fixed unused clock detection test * made clock reduction better * fixed naming * Fixed another test * Refactor * fixed another test * Fix error * merged advanced-clock-reduction * removed unnecessary mut * merged * Refactor * fixed tests * added processing to json component * added two test cases * added comments to find_equivalent_clock_groups * Fixed clock reduction tests in the simple cases * helper functions * fixed clock reduction * Error handling * fmt * working on test_check_declarations_unused_clock_are_removed * tiny refactor * start testfunc * Intersect * Small fixes * Fix removal * Added clock removal test for unused and duplicated clocks & removed advanced clock reduction samples * Fix warnings * Fixed SystemRecipe.height * Remove print * Fmt * Fixed comments Co-authored-by: Simon Laursen <[email protected]> Co-authored-by: Kira Stæhr Pedersen <[email protected]> Co-authored-by: Alexander Steffensen <[email protected]> Co-authored-by: alexsteffensen <[email protected]> Co-authored-by: Jens Emil Fink Højriis <[email protected]>
Large PR, sorry. Almost all changes depend on each other which resulted in changes all over the code base. I will do a walkthrough on request :)
Changes:
proto <=> intermediate <=> ts).Decisionstructs as in simulationMost of the changes were to be able to serialize and deserialize
States(Hence alsoLocationTupleandFederation). There are tests to ensure that theproto <=> intermediate <=> tsrelation holds for thousands of differentStatesfrom various systems.