aaltitoad
v1.2.0
Aal borg ti ck to ck a utomata vali d ator - un moteur de vérification extensible et un simulateur pour les automates Tick Tock.
Les TTA (Tick TOCK Automates) sont une théorie basée sur l'automate qui peut modéliser la logique métier parallèle pour toutes sortes de systèmes d'automatisation. Un TTA se compose d'un ensemble d'emplacements et de transitions entre eux. Chaque transition peut être gardée par une expression booléenne et a un ensemble de missions variables comme une «conséquence» de la prise de la transition.
Une bonne analogie avec la TTA est une statemachine , où un système peut passer d'un état à l'autre. Vous trouverez ci-dessous un exemple de TTA simple qui contrôle une lumière en fonction d'une entrée de bouton.
En commençant à l'emplacement désactivé, il n'y a qu'un seul bord sortant avec le garde qui vérifie si btn_is_pressed est vrai . Si c'est le cas, nous nous déplaçons vers l'emplacement sur et définissons la light variable sur True en conséquence de la prise du bord / de la transition. Ensuite, lorsque le bouton est libéré, nous retournons au Locaiton OFF et light est à nouveau réglée sur False .
Ce qui rend TTAS différent de tout autre système de transition, c'est que la variable btn_is_pressed est une variable externe , ce qui signifie qu'elle ne peut être attribuée à aucune valeur par le système de transition, elle ne peut que changer en fonction d'une entrée externe. Les entrées externes sont lues lorsque nous ne prenons pas de transitions. Cette scission de la sémantique est d'où le nom Tock Tock Automata vient de:
En prenant la syntaxe un peu plus loin, vous pouvez avoir beaucoup de ces TTA en parallèle, partageant le même pool de variables internes et externes. Un tel réseau est appelé simplement un travail de travail de tock a Utomata (NTTA).
AALTITOAD est construit à l'aide de CMake. Vous devez avoir un compilateur compatible C ++ 20, flex , bison version 3.5+ et la bibliothèque de modèles standard installée. Toutes les autres dépendances sont gérées par le merveilleux gestionnaire de packages CPM.
mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make Si l'étape CPM prend beaucoup de temps, essayez de relancer avec -DCPM_SOURCE_CACHE=~/.cache/CPM
Pour exécuter les tests unitaires, compilez la cible 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 vous souhaitez inclure des statistiques de couverture de code, fournissez le -DCODE_COVERAGE=ON l'indicateur CMake.
AALTITOAD fournit trois cibles de compilation primaires. Toutes les interfaces de ligne de commande ont une page d'aide que vous pouvez invoquer avec l'argument --help .
verifier : une interface de ligne de commande de moteur de vérificationsimulator : une interface de ligne de commande d'exécutionaaltitoad : une bibliothèque avec tout ce qui est Aaltitoad AALTITOAD prend en charge les bibliothèques de tiers "Tocker", vous pouvez donc injecter des intégrations personnalisées directement dans l'exécution. Ce référentiel fournit un exemple de TOCKER appelé pipe_tocker dans le répertoire tocker_plugins pour servir d'exemple de projet. Un "tocker" doit définir les symboles suivants:
# 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;
}
} Le TOCKER_NAME fait référence à la chaîne C fournie par la fonction get_plugin_name . Les noms de fonction doivent correspondre, sinon le plugin ne se chargera pas. Les plugins Tocker doivent être liés à la bibliothèque partagée aaltitoad et doivent être compilées en tant que bibliothèque partagée, comme ainsi:
add_library (TOCKER_NAME_tocker SHARED *.cpp)
target_link_libraries (TOCKER_NAME_tocker aaltitoad) Une fois compilé, vous pouvez instancier le tocker en fournissant le --tocker / -t avec --tocker-dir / -T à la ligne de commande AALTITOAD. L'option --tocker doit être fournie comme tel:
--tocker-dir /path/to/tocker-plugins --tocker " TOCKER_NAME(argument string) " La "argument string" -Part de l'option fait référence à la chaîne d'argument d'entrée fournie à la fonction create_TOCKER_NAME . Maintenant, vos tockers auraient dû être instanciés, et sa fonction tock sera appelée chaque fois que le TTA est prêt à calculer les valeurs tocker.
Il existe deux types d'interfaces TOCKER qu'un tiers TOCKER peut étendre:
tocker_t )async_tocker_t ) Le blocage Tocker s'exécutera dans un seul thread et bloquera toute l'exécution des tiques jusqu'à ce que le TOCK soit terminé, et une intégration tierce ne devrait que remplacer la fonction tock . En revanche, le tocker asynchrone ne bloquera pas l'exécution des tiques, mais commencera une nouvelle tâche asynchrone de la fonction get_tock_values .
Lors de la mise en œuvre de votre TOCKER, vous devez considérer si vous souhaitez empêcher le TTA d'exécuter ou non. Si vous choisissez d'implémenter un tocker asynchrone, sachez que l'environnement d'entrée peut avoir changé depuis l'émission du TOCK.
Si vous ne souhaitez pas utiliser l'analyseur inclus, vous pouvez toujours fournir le vôtre. Tant que vous fournissez les symboles suivants (rappelez 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;
}
} Pour faciliter la construction de l'objet aaltitoad::ntta_t , nous fournissons quelques classes de constructeur: aaltitoad::tta_builder et aaltitoad::ntta_builder
