새 소식
2023-08-02
경계 없는 모델 다루기와 모델 체킹 최적화 주제를 추가했다.
2023-01-13
메시지 큐 모델링 주제를 추가했다.
2022-11-11
Github에 올라온 여러 이슈를 고쳤고, 새 연산자(operator) 예제를 추가했다.
2022-07-25
연습 문제 디렉티브(directive)를 추가했으니, 이제 핵심 과정에 연습 문제를 넣기 시작할 수 있다.
2022-07-08
표준 모듈 레퍼런스를 추가했다.
2022-06-30
베타를 공개했다!
로드맵
핵심 과정:
연습 문제
사람들이 이해하기 어려워하는 부분은 뭐든 고치기
다이어그램 몇 개 더
주제별 심화:
정제(refinement)
ADT 모델링
커뮤니티 모듈(community modules)
레거시 시스템 모델링
기계와 세계의 차이
스펙(spec)과 코드베이스를 어긋나지 않게 유지하기
하이퍼속성(hyperproperties)
::문법
예제:
많이
레퍼런스:
문제 해결 페이지
LaTeX-ASCII 대응표
TLA+와 PlusCal 치트시트
기타:
오프라인용 PDF 출력
C 문법 PlusCal용 패널
팝업 각주