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.

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

Clock settings refactor #10

Closed
wants to merge 39 commits into from
Closed

Conversation

t-lohse
Copy link
Contributor

@t-lohse t-lohse commented Nov 15, 2022

No description provided.

mads256h and others added 30 commits October 5, 2022 11:19
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
…simulation

Change simulation api to support a stateless solution
Added reason on results for some detail
 - Remove unused messages
 - Change "string component_name" to "SpecificComponent specific_component" in Location
 - Unest Location from LocationTuple
- Remove and replace StateTuple with State
Added the changes discussed in GRPC comittee
t-lohse and others added 9 commits November 7, 2022 13:14
#11)

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

* Changed refinement action from 4 to 5.
* query

* fix optional

* proto

* proto

* init

* name change
@t-lohse t-lohse closed this Nov 15, 2022
t-lohse added a commit that referenced this pull request Aug 23, 2023
…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
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants