aaltitoad
v1.2.0
AAL Borg Ti ck a CK A Utomata Vali d ator: un motor de verificación extensible y simulador para Automata Tick Tock.
Los TTA (Tick Tock Automata) son una teoría basada en autómatas que puede modelar la lógica comercial paralela para todo tipo de sistemas de automatización. Un TTA consiste en un conjunto de ubicaciones y transiciones entre ellos. Cada transición puede ser protegida por una expresión booleana y tiene un conjunto de asignaciones variables como "consecuencia" de tomar la transición.
Una buena analogía con TTA es una estadística , donde un sistema puede hacer la transición de un estado a otro. A continuación se muestra un ejemplo de un TTA simple que controla una luz basada en una entrada de botón.
Comenzando en la ubicación fuera de la ubicación, solo hay un borde saliente con el protector que verifica si btn_is_pressed es verdadero . Si es así, nos movemos a la ubicación y establecemos la light variable en verdad como consecuencia de tomar el borde/transición. Luego, cuando se libera el botón, volvemos al Locaiton OFF y light se establece en falso nuevamente.
Lo que hace que los TTA sean diferentes de cualquier otro sistema de transición es que la variable btn_is_pressed es una variable externa , lo que significa que el sistema de transición no puede asignar a ningún valor, solo puede cambiar en función de una entrada externa. Las entradas externas se leen cuando no estamos tomando transiciones. Esta división de la semántica es de donde proviene el nombre Tick Tock Automata:
Llevando la sintaxis un paso más allá, puede tener muchos de estos TTA funcionando en paralelo, compartiendo el mismo conjunto de variables internas y externas. Dicha red se llama simplemente un trabajo de Tick t Ock A Utomata (NTTA).
Aaltitoad se construye con CMake. Debe tener un compilador compatible C ++ 20, flex , bison versión 3.5+ y la biblioteca de plantillas estándar instalada. Todas las demás dependencias se manejan a través del maravilloso Administrador de paquetes CPM.
mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make Si el paso CPM está tomando mucho tiempo, intente volver a sin embargo con -DCPM_SOURCE_CACHE=~/.cache/CPM
Para ejecutar las pruebas unitarias, compile el objetivo 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 Si desea incluir estadísticas de cobertura de código, proporcione el indicador -DCODE_COVERAGE=ON cmake.
AALTITOAD proporciona tres objetivos de compilación primarios. Todas las interfaces de línea de comandos tienen una página de ayuda que puede convocar con el argumento --help .
verifier : una interfaz de línea de comando de verificación del motorsimulator : una interfaz de línea de comandos de tiempo de ejecuciónaaltitoad : una biblioteca con todas las cosas aaltitoad Aaltitoad admite bibliotecas de terceros "Tocker", por lo que puede inyectar integraciones personalizadas directamente en el tiempo de ejecución. Este repositorio proporciona un ejemplo de Tocker llamado pipe_tocker en el directorio tocker_plugins para servir como un proyecto de ejemplo. Un "Tocker" debe definir los siguientes 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;
}
} El TOCKER_NAME se refiere a la C-String proporcionada por la función get_plugin_name . Los nombres de las funciones deben coincidir, de lo contrario el complemento no se cargará. Los complementos de Tocker deben vincularse con la biblioteca compartida aaltitoad , y deben compilarse como una biblioteca compartida, así:
add_library (TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries (TOCKER_NAME_tocker aaltitoad) Una vez compilado, puede instanciar el Tocker proporcionando el --tocker / -t junto con --tocker-dir / -T a la línea de comandos AALTITOAD. La opción --tocker debe proporcionarse así:
--tocker-dir /path/to/tocker-plugins --tocker " TOCKER_NAME(argument string) " La "argument string" de la opción se refiere a la cadena de argumento de entrada proporcionada a la función create_TOCKER_NAME . Ahora sus tocadores deberían haber sido instanciados, y su función tock se llamará cada vez que el TTA esté listo para calcular los valores de Tocker.
Hay dos tipos de interfaces de Tocker que un tercero puede extender:
tocker_t )async_tocker_t ) El Bloqueo de Tocker se ejecutará en un solo hilo y bloqueará toda la ejecución de tick hasta que se haya completado el TOCK, y una integración de terceros solo debería anular la función tock . En contraste, el Tocker asíncrono no bloqueará la ejecución de la garrapata, sino que iniciará una nueva tarea asíncrona de la función get_tock_values .
Al implementar su Tocker, debe considerar si desea bloquear el TTA para ejecutar o no. Si elige implementar un Tocker asincrónico, tenga en cuenta que el entorno de entrada puede haber cambiado desde que se emitió el TOCK.
Si no desea usar el analizador incluido, siempre puede suministrar el suyo. Mientras proporcione los siguientes símbolos (recuerde 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 que sea un poco más fácil construyendo el objeto aaltitoad::ntta_t , proporcionamos algunas clases de constructor: aaltitoad::tta_builder y aaltitoad::ntta_builder
