Clock reduction

component.proto

@@ -13,6 +13,11 @@ message Component {
   }
 }
 
+message ComponentsInfo {
+  repeated Component components = 1;
+  uint32 components_hash = 2;
+}
+
 /*
 message Location {
     string id = 1;

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;
 }

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;
 }

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);
 }