-
Notifications
You must be signed in to change notification settings - Fork 2
CPP API
A timed automaton (TA) in TACOS is a templated six-tuple consisting of
- a set of locations,
- an alphabet (a set of actions),
- a single initial location,
- a set of final locations,
- a set of clocks, and
- a set of transitions.
We use two template types to define the set of actions on transitions and atomic propositions (APs), which label locations. See here for a full example.
As clocks in timed automata are always running and the set of clocks is global (i.e., all locations consider the same set of clocks), only a set of APs is required to create a location. A location labeled with "INITIAL" (using std::string as the type for APs) is created by
auto loc1 = tacos::automata::ta::Location{"INITIAL"};Currently, locations do not allow invariant constraints.
The alphabet given as a set of (templated) actions contains all actions that can be used on discrete transitions for synchronization or validation of specifications.
The initial location represents the initial configuration. Implicitly, all clocks are initialized with the valuation 0.
All locations marked as being final.
Clocks are identified by strings and represent variables which evolve continuously with slope one.
Transitions allow switching the mode from one location to another (from source to target location) using an action action (which may be used for synchronization). Transitions may be guarded, i.e., a transition can only be taken if the clock valuations in the source location satisfy the set of clock constraints associated with the transition. Additionally, clocks may be reset to zero when taking a transition. A transition can be specified as
auto t = tacos::automata::ta::Transition{source, action, target, guard, reset};where source and target are locations, action is an action-type, guard is a set of clock constraints, and reset is a set of clocks (a set of std::string).
A clock constraint can be for instance to define a guarding condition for a discrete transition. A clock constraint always compares a clock to a valuation using the relation symbols <,<=,=,>=,> represented by the c++-types std::less, std::less_equal, std::equal, std::greater_equal, and std::greater. Clock constraints may only use integer values (even though the type is double for technical reasons). A clock constraint comparing a clock x to the valuation 3 can for instance be defined as
using namespace tacos::automata;
auto cc = ClockConstraint{"x",AtomicClockConstraintT<std::equal_to<Time>>(3)};We want to create a TA with two locations, where the second one is final and only reachable after two or more time units. Furthermore, the only clock x can be reset in the first location only after exactly one time unit. To be able to distinguish locations we use the APs of type integer "0" (first location) and "1" (second location) and appropriate actions on ("restart" and "turn_off") of type string on the transitions. The resulting automaton can be created by
using TA = tacos::automata::ta::TimedAutomaton<int, std::string>;
using Location = automata::ta::Location<int>;
using Transition = automata::ta::Transition<int, std::string>;
using tacos::automata::Time;
using tacos::automata::AtomicClockConstraintT;
auto automaton = TA{{Location{0}, Location{1}},
{"restart", "turn_off"},
Location{0},
{Location{1}},
{"x"},
{
Transition(Location{0},
"restart",
Location{0},
{{"x", AtomicClockConstraintT<std::equal<Time>>(1)}},
{"x"}),
Transition(Location{0},
"turn_off",
Location{1},
{{"x", AtomicClockConstraintT<std::greater_equal<Time>>(2)}},
{})
}
};Formulas in metric temporal logic (MTL) in TACoS are used as a specification for controller synthesis. MTL formulas over atomic propositions (APs, template type) are composed recursively using negation, conjunction, disjunction, until, and dual until operators.
We use the usual c++-operators as much as possible with the usual semantics (see here for examples).
The single terms (assuming std::string as a type for APs) can be created (from the namespace tacos::logic) as follows (we assume the atomic propositions a and b have been created before):
- atomic propositions:
auto ap = AtomicProposition<std::string>("a"); - negation:
auto not_a = !a; - conjunction:
auto a_and_b = a && b; - disjunction:
auto a_or_b = a || b; - until:
auto a_until_b = a.until(b); - bounded until (satisfied in [1,2]):
auto a_until_b = a.until(b,{1,2}); - bounded dual until (satisfied in [3,4]):
auto a_until_b = a.dual_until(b,[3,4]);
We use the constant MTLFormula::TRUE() to derive syntactic sugar, e.g., tacos::logic::finally(a,bound) and tacos::logic::globally(a,bound) where a is an MTL-Formula and bound is a time interval (tacos::utilities::arithmetic::Interval).
We can validate timed words (sequences of tuples of atomic propositions and time points) against MTL-specifications:
tacos::logic::AtomicProposition<std::string> a{"a"};
tacos::logic::AtomicProposition<std::string> b{"b"};
tacos::logic::MTLWord<std::string> word = {{{a}, 1},{{b}, 2},{{a}, 3}};
bool a_true_at_one = word.satisfies(tacos::logic::finally(a, tacos::logic::TimeInterval{1,1}));MTL-formulas can be brought to positive normal form using the member-function to_positive_normal_form(), which recursively moves all negations inside the subformulas using standard transformations.
To synthesize a controller, given a plant and an MTL-specification, TACOS employs the approach presented by Bouyer et al.. The method operates in several stages. We assume spec to be a MTL-formula over the set of atomic propositions actions and plant to be a timed automaton. The set of actions can be partitioned in uncontrollable environment actions and controllable controller actions.
- The MTL-specification is transformed into an alternating timed automaton (ATA)
[...]
auto spec_ata = tacos::mtl_ata_translation::translate(spec, actions);
- An exhaustive search is performed on the product automaton of the TA and the ATA (created internally), nodes in the resulting search tree are labelled throughout the process (whether the specification is satisfied in the respective subtree, or not)
[...]
auto spec_ata = tacos::mtl_ata_translation::translate(spec, actions);
// determines the largest constant used in the TA and in the ATA
std::size_t K = std::max(plant.get_largest_constant(), spec.get_largest_constant());
// the last parameter enables incremental labeling during search,
// otherwise searcher.label() needs to be called
auto searcher = tacos::TreeSearch{plant,spec_ata,controller_actions,environment_actions,K,true};
// build search tree, label directly. The passed flag enables multithreading if set to true.
searcher.build_tree(false);- The resulting search tree is traversed to create a controller in case the specification can be satisfied in the root node.
[...]
// build search tree, label directly. The passed flag enables multithreading if set to true.
searcher.build_tree(false);
// construct controller from resulting search tree
auto controller = controller_synthesis::create_controller(searcher.get_root(),
controller_actions,
environment_actions,
K);