이것은 Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 공급자에서 실행할 수 있는 명령 lpsinvelm입니다.
프로그램:
이름
lpsinvelm - 불변량을 확인하고 이를 사용하여 LPS의 명령을 단순화하거나 제거합니다.
개요
lpsinvelm [OPTION]... --invfile=INVFILE [인파일 [아웃파일]]
기술
부울 공식(Bool 정렬의 mCRL2 데이터 표현식)이 다음과 같이 제공되는지 확인합니다.
invariant는 INFILE의 LPS(선형 프로세스 사양)의 불변입니다. 이 경우
이 경우 도구는 조건이 다음을 위반하는 LPS의 모든 명령을 제거합니다.
불변하고 결과를 OUTFILE에 씁니다. INFILE이 있으면 stdin이 사용됩니다. 만약에
OUTFILE이 없고 stdout이 사용됩니다.
이 도구는 주어진 LPS의 피가수 조건을 단순화하는 데에도 사용할 수 있습니다.
옵션
OPTION 다음 중 하나일 수 있습니다.
-y, --모든 위반
불변의 단일 위반이 발견되는 즉시 종료하지 마십시오.
대신 모든 위반 사항을 보고하십시오.
-c, --반대 예
불변량이 다음과 같은 경우 위반될 수 있는 이유를 나타내는 평가를 표시합니다.
summand가 불변을 위반하는지 여부가 불확실하다.
-o, --유도
목록에 귀납법 적용
-i초대, --불변=초대
INVFILE에서 부울 공식(Bool 정렬의 mCRL2 데이터 표현식)을 다음과 같이 사용하십시오.
변하지 않는
-n, --확인하지 않음
도달할 수 없는 명령을 제거하기 전에 불변이 성립하는지 확인하지 마십시오.
-e, --제거 없음
명령을 제거하거나 단순화하지 않고 각 조건에 불변량을 추가합니다.
-p접두사, --인쇄점=접두사
여부를 결정할 수 없는 경우 결과 BDD의 .dot 파일을 저장합니다.
summand는 불변을 위반합니다. PREFIX는 출력 파일의 접두사로 사용됩니다.
-QNUM, --qlimit=NUM
수량자의 열거를 NUM개의 변수로 제한합니다. (기본값 NUM=1000, NUM=0
제한 없는).
-r이름, --재작성자=이름
재작성 전략 사용 NAME: 'jitty' jitty 재작성(기본값) 'jittyc' 컴파일됨
jitty rewriting 'jittyp' jitty rewrite with Prover
-l, --모두 단순화
단순히 summands를 제거하는 대신 모든 summands의 조건을 단순화합니다.
불변과 관련된 조건은 모순입니다.
-z솔버, --smt-해결사=솔버
SOLVER를 사용하여 내부적으로 사용되는 BDD에서 일관되지 않은 경로를 제거합니다(기본적으로
경로 제거가 적용되지 않음): 'cvc' SMT 솔버 CVC3
-t제한, --시간 제한=제한
단일 공식을 증명하는 데 최대 LIMIT초 소요
--타이밍[=FILE]
FILE에 타이밍 측정을 추가합니다. 측정값은 다음과 같은 경우 표준 오차로 기록됩니다.
파일이 제공되지 않음
표준 옵션:
-q, --조용한
경고 메시지를 표시하지 않음
-v, --말 수가 많은
짧은 중간 메시지 표시
-d, -디버그
자세한 중간 메시지 표시
--로그 수준=LEVEL
레벨을 포함한 중간 메시지 표시
-h, --도움
도움말 정보 표시
--번역
버전 정보 표시
onworks.net 서비스를 사용하여 온라인으로 lpsinvelm 사용
