이것은 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 pbesconstelm 명령입니다.
프로그램:
이름
pbesconstelm - PBES에서 상수 매개변수 제거
개요
pbesconstelm [OPTION]... [인파일 [아웃파일]]
기술
PBES가 포함된 파일을 읽고 상수 매개변수 제거를 적용합니다. 만약에
OUTFILE이 없으면 표준 출력이 사용됩니다. INFILE이 없으면 표준 입력
사용.
옵션
OPTION 다음 중 하나일 수 있습니다.
-c, --계산-조건
계산 전파 조건
-iFORMAT, --에=FORMAT
입력 형식 FORMAT 사용: 내부 형식 'pbes_text' PBES의 'pbes' PBES
내부 텍스트 형식 '텍스트' 텍스트 형식의 PBES(mCRL2) 형식 'bes' 내부의 BES
내부 텍스트 형식 'cwi'의 BES 형식 'bes_text' CWI 형식 'pgsolver'의 BES
PGSolver 형식의 BES
-oFORMAT, --밖=FORMAT
출력 형식 사용 FORMAT: 내부 형식 'pbes_text' PBES의 'pbes' PBES
내부 텍스트 형식 '텍스트' 텍스트(mCRL2) 형식의 PBES
-p이름, --pbes-재작성기=이름
단순화를 위해 pbes 재작성 전략 이름: 'simplify' 사용(기본값)
모든 수량사를 제거하기 위한 'quantifier-all'
PFNF 정규형으로 다시 쓰기 위해 유한 수량자 변수 'pfnf' 제거
Parameterised Parity Game 형식 'bqnf-quantifier'로 재작성하기 위한 'ppg'
정량사의 접속사에 대한 접속사에 대한 수량사 재작성(실험적)
-QNUM, --qlimit=NUM
수량자의 열거를 NUM개의 변수로 제한합니다. (기본값 NUM=1000, NUM=0
제한 없는).
-e, --제거 방정식
중복 방정식 제거
-r이름, --재작성자=이름
재작성 전략 사용 NAME: 'jitty' jitty 재작성(기본값) 'jittyc' 컴파일됨
jitty rewriting 'jittyp' jitty rewrite with Prover
--타이밍[=FILE]
FILE에 타이밍 측정을 추가합니다. 측정값은 다음과 같은 경우 표준 오차로 기록됩니다.
파일이 제공되지 않음
표준 옵션:
-q, --조용한
경고 메시지를 표시하지 않음
-v, --말 수가 많은
짧은 중간 메시지 표시
-d, -디버그
자세한 중간 메시지 표시
--로그 수준=LEVEL
레벨을 포함한 중간 메시지 표시
-h, --도움
도움말 정보 표시
--번역
버전 정보 표시
onworks.net 서비스를 사용하여 온라인에서 pbesconstelm 사용
