Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refactor for query results and failures, new protobuf protocol, fixing simulation/reachability #147

Merged
merged 56 commits into from
Apr 6, 2023
Merged

Refactor for query results and failures, new protobuf protocol, fixing simulation/reachability #147

merged 56 commits into from
Apr 6, 2023

Conversation

seblund
Copy link
Member

@seblund seblund commented Mar 2, 2023

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:

  • Update protobuf to support:
    • Simulation of all system types (Quotient works now)
    • Cause of failure for all query types with as much information as possible
  • Add nice result enum types for every query and cause of failure
  • Introduce intermediate types between protobuf structs and TransitionSystem related structs (State, LocationTuple, Federation, etc.) with conversions between them (proto <=> intermediate <=> ts ).
  • Basically rewrite simulation as the only complicated part is serialization/deserialization of states
  • Change reachability to use the same Decision structs as in simulation

Most of the changes were to be able to serialize and deserialize States (Hence also LocationTuple and Federation). There are tests to ensure that the proto <=> intermediate <=> ts relation holds for thousands of different States from various systems.

@seblund
Ensure that components have the same file name as name field in json
e5d0777
@seblund
Add intermediate 'specific' structs between protobuf objects and Mode…
bb5399e 
…lObjects and their conversions into proto
@seblund
Introduce QueryResult enum with nicely structured query failures and …
d27db39 
…convenient from<T> conversions
@seblund
Add method to convert a transition system to a string
eae937b
@seblund
Add method to get a tree structure of the ComponentInfos in a Transit…
8203940 
…ionSystem
@seblund
Change proto branch to use the new definitions
50b0969
@seblund
Change Decision to be a state and action. Removing the need for Decis…
81fc378 
…ionPoint and its 3 variants
@seblund
Use new Decision struct in reachability paths
edb15a2
@seblund
Update 'specifics' to match new Proto definitions
5e71ba1
@seblund
Update query failures to use new specifics
85c236d
@seblund
Use new specifics and failures in ExecutableQueries
112182f
@seblund
Implement necessary protobuf conversions
8b0f5f0
@seblund
Use new result types in all TransitionSystem definitions
7f1eb03
@seblund
Use new result types in refinement, simplifying the code
c8cb39b
@seblund
Fix lib.rs and main.rs with new error types
2744fd6
@seblund
Add trivial check to fail reachability if states are empty
3244f84
@seblund
Update to use new error and result types
9701b6b
@seblund
Box parsing errors to avoid clippy warnings
5d56958
@seblund
Add utility method to State struct
dae4e77
@seblund
Simplify code
9e4d75d
@seblund
Use proto conversions from proto_conversions.rs to convert query results
7b94453
@seblund
Use new conversion methods in simulation backend implementation
ae8b4a7
@seblund
Fix benches after code changes
d16476f
@seblund
Update GRPC tests, removing confusing simulation tests (we'll replace…
30628ed 
… them with better ones)
@seblund
Change code to match edge formatting
affceb4
@seblund
Use new CompiledComponent::compile in tests, setting the component id…
dd7fb2e 
…s to 0
@seblund
Update simulation tests and remove confusing simulation test data (mo…
4f298ca 
…re confusing than helpful)
@seblund
Update refinement tests after result code changes
b0fc5d0
@seblund
Update reachability tests after refactor
c1e6375
@seblund
Update failure message tests after refactor
d08966a
@seblund seblund requested a review from t-lohse March 3, 2023 15:37
t-lohse
t-lohse requested changes Mar 9, 2023
View reviewed changes
Copy link
Contributor

@t-lohse t-lohse left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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! 💪

src/DataReader/proto_reader.rs Outdated Show resolved Hide resolved
src/ProtobufServer/ecdar_requests/send_query.rs Outdated Show resolved Hide resolved
src/ProtobufServer/ecdar_requests/send_query.rs Outdated Show resolved Hide resolved
src/System/extract_state.rs Outdated Show resolved Hide resolved
src/System/local_consistency.rs Outdated Show resolved Hide resolved
src/System/query_failures.rs Outdated Show resolved Hide resolved
src/System/query_failures.rs Show resolved Hide resolved
src/System/reachability.rs Show resolved Hide resolved
src/System/refine.rs Outdated Show resolved Hide resolved
src/System/specifics.rs Outdated Show resolved Hide resolved
@seblund
Copy link
Member Author

seblund commented Mar 9, 2023

I have resolved the conversations that I have fixed with these commits.
I have also added documentation to all structs/enums/funcs in specifics.rs and query_failures.rs.

I have now added issues for documentation in general and for consistent naming of build_* methods :)

t-lohse
t-lohse approved these changes Mar 10, 2023
View reviewed changes
Copy link
Contributor

@t-lohse t-lohse left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, very nice 😃

seblund and others added 2 commits March 18, 2023 20:00
@seblund
Update proto names and add BinaryOp type to binary op types
f1de065
@t-lohse
Clock reduction fix (#151)
ba0583e 
* clock reduction fix

* removed component

* fmt

* rename

* Added tests, along with refactor

* refactored unwrap

* Fixed error with locations
@seblund seblund linked an issue Mar 30, 2023 that may be closed by this pull request
Remove state field from the reachability result #139
Open
@seblund seblund merged commit a998584 into Ecdar-SW5/main Apr 6, 2023
@seblund seblund deleted the new_results_refactor branch April 6, 2023 15:32
seblund pushed a commit that referenced this pull request May 11, 2023
@t-lohse @Laursen79
@KiraStaehr @alexsteffensen @JE-FH
Advanced clock reduction (#147)
8ff768b 
* 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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@t-lohse t-lohse t-lohse approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Remove state field from the reachability result
2 participants
@seblund @t-lohse