Protobuf

TACoS supports protobuf as input and output format (both binary and pbtxt) for automata and formulas. This page explains TACoS' protocol format.

Timed Automata

See ta.proto for the full specification and railroad/plant.pbtxt for a full example.

The timed automata protobuf format is specified in the tacos.automata.ta.proto package.

Locations

Locations are specified as repeated strings.

automata {
  locations: "OPEN"
  locations: "CLOSING"
  locations: "CLOSED"
  locations: "OPENING"
  final_locations: "CLOSED"
  final_locations: "OPEN"
  initial_location: "OPEN"
}

This creates an automaton with four locations, of which OPEN and CLOSED are final locations, and OPEN is the initial location.

Alphabet

The alphabet of an automaton also needs to be explicitly specified with the repeated string alphabet, e.g.:

  alphabet: "start_close"
  alphabet: "finish_close"
  alphabet: "start_open"
  alphabet: "finish_open"

Clocks

Clocks are specified as repeated strings, e.g.:

  clocks: "c1"
  clocks: "c2"

Transitions

Transitions are sub-messages of timed automata and consist of a source, a target, a symbol, repeated clock_constraints, and repeated clock_resets, where

• source and target are strings that must match a location of the TA
• symbol is a string that is part of the alphabet
• clock_resets is a repeated string, specifying a subset of the automaton's clocks
• clock_constraints is a repeated ClockConstraint message

  transitions {
    source: "CLOSING"
    target: "CLOSED"
    symbol: "finish_close"
    clock_constraints { clock: "c1" operand: EQUAL_TO comparand: 2 }
    clock_resets: "c1"
    clock_resets: "c2"
  }

Clock Constraints

A clock constraint consists of

• a clock name as string
• an operand, which is an enum and must be one of LESS, LESS_EQUAL, EQUAL_TO, GREATER_EQUAL, or GREATER.
• a comparand of type uint32 As an example,

clock_constraints { clock: "c1" operand: LESS_EQUAL comparand: 2 }

specifies to the constraint c1 <= 2.

Product Automata

A ProductAutomaton is simply a message that contains repeated automata of type TimedAutomaton. Note that the tacos main binary expects a product automaton, therefore you can simply put multiple automata in the plant specification:

automata {
  locations: "OPEN"
  locations: "CLOSING"
  locations: "CLOSED"
  locations: "OPENING"
  ...
}
automata {
  locations: "FAR"
  locations: "NEAR"
  locations: "IN"
  locations: "BEHIND"
  ...
}

This is the product of two automata with four locations each (transitions are omitted, see railroad/plant.pbtxt for a full example).

MTL

See mtl.proto for the full specification and railroad/spec.pbtxt for a full example.

The MTLFormula message has a oneof field formula, which contains on of the possible formula types.

Constants

A constant value (true or false) can be specified with the Constant message type.

constant { value : TRUE }

AtomicFormula

An atomic formula consists of a string symbol:

atomic { symbol: "enter" }

ConjunctionFormula

A conjunction consists of repeated conjuncts, which in turn can be arbitrary formulas:

conjunction {
  conjuncts {
    constant { value: TRUE }
  }
  conjuncts {
    atomic { symbol: "enter" }
  }
  conjuncts {
    atomic { symbol: "leave" }
  }
}

DisjunctionFormula

A disjunction works the same as way as a conjunction, except that it consists of repeated disjuncts:

disjunction {
  disjuncts {
    constant { value: TRUE }
  }
  disjuncts {
    atomic { symbol: "enter" }
  }
  disjuncts {
    atomic { symbol: "leave" }
  }
}

NegationFormula

A NegationFormula message has a single field formula, which is the formula to be negated:

negation {
 formula { atomic { symbol: "leave" } }
}

Intervals and Endpoints

All temporal modalities have an optional Interval, which consists of the optional Endpoints lower and upper. Each Endpoint has a BoundType and a value:

interval {
  upper {
    value: 2
    bound_type: STRICT
  }
}

UntilFormula and DualUntilFormula

An UntilFormula and DualUntilFormula consist of sub-formulas front and back, and an optional Interval interval:

dual_until {
  front {
    atomic { symbol: "travel" }
  }
  back {
    negation {
     formula { atomic { symbol: "finish_open" } }
    }
  }
  interval { lower { value: 1 } }
}

which specifies the formula (enter ~U !(finish_close)).

FinallyFormula and GloballyFormula

Both FinallyFormula and GloballyFormula have a field formula and an optional interval:

finally {
  formula {
    atomic { symbol: "travel" }
  }
  interval {
    upper {
      value: 2
      bound_type: STRICT
    }
  }
}