tla+ vscode setting

1. Install vscode-tlaplus

https://github.com/tlaplus/vscode-tlaplus/wiki/How-to-Install

• install extension

• install java

  sudo pacman -Syu
  yay jdk17-openjdk
  

2. Getting started

https://github.com/tlaplus/vscode-tlaplus/wiki/Getting-Started

• squares.tla 파일을 만든다.
• snippet이 있다.
  • module
  • pluscal
• pluscal을 사용하고, 다음의 스펙을 적는다.

---- MODULE squares ----
EXTENDS TLC, Integers

(*--algorithm squares

begin
    skip;
end algorithm; *)
====

• 이후 TLA+: Parse module 명령을 쓴다.
  • pluscal을 tla+로 바꿔준다.
  • vscode에서 ctrl + p 누르고 > 치고 검색하면 된다.
• TLA+: Check model 명령을 쓴다.
  • tlc model checker를 이용한다.
  • 아래의 그림과 같이 결과를 볼 수 있다.

• .out 파일에서 TLA+: Visualize TLC output을 치면 결과창을 다시 볼 수 있다.

• pdf로 spec을 뽑고 싶다면 pdflatex를 설치한다.

  • 이후 Export ~~ pdf 명령을 실행한다.

yay texlive-latex

3. Eval

• 아래와 같이 특정 식이나 값을 eval 할 수 있다.
  • 다만 ==== 아래에 (module 정의 아래에) 위치해야 잘 작동한다.

4. Invariant

• spec을 검증하기 위한 방법 중 하나이다.
• 어떤 프로그램이 실행됨에 따라 유지되는 성질을 말한다.
  • 예) lamport clock에서 “인과 관계라면 time stamp 값이 크다”
• define이라는 block안에 variable definition과 algorithm proper를 적는다.

아래와 같이 spec이 있다.

---- MODULE invariant ----
EXTENDS TLC, Integers, Sequences, FiniteSets

S == 1..10

(*--algorithm invariant
variable 
    seq \in S \X S \X S \X S;
    index = 1;
    seen = {};
    is_unique = TRUE;
    
define
    IsUnique(s) == Cardinality(seen) = Len(s)
    IsCorrect == pc = "Done" => is_unique = IsUnique(seq)
end define;

begin
    Iterate:
        while index <= Len(seq) do 
            if seq[index] \notin seen then 
                seen := seen \union {seq[index]};
            else 
                is_unique := FALSE;
            end if;
            index := index + 1;
        end while;
end algorithm; *)

만약 IsCorrect 라는 invariant를 이용해 spec을 검증하고 싶다면 다음과 같이 한다.

1. pluscal을 parse한다. (vscode 명령)
2. ????.cfg 파일을 연다.
3. INVARIANT IsCorrect를 적어준다.
4. tlc checker를 부른다. (vscode 명령)

일부로 invariant를 깨지게 하면, 다음과 같은 결과를 얻을 수 있다.