aaltitoad 다운로드 - aaltitoad 소스 코드 다운로드

aaltitoad

기타 소스코드

v1.2.0

다운로드

aal borg ti ck to ck a utomata vali d ator- 진드기 tock automata를위한 확장 가능한 검증 엔진 및 시뮬레이터.

진드기 Tock Automata 란 무엇입니까?

TTA (Tick Tock Automata)는 모든 종류의 자동화 시스템에 대해 병렬 비즈니스 로직을 모델링 할 수있는 오토마타 기반 이론입니다. TTA는 일련의 위치와 그들 사이의 전환으로 구성됩니다. 각 전이는 부울 표현 으로 보호 될 수 있으며 전환을 취하는 "결과"로서 변수 할당 세트를 가질 수 있습니다.

TTA와 좋은 비유는 시스템이 한 상태에서 다른 상태로 전환 할 수있는 Statemachine 입니다. 아래는 버튼 입력을 기반으로 조명을 제어하는 간단한 TTA의 예입니다.

오프 위치에서 시작하여 btn_is_pressed 사실 인지 확인하는 가드와 함께 나가는 가장자리가 하나뿐입니다. 그렇다면, 우리는 위치로 이동하여 Edge/Transition을 취한 결과로 가변 light true 로 설정합니다. 그런 다음 버튼이 해제되면 Off Locaiton으로 돌아가고 light 다시 False 로 설정됩니다.

TTA를 다른 전환 시스템과 다르게 만드는 것은 btn_is_pressed 변수가 외부 변수라는 것입니다. 즉, 전환 시스템에 의해 어떤 값 으로든 할당 할 수 없으므로 외부 입력에 따라 만 변경할 수 있습니다. 외부 입력은 우리가 전환하지 않을 때 읽습니다. 이 의미의 분할은 이름 진드기 Tock Automata가 다음과 같은 곳입니다.

진드기 단계 : 가드를 평가하고, 업데이트를 적용하고, 위치를 변경하십시오
Tock-Step : 외부 입력을 읽고 외부 출력을 작성하십시오

구문을 한 걸음 더 한 걸음 더 나아가면 이러한 TTA의 많은 부분이 동일한 내부 및 외부 변수 풀을 공유 할 수 있습니다. 이러한 네트워크는 단순히 ictomata (ntta)의 ick tock 의 n etwork라고합니다.

추가 독서

이 논문은 기본 진드기 Tock Automata 이론에 대해 설명합니다
이 백서는 도구의 최신 반복을 자세히 설명합니다 (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는 세 가지 기본 컴파일 대상을 제공합니다. 모든 CommandLine 인터페이스에는 --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 Plugin은 aaltitoad 공유 라이브러리와 연결되어야하며 다음과 같이 공유 라이브러리로 편집해야합니다.

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

컴파일되면 --tocker / -t aaltitoad 명령 줄에 --tocker-dir / -T 를 제공하여 토커를 인스턴스화 할 수 있습니다. --tocker 옵션은 다음과 같이 제공해야합니다.

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

옵션의 "argument string" -파트는 create_TOCKER_NAME 함수에 제공된 입력 인수 문자열을 나타냅니다. 이제 TTA가 토커 값을 계산할 준비가 될 때마다 Tockers가 인스턴스화되어야했으며 tock 함수가 호출됩니다.

토커 유형

제 3 자 토커가 확장 할 수있는 두 가지 유형의 토커 인터페이스가 있습니다.

Tockers 차단 (기본 tocker_t )
비동기 토커 ( async_tocker_t )

차단 토커는 단일 스레드로 실행되며 Tock가 완료 될 때까지 모든 진드기 실행을 차단하고 타사 통합은 tock 함수 만 무시해야합니다. 대조적으로, 비동기 토커는 진드기 실행을 차단하지 않고 get_tock_values 함수의 새로운 비동기 작업을 시작합니다.

토커를 구현할 때는 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;
    }
}