From f3aec2c50f9fa511d971019cb1ef0124b48bba35 Mon Sep 17 00:00:00 2001 From: Mads Mogensen Date: Wed, 5 Oct 2022 11:19:48 +0200 Subject: [PATCH 01/25] Added the changes discussed in GRPC comittee See document --- objects.proto | 61 +++++++++++++++++++++++++++++++++++++++++++----- query.proto | 63 ++++++++++++++++++++++++++++++++++++-------------- services.proto | 8 +++++-- 3 files changed, 107 insertions(+), 25 deletions(-) diff --git a/objects.proto b/objects.proto index 254ff24..87a280b 100644 --- a/objects.proto +++ b/objects.proto @@ -6,12 +6,6 @@ option java_multiple_files = false; option java_package = "EcdarProtoBuf"; option java_outer_classname = "ObjectProtos"; -message Zone { - int32 dimensions = 1; - repeated int32 matrix = 2; - // Maybe include a lookup table for the indices? -} - message StateTuple { message LocationTuple { string name = 1; @@ -25,3 +19,58 @@ message Transition { // Figure out what we need here // repeated Edge edges = 1; //? } + +message SpecificComponent { + string component_name = 1; + uint32 component_index = 2; +} + +message Zone { + message Disjunction { + message Conjunction { + message Constraint { + message ComponentClock { + SpecificComponent specific_component = 1; + string clock_name = 2; + } + // This message represents if (!strict) { x - y <= c } else { x - y < c } + ComponentClock x = 1; + ComponentClock y = 2; + bool strict = 3; + int32 c = 4; + } + repeated Constraint constraints = 1; + } + + repeated Conjunction conjunctions = 1; + } + Disjunction disjunction = 1; +} + +message LocationTuple { + message Location { + string id = 1; + string component_name = 2; + } + repeated Location locations = 1; +} + +message State { + LocationTuple location_tuple = 1; + Zone zone = 2; +} + +message DecisionPoint { + State source = 1; + repeated Edge edges = 2; +} + +message Edge { + string id = 1; + SpecificComponent specific_component = 2; +} + +message Decision { + State source = 1; + Edge edge = 2; +} diff --git a/query.proto b/query.proto index 9804c6c..b57b7db 100644 --- a/query.proto +++ b/query.proto @@ -14,30 +14,49 @@ message IgnoredInputOutputs { repeated string ignored_outputs = 2; } -message Query { - int32 id = 1; - string query = 2; - IgnoredInputOutputs ignored_input_outputs = 3; +message ComponentsInfo { + repeated Component components = 1; + uint32 components_hash = 2; } -message QueryRequest { repeated Query queries = 1; } -message ComponentsUpdateRequest { - repeated Component components = 2; - int32 etag = 3; // hash +message UserTokenResponse { + int32 user_id = 1; +} + +message QueryRequest { + int32 user_id = 1; + int32 query_id = 2; + string query = 3; + ComponentsInfo components_info = 4; + IgnoredInputOutputs ignored_input_outputs = 5; } message QueryResponse { - Query query = 1; + int32 query_id = 1; message RefinementResult { bool success = 1; repeated StateTuple relation = 2; + optional StateTuple state = 3; } message ComponentResult { Component component = 1; } - message ConsistencyResult { bool success = 1; } - message DeterminismResult { bool success = 1; } - message ImplementationResult { bool success = 1; } + message ConsistencyResult { + bool success = 1; + optional StateTuple state = 2; + } + message DeterminismResult { + bool success = 1; + optional StateTuple state = 2; + } + message ImplementationResult { + bool success = 1; + optional StateTuple state = 2; + } + message ReachabilityResult { + bool success = 1; + repeated Edge edges = 2; + } oneof result { RefinementResult refinement = 3; @@ -46,19 +65,29 @@ message QueryResponse { DeterminismResult determinism = 6; string error = 7; ImplementationResult implementation = 8; + ReachabilityResult reachability = 9; } } message SimulationStartRequest { - string system = 1; // e.g. "(A || B) && C" or "A<=B" + string component_composition = 1; // example: A || B || A + ComponentsInfo components_info = 2; +} + +message SimulationStartResponse { + int32 simulation_id = 1; + DecisionPoint initial_decision_point = 2; } message SimulationStepRequest { - StateTuple state = 1; - Transition transition = 2; + int32 simulation_id = 1; + Decision decision = 2; } message SimulationStepResponse { - StateTuple state = 1; - repeated Transition transitions = 2; + repeated DecisionPoint new_possible_decision_points = 1; +} + +message SimulationStopRequest { + int32 simulation_id = 1; } diff --git a/services.proto b/services.proto index 0b12799..09843d0 100644 --- a/services.proto +++ b/services.proto @@ -13,6 +13,10 @@ import "query.proto"; import "google/protobuf/empty.proto"; service EcdarBackend { - rpc UpdateComponents(ComponentsUpdateRequest) returns (google.protobuf.Empty); - rpc SendQuery(Query) returns (QueryResponse); + rpc GetUserToken(google.protobuf.Empty) returns (UserTokenResponse); + rpc SendQuery(QueryRequest) returns (QueryResponse); + + rpc StartSimulation(SimulationStartRequest) returns (SimulationStartResponse); + rpc TakeSimulationStep(SimulationStepRequest) returns (SimulationStepResponse); + rpc StopSimulation(SimulationStopRequest) returns (google.protobuf.Empty); } From 9401b2a912fb92775b748e9421bce33e7ab8f37d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 5 Oct 2022 23:41:03 +0200 Subject: [PATCH 02/25] Change simulation api to support a stateless solution --- objects.proto | 7 +++++++ query.proto | 17 ++++------------- services.proto | 3 +-- 3 files changed, 12 insertions(+), 15 deletions(-) diff --git a/objects.proto b/objects.proto index 87a280b..cd10dc9 100644 --- a/objects.proto +++ b/objects.proto @@ -6,6 +6,8 @@ option java_multiple_files = false; option java_package = "EcdarProtoBuf"; option java_outer_classname = "ObjectProtos"; +import "component.proto"; + message StateTuple { message LocationTuple { string name = 1; @@ -74,3 +76,8 @@ message Decision { State source = 1; Edge edge = 2; } + +message SimulationState { + Component component = 1; + repeated DecisionPoint decision_points = 2; +} diff --git a/query.proto b/query.proto index b57b7db..e36bec1 100644 --- a/query.proto +++ b/query.proto @@ -74,20 +74,11 @@ message SimulationStartRequest { ComponentsInfo components_info = 2; } -message SimulationStartResponse { - int32 simulation_id = 1; - DecisionPoint initial_decision_point = 2; -} - message SimulationStepRequest { - int32 simulation_id = 1; - Decision decision = 2; + SimulationState current_state = 1; + Decision chosen_decision = 2; } message SimulationStepResponse { - repeated DecisionPoint new_possible_decision_points = 1; -} - -message SimulationStopRequest { - int32 simulation_id = 1; -} + SimulationState new_state = 1; +} \ No newline at end of file diff --git a/services.proto b/services.proto index 09843d0..d8eb8c1 100644 --- a/services.proto +++ b/services.proto @@ -16,7 +16,6 @@ service EcdarBackend { rpc GetUserToken(google.protobuf.Empty) returns (UserTokenResponse); rpc SendQuery(QueryRequest) returns (QueryResponse); - rpc StartSimulation(SimulationStartRequest) returns (SimulationStartResponse); + rpc StartSimulation(SimulationStartRequest) returns (SimulationStepResponse); rpc TakeSimulationStep(SimulationStepRequest) returns (SimulationStepResponse); - rpc StopSimulation(SimulationStopRequest) returns (google.protobuf.Empty); } From 9212549108560c8e0bb159163919fddb78eca72d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Thu, 6 Oct 2022 15:08:45 +0200 Subject: [PATCH 03/25] Change State to have a location_id instead of LocationTuple and unnest Zone --- objects.proto | 40 +++++++++++++++++++++------------------- 1 file changed, 21 insertions(+), 19 deletions(-) diff --git a/objects.proto b/objects.proto index cd10dc9..074e8e0 100644 --- a/objects.proto +++ b/objects.proto @@ -26,26 +26,28 @@ message SpecificComponent { string component_name = 1; uint32 component_index = 2; } +message ComponentClock { + SpecificComponent specific_component = 1; + string clock_name = 2; +} + +message Constraint { + // This message represents if (!strict) { x - y <= c } else { x - y < c } + ComponentClock x = 1; + ComponentClock y = 2; + bool strict = 3; + int32 c = 4; +} + +message Conjunction { + repeated Constraint constraints = 1; +} + +message Disjunction { + repeated Conjunction conjunctions = 1; +} message Zone { - message Disjunction { - message Conjunction { - message Constraint { - message ComponentClock { - SpecificComponent specific_component = 1; - string clock_name = 2; - } - // This message represents if (!strict) { x - y <= c } else { x - y < c } - ComponentClock x = 1; - ComponentClock y = 2; - bool strict = 3; - int32 c = 4; - } - repeated Constraint constraints = 1; - } - - repeated Conjunction conjunctions = 1; - } Disjunction disjunction = 1; } @@ -58,7 +60,7 @@ message LocationTuple { } message State { - LocationTuple location_tuple = 1; + string location_id = 1; Zone zone = 2; } From 4619ab6b6b34a41226631438b10bf21993262746 Mon Sep 17 00:00:00 2001 From: Archdragon Date: Fri, 7 Oct 2022 10:02:38 +0200 Subject: [PATCH 04/25] 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 --- query.proto | 76 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 44 insertions(+), 32 deletions(-) diff --git a/query.proto b/query.proto index b57b7db..e481aaa 100644 --- a/query.proto +++ b/query.proto @@ -31,42 +31,54 @@ message QueryRequest { IgnoredInputOutputs ignored_input_outputs = 5; } -message QueryResponse { - int32 query_id = 1; - - message RefinementResult { - bool success = 1; - repeated StateTuple relation = 2; - optional StateTuple state = 3; +message QueryResponse { + oneof response { + QueryOk query_ok = 1; + UserTokenError user_token_error = 2; } - message ComponentResult { Component component = 1; } - message ConsistencyResult { - bool success = 1; - optional StateTuple state = 2; - } - message DeterminismResult { - bool success = 1; - optional StateTuple state = 2; - } - message ImplementationResult { - bool success = 1; - optional StateTuple state = 2; - } - message ReachabilityResult { - bool success = 1; - repeated Edge edges = 2; + message QueryOk { + int32 query_id = 1; + + message RefinementResult { + bool success = 1; + repeated StateTuple relation = 2; + StateTuple state = 3; + } + + message ComponentResult { Component component = 1; } + message ConsistencyResult { + bool success = 1; + StateTuple state = 2; + } + message DeterminismResult { + bool success = 1; + StateTuple state = 2; + } + message ImplementationResult { + bool success = 1; + StateTuple state = 2; + } + message ReachabilityResult { + bool success = 1; + repeated Edge edges = 2; + } + + oneof result { + RefinementResult refinement = 3; + ComponentResult component = 4; + ConsistencyResult consistency = 5; + DeterminismResult determinism = 6; + string error = 7; + ImplementationResult implementation = 8; + ReachabilityResult reachability = 9; + } } +} - oneof result { - RefinementResult refinement = 3; - ComponentResult component = 4; - ConsistencyResult consistency = 5; - DeterminismResult determinism = 6; - string error = 7; - ImplementationResult implementation = 8; - ReachabilityResult reachability = 9; - } +message UserTokenError { + int32 user_id = 1; + string error_message = 2; } message SimulationStartRequest { From 71baaade29f69887c6d2bbb61efa3eb437732688 Mon Sep 17 00:00:00 2001 From: Sigurd Date: Tue, 11 Oct 2022 09:49:37 +0200 Subject: [PATCH 05/25] Added string reason on results for some detail --- query.proto | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/query.proto b/query.proto index 7344ce8..c4186ce 100644 --- a/query.proto +++ b/query.proto @@ -43,25 +43,30 @@ message QueryResponse { message RefinementResult { bool success = 1; repeated StateTuple relation = 2; - StateTuple state = 3; + string reason = 3; + StateTuple state = 4; } message ComponentResult { Component component = 1; } message ConsistencyResult { bool success = 1; - StateTuple state = 2; + string reason = 2; + StateTuple state = 3; } message DeterminismResult { bool success = 1; - StateTuple state = 2; + string reason = 2; + StateTuple state = 3; } message ImplementationResult { bool success = 1; - StateTuple state = 2; + string reason = 2; + StateTuple state = 3; } message ReachabilityResult { bool success = 1; - repeated Edge edges = 2; + string reason = 2; + StateTuple state = 3; } oneof result { From 173c65690179a788260dd5f7b5d3f7126e5bbcb9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 12 Oct 2022 15:03:26 +0200 Subject: [PATCH 06/25] Add changes discussed with Sebastian --- component.proto | 5 +++++ objects.proto | 7 ++++--- query.proto | 4 ---- services.proto | 2 -- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/component.proto b/component.proto index 5943d50..3182b95 100644 --- a/component.proto +++ b/component.proto @@ -13,6 +13,11 @@ message Component { } } +message ComponentsInfo { + repeated Component components = 1; + uint32 components_hash = 2; +} + /* message Location { string id = 1; diff --git a/objects.proto b/objects.proto index 074e8e0..eda300d 100644 --- a/objects.proto +++ b/objects.proto @@ -60,7 +60,7 @@ message LocationTuple { } message State { - string location_id = 1; + LocationTuple location_id = 1; Zone zone = 2; } @@ -80,6 +80,7 @@ message Decision { } message SimulationState { - Component component = 1; - repeated DecisionPoint decision_points = 2; + string component_composition = 1; + ComponentsInfo components = 2; + repeated DecisionPoint decision_points = 3; } diff --git a/query.proto b/query.proto index 7344ce8..899d26b 100644 --- a/query.proto +++ b/query.proto @@ -14,10 +14,6 @@ message IgnoredInputOutputs { repeated string ignored_outputs = 2; } -message ComponentsInfo { - repeated Component components = 1; - uint32 components_hash = 2; -} message UserTokenResponse { int32 user_id = 1; diff --git a/services.proto b/services.proto index d8eb8c1..e6bf71e 100644 --- a/services.proto +++ b/services.proto @@ -6,8 +6,6 @@ option java_multiple_files = false; option java_package = "EcdarProtoBuf"; option java_outer_classname = "ServiceProtos"; -import "component.proto"; -import "objects.proto"; import "query.proto"; import "google/protobuf/empty.proto"; From d0e37a325b366192300d8953fe92a3aabd545c93 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 12 Oct 2022 15:43:19 +0200 Subject: [PATCH 07/25] Update protocol as discussed by Sebastian --- objects.proto | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/objects.proto b/objects.proto index eda300d..fe477eb 100644 --- a/objects.proto +++ b/objects.proto @@ -60,7 +60,7 @@ message LocationTuple { } message State { - LocationTuple location_id = 1; + LocationTuple location_tuple = 1; Zone zone = 2; } @@ -81,6 +81,6 @@ message Decision { message SimulationState { string component_composition = 1; - ComponentsInfo components = 2; + ComponentsInfo components_info = 2; repeated DecisionPoint decision_points = 3; } From 4d15d868cbc550f547cd5fa160fc3c42afd2570b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 12 Oct 2022 20:41:44 +0200 Subject: [PATCH 08/25] Change objects.proto: - Remove unused messages - Change "string component_name" to "SpecificComponent specific_component" in Location - Unest Location from LocationTuple --- objects.proto | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/objects.proto b/objects.proto index fe477eb..0393e5b 100644 --- a/objects.proto +++ b/objects.proto @@ -51,11 +51,12 @@ message Zone { Disjunction disjunction = 1; } +message Location { + string id = 1; + SpecificComponent specific_component = 2; +} + message LocationTuple { - message Location { - string id = 1; - string component_name = 2; - } repeated Location locations = 1; } From f13e0b20736afabf12b510942f589ed80408bae5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Thu, 13 Oct 2022 11:02:21 +0200 Subject: [PATCH 09/25] Remove unused message Transition --- objects.proto | 5 ----- 1 file changed, 5 deletions(-) diff --git a/objects.proto b/objects.proto index 0393e5b..785cdd2 100644 --- a/objects.proto +++ b/objects.proto @@ -17,11 +17,6 @@ message StateTuple { repeated Zone federation = 2; } -message Transition { - // Figure out what we need here - // repeated Edge edges = 1; //? -} - message SpecificComponent { string component_name = 1; uint32 component_index = 2; From 92aa3ccd6942ba22757c3e7bedcf07fb3b1000c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Thu, 13 Oct 2022 11:11:28 +0200 Subject: [PATCH 10/25] - Rename Zone to Federation, which is the correct term - Remove and replace StateTuple with State --- objects.proto | 13 ++----------- query.proto | 10 +++++----- 2 files changed, 7 insertions(+), 16 deletions(-) diff --git a/objects.proto b/objects.proto index 785cdd2..b0519f3 100644 --- a/objects.proto +++ b/objects.proto @@ -8,15 +8,6 @@ option java_outer_classname = "ObjectProtos"; import "component.proto"; -message StateTuple { - message LocationTuple { - string name = 1; - // Maybe the component name? or some comp id? - } - LocationTuple location = 1; - repeated Zone federation = 2; -} - message SpecificComponent { string component_name = 1; uint32 component_index = 2; @@ -42,7 +33,7 @@ message Disjunction { repeated Conjunction conjunctions = 1; } -message Zone { +message Federation { Disjunction disjunction = 1; } @@ -57,7 +48,7 @@ message LocationTuple { message State { LocationTuple location_tuple = 1; - Zone zone = 2; + Federation federation = 2; } message DecisionPoint { diff --git a/query.proto b/query.proto index 899d26b..2629566 100644 --- a/query.proto +++ b/query.proto @@ -38,22 +38,22 @@ message QueryResponse { message RefinementResult { bool success = 1; - repeated StateTuple relation = 2; - StateTuple state = 3; + repeated State relation = 2; + State state = 3; } message ComponentResult { Component component = 1; } message ConsistencyResult { bool success = 1; - StateTuple state = 2; + State state = 2; } message DeterminismResult { bool success = 1; - StateTuple state = 2; + State state = 2; } message ImplementationResult { bool success = 1; - StateTuple state = 2; + State state = 2; } message ReachabilityResult { bool success = 1; From c5d9e4b020cd0108ea9c3c18097e366b656fe962 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Thu, 13 Oct 2022 11:24:41 +0200 Subject: [PATCH 11/25] Add comment with alternative Simulation API --- query.proto | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/query.proto b/query.proto index 2629566..e29cdb8 100644 --- a/query.proto +++ b/query.proto @@ -89,4 +89,23 @@ message SimulationStepRequest { message SimulationStepResponse { SimulationState new_state = 1; -} \ No newline at end of file +} + +// --- ALTERNATIVE SIMULATION API --- +// message SimulationStartRequest { +// SimulationInfo simulation_info = 1; +// } + +// message SimulationStepRequest { +// SimulationInfo simulation_info = 1; +// Decision chosen_decision = 2; +// } + +// message SimulationStepResponse { +// DecisionPoint new_decision_point = 1; +// } + +// message SimulationInfo { +// string component_composition = 2; // example: A || B || A +// ComponentsInfo components_info = 3; +// } \ No newline at end of file From 890f245eb6548f1d5423c3e13e4c093f9d07784a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Fri, 14 Oct 2022 11:20:34 +0200 Subject: [PATCH 12/25] Change to alternative simulation api, as dicussed with the GUI group --- query.proto | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/query.proto b/query.proto index e29cdb8..0f8dd40 100644 --- a/query.proto +++ b/query.proto @@ -77,35 +77,35 @@ message UserTokenError { string error_message = 2; } -message SimulationStartRequest { - string component_composition = 1; // example: A || B || A - ComponentsInfo components_info = 2; -} - -message SimulationStepRequest { - SimulationState current_state = 1; - Decision chosen_decision = 2; -} - -message SimulationStepResponse { - SimulationState new_state = 1; -} - -// --- ALTERNATIVE SIMULATION API --- // message SimulationStartRequest { -// SimulationInfo simulation_info = 1; +// string component_composition = 1; // example: A || B || A +// ComponentsInfo components_info = 2; // } // message SimulationStepRequest { -// SimulationInfo simulation_info = 1; +// SimulationState current_state = 1; // Decision chosen_decision = 2; // } // message SimulationStepResponse { -// DecisionPoint new_decision_point = 1; +// SimulationState new_state = 1; // } -// message SimulationInfo { -// string component_composition = 2; // example: A || B || A -// ComponentsInfo components_info = 3; -// } \ No newline at end of file +// --- ALTERNATIVE SIMULATION API --- +message SimulationStartRequest { + SimulationInfo simulation_info = 1; +} + +message SimulationStepRequest { + SimulationInfo simulation_info = 1; + Decision chosen_decision = 2; +} + +message SimulationStepResponse { + DecisionPoint new_decision_point = 1; +} + +message SimulationInfo { + string component_composition = 2; // example: A || B || A + ComponentsInfo components_info = 3; +} \ No newline at end of file From d7438afc9e9eade914431c46a1e02114de2cabde Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Fri, 14 Oct 2022 11:27:37 +0200 Subject: [PATCH 13/25] Format --- objects.proto | 1 + 1 file changed, 1 insertion(+) diff --git a/objects.proto b/objects.proto index b0519f3..b14cf1d 100644 --- a/objects.proto +++ b/objects.proto @@ -12,6 +12,7 @@ message SpecificComponent { string component_name = 1; uint32 component_index = 2; } + message ComponentClock { SpecificComponent specific_component = 1; string clock_name = 2; From 50e5b1d630963e5777dd8fcf658a13630d9058a5 Mon Sep 17 00:00:00 2001 From: CasperStaahl Date: Tue, 18 Oct 2022 13:17:41 +0200 Subject: [PATCH 14/25] Update query.proto --- query.proto | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/query.proto b/query.proto index bf24483..772289c 100644 --- a/query.proto +++ b/query.proto @@ -58,7 +58,7 @@ message QueryResponse { message ReachabilityResult { bool success = 1; string reason = 2; - StateTuple state = 3; + State state = 3; } oneof result { @@ -109,4 +109,4 @@ message SimulationStepResponse { message SimulationInfo { string component_composition = 2; // example: A || B || A ComponentsInfo components_info = 3; -} \ No newline at end of file +} From e8fd38066f62b79aed735fb4491ec7912377f015 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Tue, 18 Oct 2022 13:32:33 +0200 Subject: [PATCH 15/25] Readd reason to quries --- query.proto | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/query.proto b/query.proto index 772289c..fbb4d55 100644 --- a/query.proto +++ b/query.proto @@ -39,20 +39,24 @@ message QueryResponse { message RefinementResult { bool success = 1; repeated State relation = 2; + string reason = 2; State state = 3; } message ComponentResult { Component component = 1; } message ConsistencyResult { bool success = 1; + string reason = 2; State state = 2; } message DeterminismResult { bool success = 1; + string reason = 2; State state = 2; } message ImplementationResult { bool success = 1; + string reason = 2; State state = 2; } message ReachabilityResult { From e93c2b0ca13bd152a707c391c289482e2e175faa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Tue, 18 Oct 2022 13:34:14 +0200 Subject: [PATCH 16/25] Fix indexes --- query.proto | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/query.proto b/query.proto index fbb4d55..4136e5d 100644 --- a/query.proto +++ b/query.proto @@ -39,25 +39,25 @@ message QueryResponse { message RefinementResult { bool success = 1; repeated State relation = 2; - string reason = 2; - State state = 3; + string reason = 3; + State state = 4; } message ComponentResult { Component component = 1; } message ConsistencyResult { bool success = 1; string reason = 2; - State state = 2; + State state = 3; } message DeterminismResult { bool success = 1; string reason = 2; - State state = 2; + State state = 3; } message ImplementationResult { bool success = 1; string reason = 2; - State state = 2; + State state = 3; } message ReachabilityResult { bool success = 1; From d6b73556eca8c8fd9dc9bacea247aa352499cbab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Tue, 18 Oct 2022 13:51:19 +0200 Subject: [PATCH 17/25] Remove commented code --- query.proto | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/query.proto b/query.proto index 4136e5d..9f2d888 100644 --- a/query.proto +++ b/query.proto @@ -82,21 +82,6 @@ message UserTokenError { string error_message = 2; } -// message SimulationStartRequest { -// string component_composition = 1; // example: A || B || A -// ComponentsInfo components_info = 2; -// } - -// message SimulationStepRequest { -// SimulationState current_state = 1; -// Decision chosen_decision = 2; -// } - -// message SimulationStepResponse { -// SimulationState new_state = 1; -// } - -// --- ALTERNATIVE SIMULATION API --- message SimulationStartRequest { SimulationInfo simulation_info = 1; } From cea346533469b54958152db975c486c8ec1b3ff5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 19 Oct 2022 08:20:13 +0200 Subject: [PATCH 18/25] Remove SimulationState message, was not in use --- objects.proto | 6 ------ 1 file changed, 6 deletions(-) diff --git a/objects.proto b/objects.proto index b14cf1d..4f8e4d9 100644 --- a/objects.proto +++ b/objects.proto @@ -66,9 +66,3 @@ message Decision { State source = 1; Edge edge = 2; } - -message SimulationState { - string component_composition = 1; - ComponentsInfo components_info = 2; - repeated DecisionPoint decision_points = 3; -} From ce77f23bceedf92de6ae0f9394005b9faced3710 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 19 Oct 2022 08:51:13 +0200 Subject: [PATCH 19/25] Remove unused fields, readd edges toReachabilityResult --- query.proto | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/query.proto b/query.proto index 9f2d888..f33b27f 100644 --- a/query.proto +++ b/query.proto @@ -38,31 +38,25 @@ message QueryResponse { message RefinementResult { bool success = 1; - repeated State relation = 2; - string reason = 3; - State state = 4; + string reason = 2; } - message ComponentResult { Component component = 1; } message ConsistencyResult { bool success = 1; string reason = 2; - State state = 3; } message DeterminismResult { bool success = 1; string reason = 2; - State state = 3; } message ImplementationResult { bool success = 1; string reason = 2; - State state = 3; } message ReachabilityResult { bool success = 1; string reason = 2; - State state = 3; + repeated Edge edges = 3; } oneof result { From 9a6acd41965e82a1495eca86124c892da7899db3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 19 Oct 2022 09:11:19 +0200 Subject: [PATCH 20/25] Revert "Remove unused fields, readd edges toReachabilityResult" This reverts commit ce77f23bceedf92de6ae0f9394005b9faced3710. --- query.proto | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/query.proto b/query.proto index f33b27f..9f2d888 100644 --- a/query.proto +++ b/query.proto @@ -38,25 +38,31 @@ message QueryResponse { message RefinementResult { bool success = 1; - string reason = 2; + repeated State relation = 2; + string reason = 3; + State state = 4; } + message ComponentResult { Component component = 1; } message ConsistencyResult { bool success = 1; string reason = 2; + State state = 3; } message DeterminismResult { bool success = 1; string reason = 2; + State state = 3; } message ImplementationResult { bool success = 1; string reason = 2; + State state = 3; } message ReachabilityResult { bool success = 1; string reason = 2; - repeated Edge edges = 3; + State state = 3; } oneof result { From 476edf494a04455434efd6f002b8f07976cbf98f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Wed, 19 Oct 2022 09:14:36 +0200 Subject: [PATCH 21/25] re-add edges to message ReachabilityResult --- query.proto | 1 + 1 file changed, 1 insertion(+) diff --git a/query.proto b/query.proto index 9f2d888..47c2019 100644 --- a/query.proto +++ b/query.proto @@ -63,6 +63,7 @@ message QueryResponse { bool success = 1; string reason = 2; State state = 3; + repeated Edge edges = 4; } oneof result { From 9930711bcda71c6d299d560097d10da14a76de8e Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 20 Oct 2022 11:18:25 +0200 Subject: [PATCH 22/25] query --- query.proto | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/query.proto b/query.proto index 47c2019..03649b1 100644 --- a/query.proto +++ b/query.proto @@ -25,6 +25,7 @@ message QueryRequest { string query = 3; ComponentsInfo components_info = 4; IgnoredInputOutputs ignored_input_outputs = 5; + optional bool should_reduce_clocks = 6; } message QueryResponse { @@ -75,6 +76,11 @@ message QueryResponse { ImplementationResult implementation = 8; ReachabilityResult reachability = 9; } + message Information { + string subject = 1; + string message = 2; + } + repeated Information info = 10; } } From 1d70bcfcff02ed7a3a63b3d6e923f811e7477065 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 20 Oct 2022 16:29:08 +0200 Subject: [PATCH 23/25] fix optional --- query.proto | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/query.proto b/query.proto index 03649b1..1979ccb 100644 --- a/query.proto +++ b/query.proto @@ -25,7 +25,7 @@ message QueryRequest { string query = 3; ComponentsInfo components_info = 4; IgnoredInputOutputs ignored_input_outputs = 5; - optional bool should_reduce_clocks = 6; + bool should_reduce_clocks = 6; } message QueryResponse { From 9451850470bdc283e99a13f21850caaa45d502ed Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 20 Oct 2022 16:48:42 +0200 Subject: [PATCH 24/25] proto --- query.proto | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/query.proto b/query.proto index 1979ccb..03649b1 100644 --- a/query.proto +++ b/query.proto @@ -25,7 +25,7 @@ message QueryRequest { string query = 3; ComponentsInfo components_info = 4; IgnoredInputOutputs ignored_input_outputs = 5; - bool should_reduce_clocks = 6; + optional bool should_reduce_clocks = 6; } message QueryResponse { From f99477b56fda2fac02002d352e2c3443190293a0 Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 20 Oct 2022 16:55:26 +0200 Subject: [PATCH 25/25] proto --- query.proto | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/query.proto b/query.proto index 03649b1..1979ccb 100644 --- a/query.proto +++ b/query.proto @@ -25,7 +25,7 @@ message QueryRequest { string query = 3; ComponentsInfo components_info = 4; IgnoredInputOutputs ignored_input_outputs = 5; - optional bool should_reduce_clocks = 6; + bool should_reduce_clocks = 6; } message QueryResponse {