An inline assertion describing the temporal behaviour of software.
Definition at line 67 of file tesla.proto.
Collaboration diagram for tesla::AutomatonDescription:Public Types | |
| enum | Context { Global = 1, ThreadLocal = 2 } |
| An automaton's context (e.g. More... | |
Public Attributes | |
| required Identifier | identifier = 1 |
| required Context | context = 2 |
| required Expression | expression = 3 |
| The temporal expression. More... | |
| repeated Argument | argument = 5 |
| Program variables referenced by the automaton. More... | |
An automaton's context (e.g.
thread-local) has implications for its storage and synchronization.
| Enumerator | |
|---|---|
| Global | |
| ThreadLocal | |
Definition at line 74 of file tesla.proto.
| repeated Argument tesla::AutomatonDescription::argument = 5 |
Program variables referenced by the automaton.
Definition at line 81 of file tesla.proto.
Referenced by tesla::Transition::Create().
| required Context tesla::AutomatonDescription::context = 2 |
Definition at line 75 of file tesla.proto.
Referenced by tesla::FieldInstrumentation::AppendInstrumentation(), and tesla::FnInstrumentation::AppendInstrumentation().
| required Expression tesla::AutomatonDescription::expression = 3 |
The temporal expression.
Definition at line 78 of file tesla.proto.
| required Identifier tesla::AutomatonDescription::identifier = 1 |
Definition at line 68 of file tesla.proto.
Referenced by tesla::Automaton::Automaton().
