-
Notifications
You must be signed in to change notification settings - Fork 1
133 lines (126 loc) · 4.37 KB
/
tla.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
name: TLA
on:
push:
branches: [ "main" ]
pull_request:
branches: [ "main" ]
workflow_dispatch:
jobs:
apalache-check:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: actions/setup-java@v4
with:
distribution: 'microsoft'
java-version: '17'
- name: Setup
run: |
wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
tar zxvf apalache.tgz
- name: Type- and (ordinary) invariant checking with Apalache
run: |
## -length=4 to finish in reasonable time.
./apalache/bin/apalache-mc check --config=APApbft.cfg --length=4 APApbft.tla
- name: Upload Apalache's counterexample (if any)
uses: actions/upload-artifact@v4
if: always()
with:
name: apalache-check
path: |
_apalache-out/
## Too expensive as of now.
# apalache-check-inductive:
# runs-on: ubuntu-latest
# steps:
# - uses: actions/checkout@v4
# - uses: actions/setup-java@v4
# with:
# distribution: 'microsoft'
# java-version: '17'
# - name: Setup
# run: |
# wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
# tar zxvf apalache.tgz
# - name: Partial inductive invariant checking with Apalache
# if: always()
# run: |
# # Check that Init => SafetyInv
# ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=0 APAIndpbft.tla
# # Check that SafetyInv /\ Next => SafetyInv'
# ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=1 APAIndpbft.tla
# - name: Upload Apalache's counterexample (if any)
# uses: actions/upload-artifact@v4
# if: always()
# with:
# name: apalache-check-inductive
# path: |
# _apalache-out/
apalache-simulate:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: actions/setup-java@v4
with:
distribution: 'microsoft'
java-version: '17'
- name: Setup
run: |
wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
tar zxvf apalache.tgz
- name: Simulation with Apalache
run: |
./apalache/bin/apalache-mc simulate --config=APApbft.cfg --max-run=20 --length=25 APApbft.tla
- name: Upload Apalache's counterexample (if any)
uses: actions/upload-artifact@v4
if: always()
with:
name: apalache-simulate
path: |
_apalache-out/
apalache-simulate-geninit:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: actions/setup-java@v4
with:
distribution: 'microsoft'
java-version: '17'
- name: Setup
run: |
wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
tar zxvf apalache.tgz
- name: Simulation GenInit predicate with Apalache
run: |
./apalache/bin/apalache-mc simulate --config=APApbft.cfg --init=GenInit --max-run=1 --length=1 APAIndpbft.tla
- name: Upload Apalache's counterexample (if any)
uses: actions/upload-artifact@v4
if: always()
with:
name: apalache-simulate-geninit
path: |
_apalache-out/
tlc-generate:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install TLA+ Tools
run: |
git clone https://github.com/pmer/tla-bin.git
cd tla-bin
./download_or_update_tla.sh --nightly
sudo ./install.sh
- name: Random generation with TLC
run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -generate MCpbft.tla
tlc-simulate:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install TLA+ Tools
run: |
git clone https://github.com/pmer/tla-bin.git
cd tla-bin
./download_or_update_tla.sh --nightly
sudo ./install.sh
- name: Random simulation with TLC
run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -simulate MCpbft.tla