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 254ff24..4f8e4d9 100644 --- a/objects.proto +++ b/objects.proto @@ -6,22 +6,63 @@ 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? +import "component.proto"; + +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 Federation { + Disjunction disjunction = 1; +} + +message Location { + string id = 1; + SpecificComponent specific_component = 2; +} + +message LocationTuple { + repeated Location locations = 1; +} + +message State { + LocationTuple location_tuple = 1; + Federation federation = 2; +} + +message DecisionPoint { + State source = 1; + repeated Edge edges = 2; } -message StateTuple { - message LocationTuple { - string name = 1; - // Maybe the component name? or some comp id? - } - LocationTuple location = 1; - repeated Zone federation = 2; +message Edge { + string id = 1; + SpecificComponent specific_component = 2; } -message Transition { - // Figure out what we need here - // repeated Edge edges = 1; //? +message Decision { + State source = 1; + Edge edge = 2; } diff --git a/query.proto b/query.proto index 9804c6c..1979ccb 100644 --- a/query.proto +++ b/query.proto @@ -14,51 +14,95 @@ message IgnoredInputOutputs { repeated string ignored_outputs = 2; } -message Query { - int32 id = 1; - string query = 2; - IgnoredInputOutputs ignored_input_outputs = 3; -} -message QueryRequest { repeated Query queries = 1; } -message ComponentsUpdateRequest { - repeated Component components = 2; - int32 etag = 3; // hash +message UserTokenResponse { + int32 user_id = 1; } -message QueryResponse { - Query query = 1; +message QueryRequest { + int32 user_id = 1; + int32 query_id = 2; + string query = 3; + ComponentsInfo components_info = 4; + IgnoredInputOutputs ignored_input_outputs = 5; + bool should_reduce_clocks = 6; +} - message RefinementResult { - bool success = 1; - repeated StateTuple relation = 2; +message QueryResponse { + oneof response { + QueryOk query_ok = 1; + UserTokenError user_token_error = 2; } - message ComponentResult { Component component = 1; } - message ConsistencyResult { bool success = 1; } - message DeterminismResult { bool success = 1; } - message ImplementationResult { bool success = 1; } - - oneof result { - RefinementResult refinement = 3; - ComponentResult component = 4; - ConsistencyResult consistency = 5; - DeterminismResult determinism = 6; - string error = 7; - ImplementationResult implementation = 8; + message QueryOk { + int32 query_id = 1; + + message RefinementResult { + bool success = 1; + 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; + State state = 3; + repeated Edge edges = 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 UserTokenError { + int32 user_id = 1; + string error_message = 2; +} + message SimulationStartRequest { - string system = 1; // e.g. "(A || B) && C" or "A<=B" + SimulationInfo simulation_info = 1; } message SimulationStepRequest { - StateTuple state = 1; - Transition transition = 2; + SimulationInfo simulation_info = 1; + Decision chosen_decision = 2; } message SimulationStepResponse { - StateTuple state = 1; - repeated Transition transitions = 2; + DecisionPoint new_decision_point = 1; +} + +message SimulationInfo { + string component_composition = 2; // example: A || B || A + ComponentsInfo components_info = 3; } diff --git a/services.proto b/services.proto index 0b12799..e6bf71e 100644 --- a/services.proto +++ b/services.proto @@ -6,13 +6,14 @@ 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"; 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 (SimulationStepResponse); + rpc TakeSimulationStep(SimulationStepRequest) returns (SimulationStepResponse); }