aaltitoad
v1.2.0
Aal Borg Ti ck para ck um utomata Vali d Ator - um mecanismo de verificação e simulador extensível para o Tick TOCK Automata.
O TTA (Tick TOCK Automata) é uma teoria baseada em autômatos que pode modelar a lógica de negócios paralela para todos os tipos de sistemas de automação. Um TTA consiste em um conjunto de locais e transições entre eles. Cada transição pode ser guardada por uma expressão booleana e possui um conjunto de atribuições variáveis como uma "conseqüência" de fazer a transição.
Uma boa analogia com o TTA é uma Statemachine , onde um sistema pode fazer a transição de um estado para outro. Abaixo está um exemplo de um TTA simples que controla uma luz com base em uma entrada de botão.
A partir do local desligado, há apenas uma borda de saída com o guarda que verifica se btn_is_pressed é verdadeiro . Se for, passamos para o local e definimos a light variável como verdadeira como conseqüência de levar a borda/transição. Então, quando o botão é liberado, retornamos ao Locaiton e light está definida como falsa novamente.
O que torna os TTAs diferentes de qualquer outro sistema de transição é que a variável btn_is_pressed é uma variável externa , o que significa que ela não pode ser atribuída a nenhum valor pelo sistema de transição, só pode alterar com base em uma entrada externa. As entradas externas são lidas quando não estamos fazendo transições. Esta divisão da semântica é de onde vem o nome TOCK Automatos:
Levando a sintaxe um passo adiante, você pode ter muitos desses TTAs em paralelo, compartilhando o mesmo pool de variáveis internas e externas. Essa rede é chamada simplesmente de um trabalho de tck tcing a utomata (NTTA).
O Aaltitoad é construído usando CMake. Você deve ter um compilador compatível C ++ 20, flex , bison Versão 3.5+ e a biblioteca de modelos padrão instalada. Todas as outras dependências são tratadas pelo maravilhoso gerenciador de pacotes do CPM.
mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make Se a etapa do CPM estiver levando muito tempo, tente novamente com -DCPM_SOURCE_CACHE=~/.cache/CPM
Para executar os testes de unidade, compila o alvo 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 Se você deseja incluir estatísticas de cobertura de código, forneça o sinalizador -DCODE_COVERAGE=ON sinalizador CMake.
O Aaltitoad fornece três metas de compilação primária. Todas as interfaces de comando têm uma página de ajuda que você pode convocar com o argumento --help .
verifier : uma interface de linha de comando do mecanismo de verificaçãosimulator : uma interface de linha de comando de tempo de execuçãoaaltitoad : uma biblioteca com todas as coisas aaltitoad O Aaltitoad suporta bibliotecas de "Tocker" de terceiros, para que você possa injetar integrações personalizadas diretamente no tempo de execução. Este repositório fornece um exemplo de Tocker chamado pipe_tocker no diretório tocker_plugins para servir como um projeto de exemplo. Um "tocker" deve definir os seguintes símbolos:
# 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;
}
} O TOCKER_NAME refere-se à corda C fornecida pela função get_plugin_name . Os nomes de funções devem corresponder, caso contrário, o plug -in não será carregado. Os plug -ins Tocker devem se vincular à biblioteca compartilhada aaltitoad e devem ser compilados como uma biblioteca compartilhada, assim:
add_library (TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries (TOCKER_NAME_tocker aaltitoad) Uma vez compilado, você pode instanciar o tocker, fornecendo o --tocker / -t junto com --tocker-dir / -T para a linha de comando Aaltitoad. A opção --tocker deve ser fornecida assim:
--tocker-dir /path/to/tocker-plugins --tocker " TOCKER_NAME(argument string) " A "argument string" -part da opção refere -se à sequência de argumentos de entrada fornecida à função create_TOCKER_NAME . Agora, seus tockers deveriam ter sido instanciados e sua função tock será chamada cada vez que o TTA estiver pronto para calcular os valores do tocker.
Existem dois tipos de interfaces de Tocker que um tocker de terceiros pode estender:
tocker_t )async_tocker_t ) O tocker de bloqueio será executado em um único thread e bloqueará toda a execução de ticks até que o TOCK tenha concluído, e uma integração de terceiros deve substituir apenas a função tock . Por outro lado, o tocker assíncrono não bloqueará a execução do Tick, mas iniciará uma nova tarefa assíncrona da função get_tock_values .
Ao implementar seu tocker, você deve considerar se deseja impedir que o TTA seja executado ou não. Se você optar por implementar um tocker assíncrono, esteja ciente de que o ambiente de entrada pode ter mudado desde que o TOCK foi emitido.
Se você não quiser usar o analisador incluído, sempre pode fornecer o seu. Contanto que você forneça os seguintes símbolos (lembre -se 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;
}
} Para facilitar um pouco a construção do objeto aaltitoad::ntta_t , fornecemos algumas classes do construtor: aaltitoad::tta_builder e aaltitoad::ntta_builder
