From f3aec2c50f9fa511d971019cb1ef0124b48bba35 Mon Sep 17 00:00:00 2001 From: Mads Mogensen Date: Wed, 5 Oct 2022 11:19:48 +0200 Subject: [PATCH 01/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] - 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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/39] 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 21c0d2daaf36404ac4e9f2ec05a13959c792dcb0 Mon Sep 17 00:00:00 2001 From: Lasse Andersen Date: Wed, 9 Nov 2022 09:24:22 +0100 Subject: [PATCH 22/39] 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. --- query.proto | 3 +++ 1 file changed, 3 insertions(+) diff --git a/query.proto b/query.proto index 47c2019..f26a049 100644 --- a/query.proto +++ b/query.proto @@ -41,6 +41,7 @@ message QueryResponse { repeated State relation = 2; string reason = 3; State state = 4; + string action = 5; } message ComponentResult { Component component = 1; } @@ -48,11 +49,13 @@ message QueryResponse { bool success = 1; string reason = 2; State state = 3; + string action = 4; } message DeterminismResult { bool success = 1; string reason = 2; State state = 3; + string action = 4; } message ImplementationResult { bool success = 1; From f2e230876aa3c5386770ec6a20f04dc0a925dc8c Mon Sep 17 00:00:00 2001 From: Thomas Lohse <49527735+t-lohse@users.noreply.github.com> Date: Fri, 11 Nov 2022 09:22:01 +0100 Subject: [PATCH 23/39] Settings (#10) * query * fix optional * proto * proto * init * name change --- query.proto | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/query.proto b/query.proto index f26a049..cb9707a 100644 --- a/query.proto +++ b/query.proto @@ -25,6 +25,12 @@ message QueryRequest { string query = 3; ComponentsInfo components_info = 4; IgnoredInputOutputs ignored_input_outputs = 5; + + message Settings { + bool reduce_clocks = 1; + } + + Settings settings = 6; } message QueryResponse { @@ -78,6 +84,11 @@ message QueryResponse { ImplementationResult implementation = 8; ReachabilityResult reachability = 9; } + message Information { + string subject = 1; + string message = 2; + } + repeated Information info = 10; } } From 79d1da20cc5c29dd7a2545c2cef355a8e552fd01 Mon Sep 17 00:00:00 2001 From: Thomas Lohse <49527735+t-lohse@users.noreply.github.com> Date: Tue, 15 Nov 2022 13:25:18 +0100 Subject: [PATCH 24/39] Clock settings refactor (#13) * query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name --- query.proto | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/query.proto b/query.proto index cb9707a..1f00012 100644 --- a/query.proto +++ b/query.proto @@ -27,7 +27,7 @@ message QueryRequest { IgnoredInputOutputs ignored_input_outputs = 5; message Settings { - bool reduce_clocks = 1; + optional int32 reduce_clocks_level = 1; } Settings settings = 6; @@ -114,3 +114,4 @@ message SimulationInfo { string component_composition = 2; // example: A || B || A ComponentsInfo components_info = 3; } + From c48ba74408ff6a1769dfdd42bd8c40aab7417c9f Mon Sep 17 00:00:00 2001 From: Thomas Lohse <49527735+t-lohse@users.noreply.github.com> Date: Thu, 17 Nov 2022 14:16:43 +0100 Subject: [PATCH 25/39] Clock settings (#14) * query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name * refactor * Added comments * Refactor --- query.proto | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/query.proto b/query.proto index 1f00012..af7361a 100644 --- a/query.proto +++ b/query.proto @@ -27,7 +27,10 @@ message QueryRequest { IgnoredInputOutputs ignored_input_outputs = 5; message Settings { - optional int32 reduce_clocks_level = 1; + oneof reduce_clocks_level { + int32 Level = 1; // Specifies the level of the clock reduction + bool All = 2; // Determines if all (true) or nothing (false) should be clock reduced + } } Settings settings = 6; From 22f7b52a65a7dcf56563eb7b5d353ce4c47dd231 Mon Sep 17 00:00:00 2001 From: Puvikaran Santhirasegaram <74664443+Puvikaran2001@users.noreply.github.com> Date: Fri, 18 Nov 2022 10:40:35 +0100 Subject: [PATCH 26/39] 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 <74661610+Mati-AAU@users.noreply.github.com> --- objects.proto | 4 ++++ query.proto | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/objects.proto b/objects.proto index 4f8e4d9..8f858f4 100644 --- a/objects.proto +++ b/objects.proto @@ -66,3 +66,7 @@ message Decision { State source = 1; Edge edge = 2; } + +message Path { + repeated string edge_ids = 1; +} \ No newline at end of file diff --git a/query.proto b/query.proto index af7361a..a2e5352 100644 --- a/query.proto +++ b/query.proto @@ -75,7 +75,7 @@ message QueryResponse { bool success = 1; string reason = 2; State state = 3; - repeated Edge edges = 4; + repeated Path component_paths = 4; } oneof result { From f41d85a91e70980d8385b718d9edeb2c67c55914 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Casper=20St=C3=A5hl?= Date: Thu, 24 Nov 2022 11:11:56 +0100 Subject: [PATCH 27/39] Simulation user id and nondeterminism for ambiguous edge choices. --- query.proto | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/query.proto b/query.proto index a2e5352..2f98439 100644 --- a/query.proto +++ b/query.proto @@ -110,10 +110,11 @@ message SimulationStepRequest { } message SimulationStepResponse { - DecisionPoint new_decision_point = 1; + repeated DecisionPoint new_decision_points = 1; } message SimulationInfo { + int32 user_id = 1; string component_composition = 2; // example: A || B || A ComponentsInfo components_info = 3; } From c1d41acd0cde29599f0225536bea565d0d9c9589 Mon Sep 17 00:00:00 2001 From: Mads Mogensen Date: Fri, 25 Nov 2022 12:47:42 +0000 Subject: [PATCH 28/39] 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. --- query.proto | 104 +++++++++++++++++++++++----------------------------- 1 file changed, 46 insertions(+), 58 deletions(-) diff --git a/query.proto b/query.proto index 2f98439..4642013 100644 --- a/query.proto +++ b/query.proto @@ -36,68 +36,56 @@ message QueryRequest { Settings settings = 6; } -message QueryResponse { - oneof response { - QueryOk query_ok = 1; - UserTokenError user_token_error = 2; +message QueryResponse { + int32 query_id = 1; + + message RefinementResult { + bool success = 1; + repeated State relation = 2; + string reason = 3; + State state = 4; + string action = 5; } - message QueryOk { - int32 query_id = 1; - - message RefinementResult { - bool success = 1; - repeated State relation = 2; - string reason = 3; - State state = 4; - string action = 5; - } - - message ComponentResult { Component component = 1; } - message ConsistencyResult { - bool success = 1; - string reason = 2; - State state = 3; - string action = 4; - } - message DeterminismResult { - bool success = 1; - string reason = 2; - State state = 3; - string action = 4; - } - message ImplementationResult { - bool success = 1; - string reason = 2; - State state = 3; - } - message ReachabilityResult { - bool success = 1; - string reason = 2; - State state = 3; - repeated Path component_paths = 4; - } - - oneof result { - RefinementResult refinement = 3; - ComponentResult component = 4; - ConsistencyResult consistency = 5; - DeterminismResult determinism = 6; - string error = 7; - ImplementationResult implementation = 8; - ReachabilityResult reachability = 9; - } - message Information { - string subject = 1; - string message = 2; - } - repeated Information info = 10; + message ComponentResult { Component component = 1; } + message ConsistencyResult { + bool success = 1; + string reason = 2; + State state = 3; + string action = 4; + } + message DeterminismResult { + bool success = 1; + string reason = 2; + State state = 3; + string action = 4; + } + message ImplementationResult { + bool success = 1; + string reason = 2; + State state = 3; + } + message ReachabilityResult { + bool success = 1; + string reason = 2; + State state = 3; + repeated Path component_paths = 4; } -} -message UserTokenError { - int32 user_id = 1; - string error_message = 2; + oneof result { + RefinementResult refinement = 3; + ComponentResult component = 4; + ConsistencyResult consistency = 5; + DeterminismResult determinism = 6; + string error = 7; + ImplementationResult implementation = 8; + ReachabilityResult reachability = 9; + } + message Information { + string subject = 1; + string message = 2; + } + repeated Information info = 10; } message SimulationStartRequest { From 31f6acb2e4590bc33a2a6d73d4605a2707cc63e7 Mon Sep 17 00:00:00 2001 From: mksm20 Date: Tue, 29 Nov 2022 11:30:53 +0100 Subject: [PATCH 29/39] action is now a repeated string, not a string! --- query.proto | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/query.proto b/query.proto index 4642013..9b74b5f 100644 --- a/query.proto +++ b/query.proto @@ -44,7 +44,7 @@ message QueryResponse { repeated State relation = 2; string reason = 3; State state = 4; - string action = 5; + repeated string action = 5; } message ComponentResult { Component component = 1; } @@ -52,13 +52,13 @@ message QueryResponse { bool success = 1; string reason = 2; State state = 3; - string action = 4; + repeated string action = 4; } message DeterminismResult { bool success = 1; string reason = 2; State state = 3; - string action = 4; + repeated string action = 4; } message ImplementationResult { bool success = 1; From e42e35db63efacd7ab42aecd17c9a52b291c7be9 Mon Sep 17 00:00:00 2001 From: Thomas Lohse <49527735+t-lohse@users.noreply.github.com> Date: Mon, 5 Dec 2022 13:33:41 +0100 Subject: [PATCH 30/39] Clock height (#18) * query * fix optional * proto * proto * init * name change * Refactor * Refactor * Changed name * refactor * Added comments * Refactor * Clock heights * Naming * Naming --- query.proto | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/query.proto b/query.proto index 9b74b5f..a7078b8 100644 --- a/query.proto +++ b/query.proto @@ -27,12 +27,9 @@ message QueryRequest { IgnoredInputOutputs ignored_input_outputs = 5; message Settings { - oneof reduce_clocks_level { - int32 Level = 1; // Specifies the level of the clock reduction - bool All = 2; // Determines if all (true) or nothing (false) should be clock reduced - } + bool disable_clock_reduction = 1; } - + Settings settings = 6; } From f054b3e2efac875b9a87bc64a83f0dab65cd9ceb Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Thu, 9 Feb 2023 10:36:30 +0100 Subject: [PATCH 31/39] Attempt to futureproof protobuf --- objects.proto | 39 +++++++++++------ query.proto | 115 +++++++++++++++++++++++++++++++------------------- 2 files changed, 98 insertions(+), 56 deletions(-) diff --git a/objects.proto b/objects.proto index 8f858f4..55f96b3 100644 --- a/objects.proto +++ b/objects.proto @@ -13,15 +13,30 @@ message SpecificComponent { uint32 component_index = 2; } -message ComponentClock { - SpecificComponent specific_component = 1; - string clock_name = 2; +message Clock { + message ComponentClock { + SpecificComponent specific_component = 1; + string clock_name = 2; + } + message SystemClock { + uint32 clock_index = 1; + } + message Zero {} + oneof clock { + // When a clock is attached to a component + ComponentClock component_clock = 1; + // When a clock is not attached to a component + SystemClock system_clock = 2; + // The zero clock + Zero zero = 3; + } } + message Constraint { - // This message represents if (!strict) { x - y <= c } else { x - y < c } - ComponentClock x = 1; - ComponentClock y = 2; + // This message represents if (strict) { x - y < c } else { x - y <= c } + Clock x = 1; + Clock y = 2; bool strict = 3; int32 c = 4; } @@ -52,21 +67,19 @@ message State { Federation federation = 2; } -message DecisionPoint { - State source = 1; - repeated Edge edges = 2; -} - message Edge { string id = 1; SpecificComponent specific_component = 2; } message Decision { + // Only one transition should be possible for the given state and action State source = 1; - Edge edge = 2; + string action = 2; + // Only for GUI purposes + repeated Edge edges = 3; } message Path { - repeated string edge_ids = 1; + repeated Decision decisions = 1; } \ No newline at end of file diff --git a/query.proto b/query.proto index a7078b8..215e8d8 100644 --- a/query.proto +++ b/query.proto @@ -9,12 +9,6 @@ option java_outer_classname = "QueryProtos"; import "component.proto"; import "objects.proto"; -message IgnoredInputOutputs { - repeated string ignored_inputs = 1; - repeated string ignored_outputs = 2; -} - - message UserTokenResponse { int32 user_id = 1; } @@ -24,7 +18,6 @@ message QueryRequest { int32 query_id = 2; string query = 3; ComponentsInfo components_info = 4; - IgnoredInputOutputs ignored_input_outputs = 5; message Settings { bool disable_clock_reduction = 1; @@ -33,56 +26,92 @@ message QueryRequest { Settings settings = 6; } +message FailureContext { + string system = 1; + State state = 2; + string action = 3; +} + message QueryResponse { int32 query_id = 1; - message RefinementResult { - bool success = 1; - repeated State relation = 2; - string reason = 3; - State state = 4; - repeated string action = 5; + message ComponentResult { Component component = 1; } + + message RefinementFailure { + FailureContext context = 1; + ConsistencyFailure consistency = 4; } - message ComponentResult { Component component = 1; } - message ConsistencyResult { - bool success = 1; - string reason = 2; - State state = 3; - repeated string action = 4; + message ConsistencyFailure { + FailureContext context = 1; + DeterminismFailure determinism = 5; } - message DeterminismResult { - bool success = 1; - string reason = 2; - State state = 3; - repeated string action = 4; + message DeterminismFailure { + FailureContext context = 1; } - message ImplementationResult { - bool success = 1; - string reason = 2; - State state = 3; + message ImplementationFailure { + FailureContext context = 1; + ConsistencyFailure consistency = 5; } - message ReachabilityResult { - bool success = 1; - string reason = 2; - State state = 3; + message ModelFailure { + string system = 1; + + message ActionFailure { + enum Relation { + NOT_SUBSET = 1; + NOT_DISJOINT = 2; + } + message ActionSet { + string system = 1; + repeated string actions = 2; + } + Relation failure = 2; + repeated ActionSet action_sets = 3; + } + oneof failure { + ActionFailure action = 2; + ConsistencyFailure consistency = 3; + } + } + message ReachabilityFailure { + + } + + message ReachabilityPath { repeated Path component_paths = 4; } + message Success { + + } + message Error { + string error = 1; + } oneof result { - RefinementResult refinement = 3; - ComponentResult component = 4; - ConsistencyResult consistency = 5; - DeterminismResult determinism = 6; - string error = 7; - ImplementationResult implementation = 8; - ReachabilityResult reachability = 9; + Component component = 2; + ConsistencyFailure consistency = 3; + DeterminismFailure determinism = 4; + ImplementationFailure implementation = 5; + ReachabilityFailure reachability = 6; + RefinementFailure refinement = 7; + ReachabilityPath reachability_path = 8; + + ModelFailure model = 99; + Success success = 100; + Error error = 101; + } + message Information { - string subject = 1; - string message = 2; + enum Serverity { + INFO = 0; + WARNING = 1; + } + Serverity serverity = 1; + string subject = 2; + string message = 3; } - repeated Information info = 10; + repeated Information info = 200; } message SimulationStartRequest { @@ -95,7 +124,7 @@ message SimulationStepRequest { } message SimulationStepResponse { - repeated DecisionPoint new_decision_points = 1; + repeated Decision new_decision_points = 1; } message SimulationInfo { From 481c16f0892c79bfe034b7e7fd02baec97cb146e Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Wed, 1 Mar 2023 15:24:22 +0100 Subject: [PATCH 32/39] Update failures to encompass the different ways that queries can fail --- query.proto | 115 +++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 86 insertions(+), 29 deletions(-) diff --git a/query.proto b/query.proto index 215e8d8..78699fb 100644 --- a/query.proto +++ b/query.proto @@ -26,10 +26,27 @@ message QueryRequest { Settings settings = 6; } -message FailureContext { - string system = 1; - State state = 2; - string action = 3; +message StateAction { + State state = 1; + string action = 2; +} + +enum NoInitialState { + NO_INITIAL_STATE = 0; +} + +message ActionFailure { + enum Relation { + NOT_SUBSET = 0; + NOT_DISJOINT = 1; + } + message ActionSet { + string system = 1; + repeated string actions = 2; + bool is_input = 3; + } + Relation failure = 2; + repeated ActionSet action_sets = 3; } message QueryResponse { @@ -38,55 +55,96 @@ message QueryResponse { message ComponentResult { Component component = 1; } message RefinementFailure { - FailureContext context = 1; - ConsistencyFailure consistency = 4; + string system = 1; + + message RefinementStateFailure { + enum Unmatched { + DELAY = 0; + ACTION = 1; + } + Unmatched unmatched = 1; + StateAction state = 2; + } + + oneof failure { + // The refinement failed for an action in a specific state + RefinementStateFailure refinement_state = 2; + // The refinement failed because this system was empty + string empty_system = 3; + // The refinement failed because the initial state was empty + NoInitialState no_initial_state = 4; + // The refinement failed because a child was inconsistent + ConsistencyFailure inconsistent_child = 5; + // The refinement failed because the actions mismatched + ActionFailure action_mismatch = 6; + } } message ConsistencyFailure { - FailureContext context = 1; - DeterminismFailure determinism = 5; + string system = 1; + oneof failure { + // The consistency check failed because the initial state was empty + NoInitialState no_initial_state = 2; + // The consistency check failed because this state was not consistent + State failure_state = 3; + // The consistency check failed because the system is not deterministic + DeterminismFailure determinism = 4; + } } + message DeterminismFailure { - FailureContext context = 1; + string system = 1; + // The determinism check failed in this state for this action + StateAction failure_state = 2; } + message ImplementationFailure { - FailureContext context = 1; - ConsistencyFailure consistency = 5; + string system = 1; + oneof failure { + // The determinism check failed in this state for this action + StateAction failure_state = 2; + // The implementation check failed because the system was not consistent + ConsistencyFailure consistency = 3; + } } + message ModelFailure { string system = 1; - message ActionFailure { - enum Relation { - NOT_SUBSET = 1; - NOT_DISJOINT = 2; - } - message ActionSet { - string system = 1; - repeated string actions = 2; - } - Relation failure = 2; - repeated ActionSet action_sets = 3; - } oneof failure { - ActionFailure action = 2; - ConsistencyFailure consistency = 3; + // The check failed because the actions mismatched + ActionFailure action_mismatch = 2; + // The check failed because a conjunction was not consistent + ConsistencyFailure inconsistent_conjunction = 3; + // Some other model failure + string other = 4; } } + message ReachabilityFailure { - + enum Failure { + UNREACHABLE = 0; + } + + Failure failure = 1; } message ReachabilityPath { - repeated Path component_paths = 4; + Path path = 4; } + message Success { } + message Error { string error = 1; } + message ParsingError { + string error = 1; + } + oneof result { Component component = 2; ConsistencyFailure consistency = 3; @@ -96,10 +154,10 @@ message QueryResponse { RefinementFailure refinement = 7; ReachabilityPath reachability_path = 8; + ParsingError parsing_error = 98; ModelFailure model = 99; Success success = 100; Error error = 101; - } message Information { @@ -132,4 +190,3 @@ message SimulationInfo { string component_composition = 2; // example: A || B || A ComponentsInfo components_info = 3; } - From a6d842fdf9e3d8a67ec3c0a6ac161759180bd7aa Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Wed, 1 Mar 2023 15:27:12 +0100 Subject: [PATCH 33/39] Change location tuples to a tree structure to support simulation of quotient (Universal and Error in quotient require it) --- objects.proto | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/objects.proto b/objects.proto index 55f96b3..ce0f54a 100644 --- a/objects.proto +++ b/objects.proto @@ -53,17 +53,37 @@ message Federation { Disjunction disjunction = 1; } -message Location { + +// Should only be used when quotient adds new locations to the tree +enum SpecialLocation { + UNIVERSAL = 0; + ERROR = 1; +} + +// A specific location in a specific component +message LeafLocation { string id = 1; SpecificComponent specific_component = 2; } -message LocationTuple { - repeated Location locations = 1; +// A combination/pair of locations +message BranchLocation { + LocationTree left = 1; + LocationTree right = 2; + // Could include composition type too? (e.g. Conjunction, Composition, Quotient, Refinement) +} + +// A binary tree describing a location in a system. It has to be a tree to support the special locations from quotients +message LocationTree { + oneof node_type { + LeafLocation leaf_location = 1; + BranchLocation branch_location = 2; + SpecialLocation special_location = 3; + } } message State { - LocationTuple location_tuple = 1; + LocationTree location_tuple = 1; Federation federation = 2; } From 7684645445e77c3af1ff2a95ae1b0e87d6b87ff3 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Fri, 3 Mar 2023 15:54:01 +0100 Subject: [PATCH 34/39] Add destination state to all Decision structs --- objects.proto | 2 ++ 1 file changed, 2 insertions(+) diff --git a/objects.proto b/objects.proto index ce0f54a..a35a0c0 100644 --- a/objects.proto +++ b/objects.proto @@ -98,6 +98,8 @@ message Decision { string action = 2; // Only for GUI purposes repeated Edge edges = 3; + // The state that is reached if this decision is taken. Only for GUI purposes. + State destination = 4; } message Path { From 2a1dbd3a7afb7dd52f5beacbe190aaff44a77445 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Fri, 10 Mar 2023 14:04:17 +0100 Subject: [PATCH 35/39] Rename LocationBranch and SpecificComponent to better names --- objects.proto | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/objects.proto b/objects.proto index a35a0c0..07787ed 100644 --- a/objects.proto +++ b/objects.proto @@ -8,14 +8,14 @@ option java_outer_classname = "ObjectProtos"; import "component.proto"; -message SpecificComponent { +message ComponentInstance { string component_name = 1; uint32 component_index = 2; } message Clock { message ComponentClock { - SpecificComponent specific_component = 1; + ComponentInstance component_instance = 1; string clock_name = 2; } message SystemClock { @@ -63,33 +63,39 @@ enum SpecialLocation { // A specific location in a specific component message LeafLocation { string id = 1; - SpecificComponent specific_component = 2; + ComponentInstance component_instance = 2; } -// A combination/pair of locations -message BranchLocation { +// A combination/pair of locations separated by a binary operator (conjunction, composition, quotient, refinement) +message BinaryLocationOperator { LocationTree left = 1; LocationTree right = 2; - // Could include composition type too? (e.g. Conjunction, Composition, Quotient, Refinement) + enum Operator { + CONJUNCTION = 0; + COMPOSITION = 1; + QUOTIENT = 2; + REFINEMENT = 3; + } + Operator operator = 3; } // A binary tree describing a location in a system. It has to be a tree to support the special locations from quotients message LocationTree { oneof node_type { LeafLocation leaf_location = 1; - BranchLocation branch_location = 2; + BinaryLocationOperator binary_location_op = 2; SpecialLocation special_location = 3; } } message State { - LocationTree location_tuple = 1; + LocationTree location_tree = 1; Federation federation = 2; } message Edge { string id = 1; - SpecificComponent specific_component = 2; + ComponentInstance component_instance = 2; } message Decision { From 676ab79de815cb6d775a4c68526fa497a1582a01 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Fri, 10 Mar 2023 19:05:16 +0100 Subject: [PATCH 36/39] Rename Zero message to ZeroClock --- objects.proto | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/objects.proto b/objects.proto index 07787ed..4f5b6e4 100644 --- a/objects.proto +++ b/objects.proto @@ -21,14 +21,14 @@ message Clock { message SystemClock { uint32 clock_index = 1; } - message Zero {} + message ZeroClock {} oneof clock { // When a clock is attached to a component ComponentClock component_clock = 1; // When a clock is not attached to a component SystemClock system_clock = 2; - // The zero clock - Zero zero = 3; + // The zero clock (always has a valuation of 0) + ZeroClock zero_clock = 3; } } From ae8364e6c8942a5cfde24adec779ca87d4431e4a Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Fri, 10 Mar 2023 19:09:41 +0100 Subject: [PATCH 37/39] Remove federation message as it is just a wrapper. Disjunction is also more general --- objects.proto | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/objects.proto b/objects.proto index 4f5b6e4..8205134 100644 --- a/objects.proto +++ b/objects.proto @@ -49,11 +49,6 @@ message Disjunction { repeated Conjunction conjunctions = 1; } -message Federation { - Disjunction disjunction = 1; -} - - // Should only be used when quotient adds new locations to the tree enum SpecialLocation { UNIVERSAL = 0; @@ -90,7 +85,7 @@ message LocationTree { message State { LocationTree location_tree = 1; - Federation federation = 2; + Disjunction zone = 2; } message Edge { From 9b9ce8fd52c14916d110667147e6421255b0c54d Mon Sep 17 00:00:00 2001 From: "Niels F. S. Vistisen" <42961494+Nielswps@users.noreply.github.com> Date: Thu, 18 May 2023 12:51:42 +0200 Subject: [PATCH 38/39] Update query.proto Co-authored-by: Thomas Lohse <49527735+t-lohse@users.noreply.github.com> --- query.proto | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/query.proto b/query.proto index 78699fb..d125d11 100644 --- a/query.proto +++ b/query.proto @@ -161,11 +161,11 @@ message QueryResponse { } message Information { - enum Serverity { + enum Severity { INFO = 0; WARNING = 1; } - Serverity serverity = 1; + Severity severity = 1; string subject = 2; string message = 3; } From 6fdef5fe7434fec878ebc6c76a19da1a9a99c5f9 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Wed, 23 Aug 2023 16:22:52 +0200 Subject: [PATCH 39/39] Add full_state info to simulation step response (#14) --- query.proto | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/query.proto b/query.proto index d125d11..ab1e1df 100644 --- a/query.proto +++ b/query.proto @@ -182,7 +182,11 @@ message SimulationStepRequest { } message SimulationStepResponse { + // The full state that is reached after the simulation step + State full_state = 2; + // Possible decisions for subsets of the full state repeated Decision new_decision_points = 1; + } message SimulationInfo {