The SW5 changes to protobuf along with futureproofing from the dev team #12

seblund · 2023-02-09T09:45:09Z

Changes the protobuf to be more future proof, should contain most things to support future features

See document

…t Zone

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

…-simulation

…lation Improve gRPC committee changes

This reverts commit ce77f23.

Added the changes discussed in GRPC comittee

#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

* query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name

* query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name * refactor * Added comments * Refactor

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.

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!

* query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name * refactor * Added comments * Refactor * Clock heights * Naming * Naming

…uotient (Universal and Error in quotient require it)

Update query failures and support simulation of systems with quotients

Nielswps

Just some minor thoughts, looks great!

I am still kind of bumped about versioning, even though (hopefully) nothing will break. We will just create a GitHub release when this is merged, as discussed. It will be nice to have the ability to reference what version is currently used in the README.mds for future developers, even though the code itself is oblivious.

Nielswps · 2023-03-10T17:34:36Z

objects.proto

+  message SystemClock {
+    uint32 clock_index = 1;
+  }
+  message Zero {}


Should we rename this to ZeroClock for consistency? Its purpose is pretty obvious in the way it is used, but maybe it would be nice to make it explicit

I agree, it has been changed now :)

Nielswps · 2023-03-10T17:34:49Z

objects.proto

+    // When a clock is not attached to a component
+    SystemClock system_clock = 2;
+    // The zero clock
+    Zero zero = 3;


See comment above

Nielswps · 2023-03-10T17:35:54Z

objects.proto

+message Federation {
+  Disjunction disjunction = 1;
+}


Is a Federation just a wrapper for a disjunction?

Yes, I have changed it to use a disjunction instead now. It's also much nicer to just use a disjunction because it is more general, e.g. if we switch to CDDs in the future, it still makes sense to represent them by a disjunction.

…o more general

Nielswps

Very nice! I will hopefully get started on merging the refactoring and these changes into the simulation branch of the GUI repo sometime next week ✌️

query.proto

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

t-lohse

LGTM

mads256h and others added 30 commits October 5, 2022 11:19

Added the changes discussed in GRPC comittee

f3aec2c

See document

Change simulation api to support a stateless solution

9401b2a

Change State to have a location_id instead of LocationTuple and unnes…

9212549

…t Zone

Add UserTokenError

4619ab6

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

Merge pull request #5 from Ecdar-SW5/grpc-comittee-changes_stateless-…

c32d276

…simulation Change simulation api to support a stateless solution

Added string reason on results for some detail

71baaad

Merge pull request #6 from Ecdar-SW5/query-response-details

5b0edd2

Added reason on results for some detail

Add changes discussed with Sebastian

173c656

Update protocol as discussed by Sebastian

d0e37a3

Change objects.proto:

4d15d86

- Remove unused messages - Change "string component_name" to "SpecificComponent specific_component" in Location - Unest Location from LocationTuple

Remove unused message Transition

f13e0b2

- Rename Zone to Federation, which is the correct term

92aa3cc

- Remove and replace StateTuple with State

Add comment with alternative Simulation API

c5d9e4b

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

890f245

Format

d7438af

Merge branch 'grpc-comittee-changes' into grpc-comitte-changes_update…

9256766

…-simulation

Update query.proto

50e5b1d

Readd reason to quries

e8fd380

Fix indexes

e93c2b0

Remove commented code

d6b7355

Remove SimulationState message, was not in use

cea3465

Merge pull request #8 from Ecdar-SW5/grpc-comitte-changes_update-simu…

506305d

…lation Improve gRPC committee changes

Remove unused fields, readd edges toReachabilityResult

ce77f23

Revert "Remove unused fields, readd edges toReachabilityResult"

9a6acd4

This reverts commit ce77f23.

re-add edges to message ReachabilityResult

476edf4

Merge pull request #4 from Ecdar-SW5/grpc-comittee-changes

c181269

Added the changes discussed in GRPC comittee

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

21c0d2d

#11) * Added action string to determinism, consitency and refinement queries. * Changed refinement action from 4 to 5.

Settings (#10)

f2e2308

* query * fix optional * proto * proto * init * name change

Clock settings refactor (#13)

79d1da2

* query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name

Clock settings (#14)

c48ba74

* query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name * refactor * Added comments * Refactor

Puvikaran2001 and others added 11 commits November 18, 2022 10:40

Simulation user id and nondeterminism for ambiguous edge choices.

f41d85a

Merge pull request #16 from Ecdar-SW5/Simulation_API_update

674a904

Simulation user id and nondeterminism for ambiguous edge choices.

action is now a repeated string, not a string!

31f6acb

Merge pull request #17 from Ecdar-SW5/actionToVec

fa3ed0a

action is now a repeated string, not a string!

Clock height (#18)

e42e35d

* query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name * refactor * Added comments * Refactor * Clock heights * Naming * Naming

Attempt to futureproof protobuf

f054b3e

Update failures to encompass the different ways that queries can fail

481c16f

Change location tuples to a tree structure to support simulation of q…

a6d842f

…uotient (Universal and Error in quotient require it)

Add destination state to all Decision structs

7684645

Nielswps mentioned this pull request Mar 6, 2023

Preparation for simulation #5

Closed

seblund added 2 commits March 10, 2023 14:04

Rename LocationBranch and SpecificComponent to better names

2a1dbd3

Merge pull request #13 from Ecdar/futureproof2

f6a55b9

Update query failures and support simulation of systems with quotients

seblund requested a review from Nielswps March 10, 2023 14:55

Nielswps reviewed Mar 10, 2023

View reviewed changes

seblund added 2 commits March 10, 2023 19:05

Rename Zero message to ZeroClock

676ab79

Remove federation message as it is just a wrapper. Disjunction is als…

ae8364e

…o more general

Nielswps approved these changes Mar 10, 2023

View reviewed changes

t-lohse requested changes May 18, 2023

View reviewed changes

query.proto Outdated Show resolved Hide resolved

Update query.proto

9b9ce8f

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

t-lohse approved these changes May 18, 2023

View reviewed changes

Add full_state info to simulation step response (#14)

6fdef5f

t-lohse merged commit 053d7e9 into main Aug 23, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

The SW5 changes to protobuf along with futureproofing from the dev team #12

The SW5 changes to protobuf along with futureproofing from the dev team #12

seblund commented Feb 9, 2023

Nielswps left a comment •

edited

Loading

Nielswps Mar 10, 2023

seblund Mar 10, 2023

Nielswps Mar 10, 2023

Nielswps Mar 10, 2023

seblund Mar 10, 2023 •

edited

Loading

Nielswps left a comment

t-lohse left a comment

The SW5 changes to protobuf along with futureproofing from the dev team #12

The SW5 changes to protobuf along with futureproofing from the dev team #12

Conversation

seblund commented Feb 9, 2023

Nielswps left a comment • edited Loading

Choose a reason for hiding this comment

Nielswps Mar 10, 2023

Choose a reason for hiding this comment

seblund Mar 10, 2023

Choose a reason for hiding this comment

Nielswps Mar 10, 2023

Choose a reason for hiding this comment

Nielswps Mar 10, 2023

Choose a reason for hiding this comment

seblund Mar 10, 2023 • edited Loading

Choose a reason for hiding this comment

Nielswps left a comment

Choose a reason for hiding this comment

t-lohse left a comment

Choose a reason for hiding this comment

Nielswps left a comment •

edited

Loading

seblund Mar 10, 2023 •

edited

Loading