ta.proto

/***************************************************************************
 *  ta.proto - Protobuf for Timed Automata
 *
 *  Created:   Fri 19 Mar 10:37:37 CET 2021
 *  Copyright  2021  Till Hofmann <hofmann@kbsg.rwth-aachen.de>
 *  SPDX-License-Identifier: LGPL-3.0-or-later
 ****************************************************************************/

syntax = "proto3";

package tacos.automata.ta.proto;

message TimedAutomaton {
  message Transition {
    message ClockConstraint {
      enum Operand {
        LESS = 0;
        LESS_EQUAL = 1;
        EQUAL_TO = 2;
        GREATER_EQUAL = 4;
        GREATER = 5;
      }
      string clock = 1;
      Operand operand = 2;
      uint32 comparand = 3;
    }

    string source = 1;
    string target = 2;
    string symbol = 3;
    repeated ClockConstraint clock_constraints = 4;
    repeated string clock_resets = 5;
  }

  repeated string locations = 2;
  repeated string alphabet = 3;
  string initial_location = 4;
  repeated string final_locations = 5;
  repeated string clocks = 6;
  repeated Transition transitions = 7;
}

message ProductAutomaton { repeated TimedAutomaton automata = 1; }