페트리넷 흐름 실험
가중 연결선을 가진 유한 용량 장소·전이망을 실험합니다. 토큰 배치가 전이를 활성·차단하며 너비 우선 탐색으로 도달 가능한 배치와 활성 전이가 없는 상태를 찾습니다. 상태 상한에 걸린 결과는 완전한 증명으로 표시하지 않습니다.
주요 기능
- 장소·전이·이분 가중 연결선·초기 토큰·장소별 용량 검증
- 활성 전이 한 개 또는 공동 활성 두 개 발화, 실행 취소와 초기화
- 외부 그래프 서비스 없이 현재 토큰과 연결선 가중치를 SVG로 그림
- 명시적 상태·연결선 상한으로 순차 발화 도달성 탐색
- 활성 전이가 없는 배치의 최단 발화 경로와 탐색 미완료 구분
- 전이별 정확한 토큰 증감과 전체 토큰 보존 여부 검사
- 정규화 프로젝트 JSON·도달성 보고서·상태 CSV·현재 SVG 저장
사용 방법
- 두 가지 예시·로컬 JSON 파일을 열거나 버전 1 프로젝트를 편집기에 입력합니다.
- 프로젝트를 적용하고 활성 전이를 눌러 실시간 토큰 배치를 바꿉니다.
- 공동 활성 쌍을 골라 입력 토큰 합계와 출력 용량을 확인한 뒤 동시에 발화합니다.
- 상태 상한을 정하고 초기 배치에서 너비 우선 도달성 분석을 실행합니다.
- 전이 없는 상태·최단 경로·보존량과 탐색 완전 여부를 살펴봅니다.
- 프로젝트·보고서·상태 CSV·현재 SVG 그림을 저장합니다.
활용 예시
- 두 작업이 같은 가지를 골라 자원이 막히는 경우 찾기
- 동기화 합류가 실제로 가능한지 확인하기
- 동시 발화와 전이별 발화 비교하기
- 토큰 보존 및 용량이 상태 폭발을 제한하는 방식 학습하기
자주 묻는 질문
전이는 언제 활성화되나요?
입력 연결선이 요구하는 토큰이 충분하고, 모두 소비한 다음 출력 토큰을 만든 최종 배치가 각 장소 용량을 넘지 않아야 합니다. 연결선 가중치는 양의 정수입니다. 두 전이의 동시 발화도 합계 입력과 최종 용량을 함께 검사합니다.
활성 전이가 없는 상태는 항상 오류인가요?
아닙니다. 완료된 업무 흐름도 의도적으로 더 발화할 전이가 없을 수 있습니다. 보고서는 그런 모든 도달 배치를 교착 후보로 보여 주며 의도된 완료인지 원치 않는 정지인지는 사용자가 판단해야 합니다.
도달성 보고서에 동시 발화가 포함되나요?
도달성 탐색은 연결선마다 전이 한 개를 실행하는 순차 끼워넣기 의미론입니다. 실시간 조작은 두 전이를 동시에 발화할 수 있습니다. 용량 제약에서는 동시 실행으로만 가능한 배치가 있을 수 있으므로 이 보고서를 모든 동시 실행의 증명으로 보면 안 됩니다.
탐색 상한에 닿으면 어떻게 되나요?
상태 또는 연결선 상한 도달 여부를 기록합니다. 이미 찾은 교착 후보는 유효한 증인이지만 탐색이 잘리면 교착 부재나 모든 전이 미방문을 전체 결론으로 말할 수 없습니다. 모든 장소에는 유한 용량이 선언됩니다.
토큰 보존은 어떻게 검사하나요?
전이마다 출력 연결선 가중치 합에서 입력 합을 빼 계산합니다. 모든 차이가 0이면 어떤 발화에도 전체 토큰 수가 보존됩니다. 이는 구조적 전체 토큰 검사이며 모든 장소 불변식이나 생존성을 증명하지는 않습니다.
프로젝트가 서버로 전송되나요?
아닙니다. JSON 읽기·시뮬레이션·그림·다운로드가 현재 브라우저 탭에서 동작합니다. 외부 레이아웃 서비스·계정·자동 저장을 쓰지 않습니다.
개인정보 안내
프로젝트는 자동 업로드·저장 없이 현재 브라우저 탭에서 처리합니다. 내보낸 JSON에는 사용자가 입력한 모델이 포함됩니다.
댓글과 질문