Aalborg Tick Tock Automata Validator - an extendable verification engine and simulator for Tick Tock Automata.

TTA's (Tick Tock Automata) are an Automata based theory that can model parallel business logic for all kinds of automation systems. A TTA consists of a set of locations and transitions between them. Each transition can be guarded by a boolean expression and have a set of variable assignments as a "consequence" of taking the transition.

A good analogy to TTA is a statemachine, where a system can transition from one state to another. Below is an example of a simple TTA that controls a light based on a button input.

Starting in the OFF location, there's only one outgoing edge with the guard that checks if btn_is_pressed is true. If it is, we move to the ON location and set the variable light to true as a consequence of taking the edge/transition. Then, when the button is released we return to the OFF locaiton and light is set to false again.

What makes TTAs different from any other transition system is that the btn_is_pressed variable is an external variable, meaning that it cannot be assigned to any value by the transition system, it can only change based on an external input. External inputs are read when we are not taking transitions. This split of the semantics is where the name Tick Tock Automata comes from:

• Tick-step: evaluate guards, apply updates, change locations
• Tock-step: read external inputs, write external outputs

Taking the syntax one step further, you can have many of these TTAs running in parallel, sharing the same pool of internal and external variables. Such a network is called simply a network of tick tock automata (NTTA).

• This paper describes the base Tick Tock Automata theory
• This paper describes in detail the newest iteration of the tool (v1.0.0+)
• This paper describes the first iteration of the tool (v0.10.x)
• Take a look at H-UPPAAL if you want to create some TTAs yourself

Aaltitoad is built using cmake. You must have a C++20 compatible compiler, flex, bison version 3.5+ and the standard template library installed. All other dependencies are handled through the wonderful CPM package manager.

mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make

If the CPM step is taking a long time, try rerunning with -DCPM_SOURCE_CACHE=~/.cache/CPM

To run the unit tests, compile the aaltitoad_tests target

mkdir build-test && cd build-test
cmake -DCMAKE_BUILD_TYPE=Debug ..
make aaltitoad_tests
# run the tests
./aaltitoad_test -r xml -d yes --order lex

If you want to include code-coverage stats, provide the -DCODE_COVERAGE=ON cmake flag.

Aaltitoad provides three primary compilation targets. All commandline interfaces have a help page that you can summon with the --help argument.

• verifier: A verification engine command line interface
  • use this if you want to analyze your NTTA
• simulator: A runtime command line interface
  • use this if you want to execute your NTTA and link with your custom tockers (see below)
• aaltitoad: A library with all things aaltitoad
  • use this to create your own NTTA-based applications e.g. another verifier, runtime or even compiler

Aaltitoad supports third party "tocker" libraries, so you can inject custom integrations directly into the runtime. This repository provides an example tocker called pipe_tocker in the tocker_plugins directory to serve as an example project. A "tocker" must define the following symbols:

#include <plugin_system.h> // aaltitoad::* typedefs

extern "C" {
    const char* get_plugin_name(); // Return value of this func dictates the name the next two funcs
    aaltitoad::tocker_t* create_TOCKER_NAME(const std::string& argument, const aaltitoad::ntta_t& ntta);
    void destroy_TOCKER_NAME(tocker_t* tocker);
    plugin_type get_plugin_type() {
        return plugin_type::tocker;
    }
}

The TOCKER_NAME refers to the C-String provided by the get_plugin_name function. The function names MUST match, otherwise the plugin will not load. Tocker plugins must link with the aaltitoad shared library, and should be compiled as a shared library, like so:

add_library(TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries(TOCKER_NAME_tocker aaltitoad)

Once compiled, you can instantiate the tocker by providing the --tocker / -t together with --tocker-dir / -T to the aaltitoad command line. The --tocker option should be provided like so:

--tocker-dir /path/to/tocker-plugins --tocker "TOCKER_NAME(argument string)" 

The "argument string"-part of the option refers to the input argument string provided to the create_TOCKER_NAME function. Now your tockers should've been instantiated, and it's tock function will be called each time the TTA is ready to calculate tocker values.

There are two types of tocker interfaces that a third party tocker can extend:

• Blocking tockers (default tocker_t)
• Asynchronous tockers (async_tocker_t)

The blocking tocker will run in a single thread and will block all tick-execution until the tock has completed, and a third-party integration should only override the tock function. In contrast, the asynchronous tocker will not block tick execution, but start a new asynchronous task of the get_tock_values function.

When implementing your tocker, you should consider if you want to block the TTA from executing or not. If you choose to implement an asynchronous tocker, be aware that the input environment can have changed since the tock was issued.

If you don't want to use the included parser, you can always supply your own. As long as you provide the following symbols (remember extern "C"):

#include <plugin_system.h> // aaltitoad::* typedefs 

extern "C" {
    const char* get_plugin_name();
    const char* get_plugin_version();
    aaltitoad::ntta_t* load(const std::vector<std::string>& folders, const std::vector<std::string>& ignore_list);
    plugin_type get_plugin_type() {
        return plugin_type::parser;
    }
}

To make it a bit easier constructing the aaltitoad::ntta_t object, we provide some builder classes: aaltitoad::tta_builder and aaltitoad::ntta_builder