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

Update query failures and support simulation of systems with quotients #13

Merged
merged 4 commits into from
Mar 10, 2023
Merged

Update query failures and support simulation of systems with quotients #13

merged 4 commits into from
Mar 10, 2023

Conversation

seblund
Copy link
Member

@seblund seblund commented Mar 1, 2023

There were a bunch of query failures that were not included in the initial future-proofing. This PR adds the distinct ways that i imagine queries can fail. I think this is almost exhaustive, so it should be enough for a while.

To support simulation and reachability paths where quotients are used in the systems it was necessary to change the LocationTuples to be a tree structure in States. This is because quotient adds new locations (Universal & Error) that can only really be represented with a tree structure (see below).

By the theory for a system (A\\B) \\ C:

One state could look like:
           \\
         /    \
       \\      L0
      /   \
    L1    L2

Another state could look like:
           \\
         /    \
       \\      L0
        |
       Uni

Another state could look like:
           \\
            |
           Err

These are all nicely represented by trees.

On the Reveaal side, deserialization and serialization is actually much easier with the tree structure. I would hope that the same applies for the GUI.

Nielswps
Nielswps requested changes Mar 6, 2023
View reviewed changes
Copy link
Contributor

@Nielswps Nielswps left a comment

Choose a reason for hiding this comment

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

I had some minor naming suggestions, but all-in-all, a great structure for the ProtoBuf 👍 I suspect that the others have some opinions on the naming I have commented.

In regards to the GUI, there are quite a few things to update, but I think you might be right that the (de-)serialization might actually be easier with the tree structure 😉 And having this updated ProtoBuf definitely adds a lot of great features in terms of debugging, error messaging, and supporting the user in fixing potential issues ❤️

objects.proto Outdated
}

// A specific location in a specific component
message LeafLocation {
string id = 1;
SpecificComponent specific_component = 2;
Copy link
Contributor

Choose a reason for hiding this comment

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

I assume that SpecificComponent refers to a specific instance of a component, in cases where the same component is referenced multiple times in a query, right?
Personally, I prefer ComponentInstance in that case

objects.proto Outdated
message LocationTuple {
repeated Location locations = 1;
// A combination/pair of locations
message BranchLocation {
Copy link
Contributor

Choose a reason for hiding this comment

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

I am not a big fan of BranchLocation. It does represent a branching out, but it is not a location itself. Maybe LocationFork, which signals that the location tree is forked at the given node?

Copy link
Contributor

Choose a reason for hiding this comment

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

While I agree on a name change, personally, I'd prefer InnerLocation since they represent inner nodes, and would conform more with LeafLocation 😄.

objects.proto Outdated
message BranchLocation {
LocationTree left = 1;
LocationTree right = 2;
// Could include composition type too? (e.g. Conjunction, Composition, Quotient, Refinement)
Copy link
Contributor

Choose a reason for hiding this comment

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

Should we add this?

t-lohse
t-lohse approved these 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 agree with @Nielswps' comments, So I think they should be handled. Otherwise, LGTM nice work 💪

Nielswps
Nielswps approved these changes Mar 10, 2023
View reviewed changes
Copy link
Contributor

@Nielswps Nielswps left a comment

Choose a reason for hiding this comment

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

Great!

@seblund seblund merged commit f6a55b9 into futureproof1 Mar 10, 2023
t-lohse added a commit that referenced this pull request Aug 23, 2023
@seblund @mads256h
@CasperStaahl @Archdragon79 @lugialukas @Sigurd00 @lass5588 @t-lohse @Puvikaran2001 @Mati-AAU @mksm20 @Nielswps
The SW5 changes to protobuf along with futureproofing from the dev te…
053d7e9 
…am (#12)

* Added the changes discussed in GRPC comittee

See document

* Change simulation api to support a stateless solution

* Change State to have a location_id instead of LocationTuple and unnest Zone

* Add UserTokenError

Changed query response to either return a query if the userid is
accepted, or send an error along with the ID.
Removed optional keyword due to default settings in proto3

* Added string reason on results for some detail

* Add changes discussed with Sebastian

* Update protocol as discussed by Sebastian

* Change objects.proto:
 - Remove unused messages
 - Change "string component_name" to "SpecificComponent specific_component" in Location
 - Unest Location from LocationTuple

* Remove unused message Transition

* - Rename Zone to Federation, which is the correct term
- Remove and replace StateTuple with State

* Add comment with alternative Simulation API

* Change to alternative simulation api, as dicussed with the GUI group

* Format

* Update query.proto

* Readd reason to quries

* Fix indexes

* Remove commented code

* Remove SimulationState message, was not in use

* Remove unused fields, readd edges toReachabilityResult

* Revert "Remove unused fields, readd edges toReachabilityResult"

This reverts commit ce77f23.

* re-add edges to message ReachabilityResult

* Added action string to determinism, consitency and refinement queries. (#11)

* Added action string to determinism, consitency and refinement queries.

* Changed refinement action from 4 to 5.

* Settings (#10)

* query

* fix optional

* proto

* proto

* init

* name change

* Clock settings refactor (#13)

* query

* fix optional

* proto

* proto

* init

* name change

* Refactor

* Refactor

* Changed name

* Clock settings (#14)

* query

* fix optional

* proto

* proto

* init

* name change

* Refactor

* Refactor

* Changed name

* refactor

* Added comments

* Refactor

* group 17 reachability gRPC changes (#12)

This pull request makes some changes to the reachability result.

Instead of result a list of edges as a path for each component combined, we have made a new message called Path that represents the path from a start state to an end state for the individual component.

Therefore in the message ReachabilityResult, we result a list of paths - one path for each individual component.

Co-authored-by: Mati-AAU <[email protected]>

* Simulation user id and nondeterminism for ambiguous edge choices.

* Remove UserTokenError (#15)

This was broken because it required Reveaal to store all the user tokens
that is has given out. This violates the principle of idempotency. The
server cannot know when a user id is no longer in use, because we have
no "log out" endpoint and even if we had one the client could crash and
thus not send out a "log out" message.

Instead we assume that all clients are well behaved and use GetUserToken
to get a token that is not in use.

* action is now a repeated string, not a string!

* Clock height (#18)

* query

* fix optional

* proto

* proto

* init

* name change

* Refactor

* Refactor

* Changed name

* refactor

* Added comments

* Refactor

* Clock heights

* Naming

* Naming

* Attempt to futureproof protobuf

* Update failures to encompass the different ways that queries can fail

* Change location tuples to a tree structure to support simulation of quotient (Universal and Error in quotient require it)

* Add destination state to all Decision structs

* Rename LocationBranch and SpecificComponent to better names

* Rename Zero message to ZeroClock

* Remove federation message as it is just a wrapper. Disjunction is also more general

* Update query.proto

Co-authored-by: Thomas Lohse <[email protected]>

* Add full_state info to simulation step response (#14)

---------

Co-authored-by: Mads Mogensen <[email protected]>
Co-authored-by: Casper Ståhl <[email protected]>
Co-authored-by: Archdragon <[email protected]>
Co-authored-by: lugialukas <[email protected]>
Co-authored-by: Sigurd <[email protected]>
Co-authored-by: Lasse Andersen <[email protected]>
Co-authored-by: Thomas Lohse <[email protected]>
Co-authored-by: Puvikaran Santhirasegaram <[email protected]>
Co-authored-by: Mati-AAU <[email protected]>
Co-authored-by: mksm20 <[email protected]>
Co-authored-by: mksm20 <[email protected]>
Co-authored-by: Niels F. S. Vistisen <[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

@Nielswps Nielswps Nielswps approved these changes

@Brandhoej Brandhoej Awaiting requested review from Brandhoej

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

Successfully merging this pull request may close these issues.
3 participants
@seblund @Nielswps @t-lohse