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 IgnoredInputOutputs {
  repeated string ignored_inputs = 1;
  repeated string ignored_outputs = 2;
}


message UserTokenResponse {
  int32 user_id = 1;
}

message QueryRequest {
  int32 user_id = 1;
  int32 query_id = 2;
  string query = 3;
  ComponentsInfo components_info = 4;
  IgnoredInputOutputs ignored_input_outputs = 5;

  message Settings {
    bool disable_clock_reduction = 1;
  }
  
  Settings settings = 6;
}

message QueryResponse {
  int32 query_id = 1;

  message RefinementResult {
    bool success = 1;
    repeated State relation = 2;
    string reason = 3;
    State state = 4;
    repeated string action = 5;
  }

  message ComponentResult { Component component = 1; }
  message ConsistencyResult {
    bool success = 1;
    string reason = 2;
    State state = 3;
    repeated string action = 4;
  }
  message DeterminismResult {
    bool success = 1;
    string reason = 2;
    State state = 3;
    repeated string action = 4;
  }
  message ImplementationResult {
    bool success = 1;
    string reason = 2;
    State state = 3;
  }
  message ReachabilityResult {
    bool success = 1;
    string reason = 2;
    State state = 3;
    repeated Path component_paths = 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 SimulationStartRequest {
  SimulationInfo simulation_info = 1;
}

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

message SimulationStepResponse {
  repeated DecisionPoint new_decision_points = 1;
}

message SimulationInfo {
  int32 user_id = 1;
  string component_composition = 2; // example: A || B || A
  ComponentsInfo components_info = 3;
}