query.proto

syntax = "proto3";

package EcdarProtoBuf;

option java_multiple_files = false;
option java_package = "EcdarProtoBuf";
option java_outer_classname = "QueryProtos";

import "component.proto";
import "objects.proto";

message UserTokenResponse {
  int32 user_id = 1;
}

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 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 {
  int32 query_id = 1;

  message ComponentResult { Component component = 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 SyntaxFailure {
    string msg = 1;
    string path = 2;
  }

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

  message ComponentsNotInCache {

  }

  oneof result {
    Component component = 2;
    ConsistencyFailure consistency = 3;
    DeterminismFailure determinism = 4;
    ImplementationFailure implementation = 5;
    ReachabilityFailure reachability = 6;
    RefinementFailure refinement = 7;
    ReachabilityPath reachability_path = 8;
    SyntaxFailure syntax = 9;
    
    ParsingError parsing_error = 98;
    ModelFailure model = 99;
    Success success = 100;
    Error error = 101;
    ComponentsNotInCache componentsNotInCache = 102;
  }

  message Information {
    enum Severity {
      INFO = 0;
      WARNING = 1;
    }
    Severity severity = 1;
    string subject = 2;
    string message = 3;
  }
  repeated Information info = 200;
}

message SimulationStartRequest {
  SimulationInfo simulation_info = 1;
}

message SimulationStepRequest {
  SimulationInfo simulation_info = 1;
  Decision chosen_decision = 2;
}

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 {
  int32 user_id = 1;
  string component_composition = 2; // example: A || B || A
  ComponentsInfo components_info = 3;
}