ltsconvert - 클라우드 온라인

프로그램:

이름

ltsconvert - LTS를 변환하고 선택적으로 최소화

개요

lts변환 [OPTION]... [인파일 [아웃파일]]

기술

요청된 파일에서 LTS(labeled transition system)를 INFILE에서 OUTFILE로 변환합니다.
선택한 최소화 방법을 적용한 후 형식을 지정합니다(기본값은 없음). OUTFILE이
제공되지 않으면 stdout이 사용됩니다. INFILE이 제공되지 않으면 stdin이 사용됩니다.

출력 형식은 OUTFILE의 확장자에 의해 결정되는 반면 입력 형식은
INFILE의 내용에 따라 결정됩니다. --in 및 --out 옵션을 사용하여 강제로 입력할 수 있습니다.
및 출력 형식. 지원되는 형식은 다음과 같습니다.
Aldebaran 형식(CADP)의 경우 'aut',
GraphViz 형식의 경우 '점'(더 이상 입력 형식으로 지원되지 않음),
유한 상태 기계 형식의 경우 'fsm' 또는
mCRL2 LTS 형식의 'lts'(기본값)

옵션

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

-D, --결정
LTS 결정

-e이름, --등가=이름
동등한 LTS를 생성하여 동등한 NAME: 'none' ID를 유지합니다.
등가(기본값) 'bisim' 강한 유사성 'bisim-sig' 강한 유사성
시그니처 정제 사용 'branching-bisim' branching bisimilarity 'branching-
서명 개선 'dpbranching-bisim'을 사용한 bisim-sig' 분기 유사성
발산 보존 분기 유사성 'dpbranching-bisim-sig' 발산
시그니처 정제 'weak-bisim' weak를 사용하여 분기 비스밀성 보존
bisimilarity 'weak-bisim-sig' 서명 개선을 사용하는 약한 bisimilarity 'dpweak-
약한 bisimilarity를 ​​보존하는 bisim' divergence 'dpweak-bisim-sig' divergence
서명 개선 'sim' 강한 시뮬레이션을 사용하여 약한 유사성 보존
동등성 '추적' 강한 추적 동등성 '약한 추적' 약한 추적 동등성
'타우스타' 타우스타 환원

-iFORMAT, --에=FORMAT
FORMAT을 입력 형식으로 사용

-lFILE, --lps=FILE
FILE을 입력 LTS가 생성된 LPS로 사용합니다. 이것은 필요할 수 있습니다
fsm 형식으로 저장할 때 상태의 올바른 매개변수 이름을 저장하고
비 mCRL2 LTS를 mCRL2 LTS로 변환

-- 도달 불가
입력 LTS에서 도달 가능성 검사를 수행하지 마십시오.

-n, --상태 없음
도트 형식으로 저장할 때 상태 정보 생략

-oFORMAT, --밖=FORMAT
FORMAT을 출력 형식으로 사용

--타우=행위명
쉼표로 구분된 목록 ACTNAMES에 이름이 있는 작업을 내부 작업으로 간주
(tau) 입력에 의해 정의된 작업 이외의 작업

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

표준 옵션:

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

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

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

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

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

--번역
버전 정보 표시

onworks.net 서비스를 사용하여 온라인에서 ltsconvert 사용