Update query failures and support simulation of systems with quotients

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 {
@@ -53,23 +53,49 @@ 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;
+  ComponentInstance component_instance = 2;
 }
 
-message LocationTuple {
-  repeated Location locations = 1;
+// 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 {
-  LocationTuple 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 {
@@ -78,6 +104,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 {

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