aaltitoadダウンロードaaltitoadソースコードのダウンロード

aaltitoad

その他のソースコード

v1.2.0

ダウンロード

aal borg ti ck to ck a utomata vali d ator-ティックトックオートマトンの拡張可能な検証エンジンとシミュレーター。

ティックトックオートマトンとは何ですか？

TTA（TickKK Automata）は、あらゆる種類の自動化システムの並行ビジネスロジックをモデル化できるオートマトンベースの理論です。 TTAは、それらの間の一連の場所と移行で構成されています。各遷移は、ブールの式によって守られ、移行を取る「結果」として変数割り当てのセットを持つことができます。

TTAとの良好な類似性は、システムがある状態から別の状態に移行できるステートマシンです。以下は、ボタン入力に基づいてライトを制御する単純なTTAの例です。

オフロケーションから始めて、 btn_is_pressed真であるかどうかをチェックするガードの出力エッジは1つだけです。もしそうなら、オンの場所に移動し、エッジ/トランジションを取得した結果として変数lightを真に設定します。次に、ボタンがリリースされると、オフロカイトンに戻り、 light再び偽に設定されます。

TTAを他の遷移システムと違うのは、 btn_is_pressed変数が外部変数であることです。つまり、遷移システムでは任意の値に割り当てることができないため、外部入力に基づいてのみ変更できます。外部入力は、移行を行っていないときに読み取られます。セマンティクスのこの分割は、tickkk automataという名前の名前が次の場所です。

ティックステップ：ガードを評価し、更新を適用し、場所を変更します
TOCK-STEP：外部入力を読み取り、外部出力を書き込みます

構文をさらに一歩進めると、これらのTTAの多くが並行して実行され、内部変数と外部変数の同じプールを共有できます。このようなネットワークは、単にutomata （ntta）のtick tockのnetと呼ばれます。

さらに読む

このペーパーでは、ベースダニTOCKオートマトン理論について説明します
このペーパーでは、ツールの最新の反復について詳しく説明しています（v1.0.0+）
このペーパーでは、ツールの最初の反復について説明します（v0.10.x）
自分でTTAを作成したい場合は、H-Uppaalをご覧ください

コンパイル（Linux）

aaltitoadはcmakeを使用して構築されています。 C ++ 20互換性のあるコンパイラ、 flex 、 bisonバージョン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

コードカバーの統計を含めたい場合は、cmakeフラグ-DCODE_COVERAGE=ON提供します。

使い方

Aaltitoadは、3つの主要なコンピレーションターゲットを提供します。すべてのコマンドラインインターフェイスには、 --help引数で召喚できるヘルプページがあります。

verifier ：検証エンジンコマンドラインインターフェイス
- NTTAを分析する場合は、これを使用してください
simulator ：ランタイムコマンドラインインターフェイス
- NTTAを実行し、カスタムトーカーズにリンクする場合はこれを使用します（以下を参照）
aaltitoad ：すべてのものがあるライブラリAaltitoad
- これを使用して、別の検証者、ランタイム、またはコンパイラなど、独自のNTTAベースのアプリケーションを作成します

トッカープラグイン

Aaltitoadは、サードパーティの「Tocker」ライブラリをサポートするため、ランタイムに直接カスタム統合を挿入できます。このリポジトリには、 tocker_pluginsディレクトリのpipe_tockerと呼ばれるTockerの例を提供して、プロジェクトの例として機能します。「トッカー」は次のシンボルを定義する必要があります。

# 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 、 get_plugin_name関数によって提供されるcストリングを指します。関数名と一致する必要があります。そうしないと、プラグインがロードされません。 Tockerプラグインは、 aaltitoad共有ライブラリにリンクする必要があり、次のように共有ライブラリとしてコンパイルする必要があります。

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

コンパイルしたら、 --tocker / -tと一緒に--tocker-dir / -T aaltitoadコマンドラインに提供することにより、トッカーをインスタンス化できます。 --tockerオプションは次のように提供する必要があります。

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

オプションの"argument string" - パートは、 create_TOCKER_NAME関数に提供された入力引数文字列を指します。これで、TOCKERがインスタンス化されるはずであり、TTAがTOCKER値を計算する準備ができるたびにtock関数が呼び出されます。

トッカータイプ

トッカーが拡張できるサードパーティのトッカーインターフェイスには、次の2種類があります。

トーカーズをブロックする（デフォルトの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;
    }
}