pbes2bool - 클라우드에서 온라인

프로그램:

이름

pbes2bool - PBES에서 BES를 생성하고 문제를 풉니다.

개요

pbes2bool [OPTION]...[인파일]

기술

INFILE에서 (P)BES를 해결합니다. INFILE이 없으면 stdin이 사용됩니다.

옵션

OPTION 다음 중 하나일 수 있습니다.

-c, --카운터
왼쪽의 인스턴스화로 레이블이 지정된 트리를 끝에 인쇄합니다.
방정식; 이 트리는 pbes2bool이 유효성에 도달한 방식을 나타냅니다.
PBES의 무효성

-eLEVEL, --삭제=LEVEL
bes 변수를 제거하려면 제거 레벨 LEVEL을 사용하십시오. 'none' 생성된 bes를 제거하지 마십시오.
변수. 이로 인해 과도한 메모리 사용이 발생할 수 있습니다. (기본값) '일부' 제거
생성된 bes 변수는 사용되지 않습니다. 단, 오른쪽에 있는 경우는 제외됩니다.
방정식은 참이거나 거짓입니다. 다음과 같은 경우 변수의 rhss를 다시 계산해야 합니다.
다시 만났는데 이는 매우 정상적인 현상입니다. 'all'은 모든 bes 변수를 제거합니다.
더 이상 어떤 방정식에도 사용되지 않습니다. 이는 상당히 메모리 효율적이지만
제거된 bes 변수의 rhss를 수정해야 하므로 시간이 많이 소요됩니다.
꽤 자주 다시 계산됩니다.

-H, --해시테이블
bes 방정식을 대체할 때 해시테이블을 사용하고 내부를 번역합니다.
이진 결정 다이어그램에 대한 표현(성능으로 인해 권장되지 않음)

-iFORMAT, --에=FORMAT
입력 형식 FORMAT 사용: 내부 형식 'pbes_text' PBES의 'pbes' PBES
내부 텍스트 형식 '텍스트' 텍스트 형식의 PBES(mCRL2) 형식 'bes' 내부의 BES
내부 텍스트 형식 'cwi'의 BES 형식 'bes_text' CWI 형식 'pgsolver'의 BES
PGSolver 형식의 BES

-oFORMAT, --산출=FORMAT
출력 형식 FORMAT을 사용합니다(이 옵션은 더 이상 사용되지 않습니다. pbes2bes 도구를 사용하세요.
대신).

-QNUM, --qlimit=NUM
수량자의 열거를 NUM개의 변수로 제한합니다. (기본값 NUM=1000, NUM=0
제한 없는).

-r이름, --재작성자=이름
재작성 전략 사용 NAME: 'jitty' jitty 재작성(기본값) 'jittyc' 컴파일됨
jitty rewriting 'jittyp' jitty rewrite with Prover

-z검색 선택, --검색=검색 선택
검색 전략 사용 SEARCH: 'breadth-first'
부울 변수는 선착순으로 제공됩니다. 이는 다음과 비교할 수 있습니다.
너비 우선 검색. 이는 카운터 예제를 생성하는 데 좋습니다. (기본)
'깊이 우선' 부울 변수의 우변을 계산합니다.
생성된 변수를 먼저 조사합니다. 이는 깊이 우선에 해당합니다.
찾다. 이는 유효성이 검증된 경우 너비 우선 검색보다 훨씬 뛰어난 성능을 발휘할 수 있습니다.
공식은 더 큰 깊이 후에 결정됩니다. 'b' 너비 우선의 약어입니다.
'd' 깊이 우선의 약칭입니다.

-s전략, --전략=전략
대체 전략 사용 STRAT: '0' 가능한 모든 부울 방정식을 계산합니다.
최적화 없이 초기 상태에서 도달했습니다. 이게 가장 많은 데이터야
생성된 방정식당 효율적인 옵션입니다. (기본값) '1' 즉시 최적화
이미 조사된 참인 변수를 우변으로 대체
또는 표현식을 생성할 때 false입니다. 이는 0만큼 메모리 효율적입니다. '2'
1 외에도 true 또는 false인 변수를 이미 있는 변수로 대체합니다.
생성된 오른쪽. 이는 특정 변수에 접근할 수 없게 됨을 의미할 수 있습니다.
(예: X0 및 X0의 X1, X1이 거짓이 되면 X0이 다른 곳에서는 발생하지 않는다고 가정합니다.
어떤 변수가 도달할 수 없게 되었는지는 유지됩니다.
조사할 것. PBES에 따라 크기가 줄어들 수 있습니다.
BES를 상당히 생성했지만 더 큰 메모리 공간이 필요합니다. '3' 인
2 외에도 생성된 변수가 루프에서 발생하는지 조사하고,
고정 소수점 기호에 따라 참 또는 거짓으로 설정될 수 있습니다.
이로 인해 방정식을 생성하는 데 필요한 시간이 상당히 늘어날 수 있습니다.

--타이밍[=FILE]
FILE에 타이밍 측정을 추가합니다. 측정값은 다음과 같은 경우 표준 오차로 기록됩니다.
파일이 제공되지 않음

-u, --미사용_데이터
데이터 사양에서 사용하지 않는 부분을 제거하지 마십시오.

표준 옵션:

-q, --조용한
경고 메시지를 표시하지 않음

-v, --말 수가 많은
짧은 중간 메시지 표시

-d, -디버그
자세한 중간 메시지 표시

--로그 수준=LEVEL
레벨을 포함한 중간 메시지 표시

-h, --도움
도움말 정보 표시

--번역
버전 정보 표시

onworks.net 서비스를 사용하여 pbes2bool을 온라인으로 사용하세요