lps2lts - 클라우드의 온라인

프로그램:

이름

lps2lts - LPS에서 LTS 생성

개요

lps2lts [OPTION]... [인파일 [아웃파일]]

기술

INFILE의 LPS에서 LTS를 생성하고 결과를 OUTFILE에 저장합니다. INFILE이 아닌 경우
제공되면 stdin이 사용됩니다. OUTFILE이 제공되지 않으면 LTS가 저장되지 않습니다.

'jittyc' 재작성기를 사용하는 경우 MCRL2_COMPILEREWRITER 환경 변수
(기본값: 'mcrl2compilerewriter') rewriter를 컴파일하는 스크립트를 결정하고,
MCRL2_COMPILEDIR(기본값: '.')은 임시 파일이 저장되는 위치를 결정합니다.

lps2lts는 모든 쌍 간에 동일한 레이블로 여러 전환을 전달할 수 있습니다.
상태. 이것이 바람직하지 않은 경우 강력한 적용을 통해 이러한 전환을 제거할 수 있습니다.
예를 들어 도구 ltsconvert를 사용하는 이중 시뮬레이션 환원.

OUTFILE의 형식은 확장자에 의해 결정됩니다.
옵션). 지원되는 형식은 다음과 같습니다.

Aldebaran 형식(CADP)의 경우 'aut',
GraphViz 형식의 경우 '점'(더 이상 입력 형식으로 지원되지 않음),
유한 상태 기계 형식의 경우 'fsm' 또는
mCRL2 LTS 형식의 경우 'lts' jittyc 재작성기를 사용하는 경우
MCRL2_COMPILEREWRITER 환경변수 (기본값: mcrl2compilerewriter)
rewriter를 컴파일하는 스크립트와 MCRL2_COMPILEDIR(기본값:
'.') 임시 파일이 저장되는 위치를 결정합니다. lps2lts는 여러
상태 쌍 간에 동일한 레이블로 전환합니다. 이것이 원하지 않는 경우,
예를 들어 다음을 사용하여 강력한 바이시뮬레이션 환원을 적용하여 전환을 제거할 수 있습니다.
도구 ltsconvert.

옵션

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

-a이름, --동작=이름
작업 이름이 다음과 같은 전환 시스템에서 작업을 감지하고 보고합니다.
쉼표로 구분된 목록인 NAMES. 이것은 예를 들어 찾거나 증명하는 데 유용합니다.
부재) 조치 오류. 다음 중 하나가 발생할 때마다 메시지가 인쇄됩니다.
이러한 작업 이름. -t 플래그를 사용하면 이러한 작업에 대한 추적이 생성됩니다.

-b[NUM], --비트 해시[=NUM]
비트 해싱을 사용하여 상태를 저장하고 최대 NUM개의 상태를 저장합니다. 이것은 의미합니다
방문한 모든 상태의 전체 기록을 유지하는 대신 비트 배열
상태의 해시가 이전에 본 적이 있는지 여부를 나타내는 데 사용됩니다.
이는 이 옵션으로 인해 상태가 다른 것으로 오인될 수 있음을 의미합니다.
(동일한 해시에 매핑되기 때문에) 매우 큰 규모를 탐색하는 데 유용할 수 있습니다.
그렇지 않으면 탐색할 수 없는 LTS. NUM의 기본값은 대략
2*10^8 (약 25MB 메모리에 해당)

--캐시
열거형 캐싱 기술을 사용하여 상태 공간 생성 속도를 높입니다.

-c[이름], --합류[=이름]
작업 레이블이 NAME인 전환의 우선 순위를 적용합니다.(NAME이 없는 경우
제공된(즉, '-c') 우선 순위가 'ctau' 작업에 부여됩니다. 에 우선권을 주기 위해
tau 플래그를 사용하려면 -ctau를 사용하십시오. 선형 과정이 tau-confluent가 아닌 경우,
생성된 상태 공간은 반드시 다음의 상태 공간과 유사하게 분기됩니다.
lps. 사용되는 생성 알고리즘은 선형 프로세스가 필요하지 않습니다.
타우 수렴합니다.

-D, --이중 자물쇠
교착 상태 감지(즉, 모든 교착 상태에 대해 메시지가 인쇄됨)

-F, --분기
발산 감지(즉, 발산(=tau 루프)이 있는 모든 상태에 대해 메시지는
인쇄). 발산을 감지하는 알고리즘은 모든 상태에 대해 선형이므로
상태 공간 탐색은 이 옵션을 켜면 XNUMX차 상태가 되어 상태가
이 옵션이 활성화되면 우주 탐사가 느려집니다.

-yBOOL, --가짜의=BOOL
LPS의 자유 변수를 BOOL 값을 기반으로 하는 더미 값으로 바꿉니다.
'예'(기본값) 또는 '아니요'

--오류 추적
탐색 중 오류가 발생하면 추적할 수 없는 상태로 추적을 저장합니다.
탐험 한

--init-tsize=NUM
내부적으로 사용되는 해시 테이블의 초기 크기 설정(기본값은 10000)

-lNUM, --최대=NUM
최대 NUM개 주 탐색

-m이름, --멀티액션=이름
쉼표인 NAMES에서 전환 시스템의 다중 작업을 감지하고 보고합니다.
분리된 목록. 다중 작업이 정확히 일치한다는 점을 제외하고는 -a와 같이 작동합니다.
데이터 매개변수를 포함합니다.

--정보 없음
OUTFILE에 상태 정보를 추가하지 마십시오. 이 옵션이 없으면 lps2lts가 상태를 추가합니다.
벡터를 LTS로. 이 옵션을 사용하면 이 정보가 삭제되고 상태가
시퀀스 번호로만 표시됩니다. 명시적 상태 정보는 다음과 같은 경우에 유용합니다.
예를 들어 시각화 목적이지만 OUTFILE이 커질 수 있습니다.
상당히. 이 옵션은 AUT 형식으로 작성할 때 암시적입니다.

-oFORMAT, --밖=FORMAT
지정된 FORMAT에 출력을 저장

--치다
상태 공간 생성 속도를 높이려면 summand 가지치기를 사용합니다.

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

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

-s이름, --전략=이름
NAME 전략을 사용하여 상태 공간 탐색: 'b', 'breadth' 너비 우선 검색
(기본값) 'd', 'depth' 깊이 우선 탐색 'p', 'prioritized' 우선 순위 단일
첫 번째 인수에 대한 작업은 Nat 정렬 방식입니다.
이 매개변수의 가장 낮은 값이 선택됩니다. 예를 들어 조치가 있는 경우 a(3)과하면
b(4) a(3) 잔해와 b(4)는 건너뛴다. 정렬의 첫 번째 매개변수가 없는 작업
둘 이상의 작업이 있는 Nat 및 multactions는 항상 선택됩니다(옵션은
실험적) 'q', 'prioritized'는 첫 번째 인수에 대한 작업의 우선 순위를 지정합니다.
Nat을 정렬하고(--prioritized 옵션 참조) 이들 중 하나를 무작위로 선택하여
우선 순위가 지정된 무작위 시뮬레이션(옵션은 실험적임) 'r', 'random' random
시뮬레이션. 모든 다음 상태 중에서 하나가 여부에 관계없이 무작위로 선택됩니다.
이 상태는 이미 관찰되었습니다. 결과적으로 무작위 시뮬레이션만
교착 상태가 발생하면 종료됩니다.

--막다
상세 모드에서는 방문한 횟수를 나타내는 진행 메시지를 인쇄하지 않습니다.
상태 및 전환. 큰 상태 공간의 경우 진행 메시지의 수는
상당히 끔찍하다. 이 기능은 이를 억제하는 데 도움이 됩니다. 기타 장황한 메시지,
탐색된 상태의 총 수와 같은 정보는 계속 표시됩니다.

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

--todo-최대=NUM
할 일 목록에 최대 NUM개 상태를 유지합니다. 이 옵션은 너비에만 관련이 있습니다.
첫 번째 검색, 여기서 NUM은 레벨당 최대 상태 수입니다.
첫 번째 검색, 여기서 NUM은 최대 깊이입니다.

-t[NUM], --추적하다[=NUM]
NAMES의 작업으로 도달한 각 상태에 대한 최단 추적을 작성합니다.
--action 옵션은 --deadlock으로 감지된 교착 상태이거나 발산입니다.
파일에 대한 --divergence로 감지되었습니다. NUM개 이하의 추적이 기록됩니다. 만약에
NUM은 제공되지 않습니다. 추적 수는 무제한입니다. 추적할 각 추적에 대해
확장자가 .trc(trace)인 고유한 파일을 작성하면
초기 상태에서 교착 상태까지의 최단 추적. 흔적은 수 있습니다
꽤 인쇄되고 tracepp를 사용하여 다른 형식으로 변환됩니다.

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

표준 옵션:

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

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

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

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

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

--번역
버전 정보 표시

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