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

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,103 @@ 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 ComponentInstance {
+  string component_name = 1;
+  uint32 component_index = 2;
 }
 
-message StateTuple {
-  message LocationTuple {
-    string name = 1;
-    // Maybe the component name? or some comp id?
+message Clock {
+  message ComponentClock {
+    ComponentInstance component_instance = 1;
+    string clock_name = 2;
+  }
+  message SystemClock {
+    uint32 clock_index = 1;
+  }
+  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 (always has a valuation of 0)
+    ZeroClock zero_clock = 3;
   }
-  LocationTuple location = 1;
-  repeated Zone federation = 2;
 }
 
-message Transition {
-  // Figure out what we need here
-  // repeated Edge edges = 1; //?
+
+message Constraint {
+  // This message represents if (strict) { x - y < c } else { x - y <= c }
+  Clock x = 1;
+  Clock y = 2;
+  bool strict = 3;
+  int32 c = 4;
 }
+
+message Conjunction {
+  repeated Constraint constraints = 1;
+}
+
+message Disjunction {
+  repeated Conjunction conjunctions = 1;
+}
+
+// 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;
+  ComponentInstance component_instance = 2;
+}
+
+// A combination/pair of locations separated by a binary operator (conjunction, composition, quotient, refinement)
+message BinaryLocationOperator {
+  LocationTree left = 1;
+  LocationTree right = 2;
+  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;
+    BinaryLocationOperator binary_location_op = 2;
+    SpecialLocation special_location = 3;
+  }
+}
+
+message State {
+  LocationTree location_tree = 1;
+  Disjunction zone = 2;
+}
+
+message Edge {
+  string id = 1;
+  ComponentInstance component_instance = 2;
+}
+
+message Decision {
+  // Only one transition should be possible for the given state and action
+  State source = 1;
+  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 {
+  repeated Decision decisions = 1;
+}

query.proto

@@ -9,56 +9,188 @@ 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;
 }
 
-message Query {
-  int32 id = 1;
-  string query = 2;
-  IgnoredInputOutputs ignored_input_outputs = 3;
+message QueryRequest {
+  int32 user_id = 1;
+  int32 query_id = 2;
+  string query = 3;
+  ComponentsInfo components_info = 4;
+
+  message Settings {
+    bool disable_clock_reduction = 1;
+  }
+
+  Settings settings = 6;
 }
-message QueryRequest { repeated Query queries = 1; }
 
-message ComponentsUpdateRequest {
-  repeated Component components = 2;
-  int32 etag = 3; // hash
+message StateAction {
+  State state = 1;
+  string action = 2;
 }
 
-message QueryResponse {
-  Query query = 1;
+enum NoInitialState {
+  NO_INITIAL_STATE = 0;
+}
 
-  message RefinementResult {
-    bool success = 1;
-    repeated StateTuple relation = 2;
+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 {
+  int32 query_id = 1;
 
   message ComponentResult { Component component = 1; }
-  message ConsistencyResult { bool success = 1; }
-  message DeterminismResult { bool success = 1; }
-  message ImplementationResult { bool success = 1; }
+
+  message RefinementFailure {
+    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 {
+    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 {
+    string system = 1;
+    // The determinism check failed in this state for this action
+    StateAction failure_state = 2;
+  }
+
+  message ImplementationFailure {
+    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;
+
+    oneof failure {
+      // 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 {
+    Path path = 4;
+  }
+
+  message Success {
+
+  }
+
+  message Error {
+    string error = 1;
+  }
+
+  message ParsingError {
+    string error = 1;
+  }
 
   oneof result {
-    RefinementResult refinement = 3;
-    ComponentResult component = 4;
-    ConsistencyResult consistency = 5;
-    DeterminismResult determinism = 6;
-    string error = 7;
-    ImplementationResult implementation = 8;
+    Component component = 2;
+    ConsistencyFailure consistency = 3;
+    DeterminismFailure determinism = 4;
+    ImplementationFailure implementation = 5;
+    ReachabilityFailure reachability = 6;
+    RefinementFailure refinement = 7;
+    ReachabilityPath reachability_path = 8;
+
+    ParsingError parsing_error = 98;
+    ModelFailure model = 99;
+    Success success = 100;
+    Error error = 101;
+  }
+
+  message Information {
+    enum Severity {
+      INFO = 0;
+      WARNING = 1;
+    }
+    Severity severity = 1;
+    string subject = 2;
+    string message = 3;
   }
+  repeated Information info = 200;
 }
 
 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;
+  // 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 {
+  int32 user_id = 1;
+  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);
 }