마리아 - 클라우드의 온라인

프로그램:

이름

maria - 고급 페트리 그물을 위한 모듈식 도달 가능성 분석기

개요

마리아 [옵션] 파일...

기술

이 매뉴얼 페이지는 간략하게 설명합니다 마리아 명령. 더 완전한 문서는
GNU 정보 형식으로 사용 가능; 아래를 참조하십시오.

마리아 입력에 설명된 동시 시스템 모델을 분석하는 프로그램입니다.
Algebraic System Nets를 기반으로 하는 언어. 형식주의는 Ekart에 의해 제시되었습니다.
ICATPN'98에서 Kindler와 Hagen Völzer, 유연성 in 대수 그물.
Algebraic System Nets는 데이터 유형이나 대수를 정의하지 않는 프레임워크입니다.
작업. Maria의 데이터 유형 시스템과 작업은 높은 수준으로 설계되었습니다.
프로그래밍 및 사양 언어를 염두에 두고 있습니다. 그럼에도 불구하고 각 Maria 모델에는
유한 전개.
낮은 수준의 Petri net 도구와의 상호 운용성을 보장하기 위해 Maria는 식별자를 다음으로 변환합니다.
펼친 그물을 ​​영숫자 및 밑줄 문자열로 연결합니다. 필터
폴드이름.pl 식별자의 가독성을 향상시키기 위해 사용하거나 조정할 수 있습니다.

옵션

Maria는 일반적인 GNU 명령줄 구문을 따르며 긴 옵션은 XNUMX로 시작합니다.
대시(`-'). 아래에 옵션 요약이 포함되어 있습니다. 전체 설명은 다음을 참조하십시오.
정보 파일.

-a 제한, --배열 제한=제한
배열 인덱스 유형의 크기를 다음으로 제한 제한 가능한 값. 0의 한계
검사를 비활성화합니다.

-b 모델, --너비 우선 검색=모델
도달 가능성 그래프 생성 모델 너비 우선 검색을 사용합니다.

-C 예배 규칙서, --컴파일=예배 규칙서
C 코드 생성 예배 규칙서 표현식 평가 및 저수준
전환 인스턴스 분석 알고리즘의 루틴. 이 옵션을 사용할 때,
평가 오류는 약간 다른 방식으로 보고됩니다. 통역사
상태에서 첫 번째 오류를 일으킨 평가 및 표현식을 표시합니다. NS
컴파일된 코드는 오류 수를 표시합니다. 성능상의 이유로,
생성된 코드는 다중 집합에 항목을 추가할 때 오버플로 오류를 확인하지 않습니다.

-씨, --no-컴파일
와 반대 인 -C. 내장 인터프리터에서 모든 표현식을 평가하십시오. 이것은
기본 동작.

-D 상징, --정의=상징
전처리기 기호 정의 상징.

-d 모델, --깊이 우선 검색=모델
도달 가능성 그래프 생성 모델 깊이 우선 탐색을 사용합니다.

-E 간격, --가장자리=간격
도달 가능성 그래프를 생성할 때마다 그래프의 크기를 보고합니다.
간격 생성된 가장자리.

-e 현, --실행=현
실행하다 현.

-g 그래프 파일, --그래프=그래프 파일
이전에 생성된 도달 가능성 그래프 로드 그래프 파일.rgh.

-H h[,f[,t]], --해시=h[,f[,t]]
확률적 검증을 위한 매개변수 구성(-P). 할당 t 보편적인
해시 함수 f 요소 및 해당 해시 테이블 h 비트 각각. 둘 다 h
과 f 다음 적절한 값으로 반올림됩니다.

-?, -시간, --도움
Maria에게 명령줄 옵션 요약을 인쇄하고 종료합니다.

-I 예배 규칙서, --포함=예배 규칙서
추가 예배 규칙서 포함 파일을 검색한 디렉토리 목록으로 이동합니다.

-i 열, --너비=열
출력의 오른쪽 여백을 다음으로 설정합니다. 열. 기본값은 80입니다.

-j 프로세스, --작업=프로세스
안전 특성 확인 시(옵션 -L, -M 과 -P), 이 많은 작업자를 사용하십시오.
다중 프로세서 컴퓨터에서 분석 속도를 높이는 프로세스. 또한보십시오 -k 과
-Z.

-k 포트[/주인], --연결=포트[/주인]
분산 안전 모델 검사(옵션 -L, -M 과 -P) TCP/IP 네트워크에서. 을위한
서버만 포트 일반적으로 16비트 부호 없는 정수로 지정됩니다.
1024 및 65535. 작업자 프로세스의 경우 포트/주인 포트를 지정하고
서버의 주소. 또한보십시오 -j.

-L 모델, --무손실=모델
하중 모델 도달 가능한 상태 세트를 구성하여 분석 준비
디스크 파일에서. 또한보십시오 -M, -P, -j 과 -k.

-m 모델, --모델=모델
하중 모델 도달 가능성 그래프를 지웁니다.

-M 모델, --md5-compact=모델
하중 모델 의 과대 근사를 구성하여 분석을 준비합니다.
주 메모리에서 도달 가능한 상태 집합. 또한보십시오 -P, -L, -j 과 -k.

-N 크레익스프, --이름=크레익스프
컨텍스트에서 허용되는 이름 지정 c 확장 정규 표현식으로 정규 표현식.
컨텍스트는 매개변수 문자열의 첫 번째 문자로 식별됩니다. NS
다음 문자는 허용된 이름이 반드시 있어야 하는 정규식을 구성합니다.
일치합니다.

-n 크레익스프, --이름 없음=크레익스프
컨텍스트에서 허용되지 않는 이름 지정 c 확장 정규 표현식으로
정규 표현식.
둘 다 -N 및 -n 컨텍스트에 대해 지정됨 c, 허용 일치가 걸립니다
상위. 예를 들어 모든 사용자 정의 유형 이름이
종료 _t, 지정하다 -nt -Nt'_t$'. 후자 매개변수의 따옴표는
에서 특별한 의미를 제거하는 데 필요합니다. $ 명령 줄 셸에서 당신은
아마도 마리아를 호출하는 데 사용합니다.

-P 모델, --확률적=모델
하중 모델 도달 가능한 상태 세트를 구성하여 분석 준비
라는 기술을 사용하여 주 메모리에 비트 상태 해싱.

-p 명령, --속성 번역기=명령
속성 자동 번역에 사용할 명령을 지정합니다. 명령은
표준 입력에서 공식을 읽고 해당하는 자동 장치를 작성하십시오.
표준 출력에 대한 설명입니다. 번역가 파운드 이것과 호환됩니다
옵션을 선택합니다.

-q 제한, --정량-한계=제한
이상을 갖는 유형의 수량화(다중 집합 합계) 방지 제한 가능한
가치. 제한이 0이면 검사가 비활성화됩니다.

-U 상징, --정의하지 않음=상징
전처리기 기호 정의 해제 상징.

-u [a][f[아웃파일]], --펼치기=[a][f[아웃파일]]
알고리즘을 사용하여 그물을 펼치십시오. a 그리고 그것을 형식으로 작성하십시오. f 에 아웃파일. 면 아웃파일
지정되지 않은 경우 펼쳐진 네트를 표준 출력으로 덤프합니다. 가능한 형식
are m (Maria(사람이 읽을 수 있음), 기본값), l (롤라), p (PEP) 및 r (찌르다). 거기
두 가지 알고리즘: 기존(기본값) 및 구성을 통해 축소 커버 가능한
마킹 (M).

-V, --번역
Maria의 버전 번호를 인쇄하고 종료합니다.

-V, --말 수가 많은
분석의 여러 단계에 대한 자세한 정보를 표시합니다.

- 여, --경고
의심스러운 네트워크 구성에 대한 경고를 활성화합니다. 이것이 기본 동작입니다.

-w, --경고 없음
와 반대 인 -W. 모든 경고를 비활성화합니다.

-x 숫자 베이스, --기수=숫자 베이스
진단 출력의 숫자 기준을 지정합니다. 허용되는 값 숫자 베이스 are
10월, XNUMX 진수, 8, 마녀, XNUMX 진수, 16, 12월, 소수 과 10. 기본값은 다음을 사용하는 것입니다.
십진수.

-와이, --압축 숨김
의 후속 상태를 저장하지 않음으로써 도달 가능한 상태 집합을 줄입니다.
전환 인스턴스 숨기기 상태가 유지됩니다. 숨겨진 후계자는
별도의 상태 세트에 저장됩니다. 이 옵션은 메모리를 절약할 수 있습니다(-L or -m) 또는 감소
상태가 생략될 확률(-M or -P), 개선될 수 있습니다.
병렬 분석의 효율성(-j or -k), 그러나 또한 상당히 증가할 수도 있습니다.
프로세서 시간 요구 사항. 이 옵션은 활성 모델에서도 작동합니다.
확인하지만, 활성 속성의 진실 값이 보장되지는 않습니다.
변경되지 않은 상태로 유지. 이 옵션은 다음과 결합할 수 있습니다. -Z.

-와이, --압축 없음-숨김
와 반대 인 -Y. 이것이 기본 동작입니다.

-지, --압축 경로
에 있는 중간 상태를 저장하지 않음으로써 도달 가능한 상태 집합을 줄입니다.
대부분의 후계자. 이 옵션은 메모리를 절약할 수 있습니다(-L or -m) 또는 감소
상태가 생략될 확률(-M or -P), 효율성을 향상시킬 수 있습니다.
병렬 분석(-j or -k), 그러나 그것은 또한 상당히 증가할 수 있습니다
프로세서 시간 요구 사항. 이 옵션은 활성 모델 검사와도 함께 작동합니다.
그러나 활성 속성의 진리값이 그대로 유지된다는 보장은 없습니다.
변하지 않은. 이 옵션은 다음과 결합할 수 있습니다. -Y.

-지, --압축 경로 없음
와 반대 인 -Z. 이것이 기본 동작입니다.

onworks.net 서비스를 사용하여 온라인으로 마리아 사용