Aal Borg Ti CK для CK Automata vali d Ator - расширяемый двигатель проверки и симулятор для Tick Tock Automata.
TTA (Tick Tock Automata) - это теория на основе автоматов, которая может моделировать параллельную бизнес -логику для всех видов систем автоматизации. TTA состоит из набора мест и переходов между ними. Каждый переход может быть охраняется логическим выражением и имеет набор назначений переменных в качестве «следствия» для принятия перехода.
Хорошей аналогией с TTA является Стейммахин , где система может переходить от одного состояния в другое. Ниже приведен пример простой TTA, который управляет светом на основе ввода кнопки.
Начиная с места, есть только один исходящий край с охранником, который проверяет, является ли btn_is_pressed true . Если это так, мы переходим к месту и устанавливаем переменный light на True в результате принятия края/перехода. Затем, когда кнопка выпускается, мы возвращаемся в локатон Off, а light снова установлен на False .
То, что отличает TTA, от любой другой системы перехода, так это то, что переменная btn_is_pressed является внешней переменной, что означает, что ее нельзя назначить какому -либо значению системой перехода, она может изменяться только на основе внешнего ввода. Внешние входы читаются, когда мы не переходим переходы. Это разделение семантики - это то, откуда происходит название Tick Tock Automata:
Принимая синтаксис на один шаг вперед, вы можете провести много из этих TTA, работающих параллельно, разделяя один и тот же пул внутренних и внешних переменных. Такая сеть называется просто etwork of t ock atomata (ntta).
Aaltitoad создан с использованием Cmake. У вас должен быть совместимый компилятор C ++ 20, flex , bison Version 3.5+ и установленная стандартная библиотека шаблонов. Все остальные зависимости обрабатываются через замечательный менеджер пакетов CPM.
mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make Если шаг CPM занимает много времени, попробуйте повторить с -DCPM_SOURCE_CACHE=~/.cache/CPM
Чтобы запустить модульные тесты, составьте цель aaltitoad_tests
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 Если вы хотите включить статистику кодового покрытия, предоставьте флаг -DCODE_COVERAGE=ON Cmake.
Aaltitoad обеспечивает три основных целевых компиляции. Все интерфейсы командной линии имеют страницу справки, которую вы можете вызвать с аргументом --help .
verifier : интерфейс командной строки Engine Verificationsimulator : интерфейс командной строки выполнения времениaaltitoad : библиотека со всеми вещами aaltitoad Aaltitoad поддерживает лидерные библиотеки «Tocker», поэтому вы можете вводить пользовательскую интеграцию непосредственно во время выполнения. Этот репозиторий дает пример Tocker, называемый pipe_tocker в каталоге tocker_plugins , чтобы служить примером проекта. «Токер» должен определить следующие символы:
# 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;
}
} TOCKER_NAME относится к C-String, предоставленной функцией get_plugin_name . Имена функций должны соответствовать, в противном случае плагин не будет загружаться. Плагины Tocker должны связаться с общей библиотекой aaltitoad и должны быть составлены как общая библиотека, например, так:
add_library (TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries (TOCKER_NAME_tocker aaltitoad) После составления вы можете создать экземпляр Tocker, предоставив --tocker / -t вместе с --tocker-dir / -T для командной строки Aaltitoad. Опция --tocker должна быть предоставлена так:
--tocker-dir /path/to/tocker-plugins --tocker " TOCKER_NAME(argument string) " "argument string" -part опции относится к строке аргумента ввода, предоставленной функции create_TOCKER_NAME . Теперь ваши Tockers должны были быть созданы созданы, и это функция tock будет вызывать каждый раз, когда TTA готова рассчитать значения Tocker.
Есть два типа интерфейсов Tocker, которые может расширить сторонний Tocker:
tocker_t )async_tocker_t ) Блокирующий токер будет работать в одном потоке и заблокирует все выполнения клещей до тех пор, пока не будет завершен TOCK, а сторонняя интеграция должна только переопределить функцию tock . Напротив, асинхронный токер не будет блокировать выполнение клещей, но запустите новую асинхронную задачу функции get_tock_values .
При внедрении вашего Tocker вы должны рассмотреть, хотите ли вы заблокировать TTA от выполнения или нет. Если вы решите реализовать асинхронный токер, имейте в виду, что среда ввода могла измениться с момента выпуска TOCK.
Если вы не хотите использовать прилагаемый анализатор, вы всегда можете предоставить свой собственный. Пока вы предоставляете следующие символы (помните 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;
}
} Чтобы немного проще построить объект aaltitoad::ntta_t , мы предоставляем несколько классов строителей: aaltitoad::tta_builder и aaltitoad::ntta_builder