Skip to content

Commit 269817c

Browse files
AngeloFerrandoAngeloFerrando
committed
experiments
1 parent 8a922a8 commit 269817c

File tree

4,156 files changed

+110013
-4
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

4,156 files changed

+110013
-4
lines changed

‎tools/csp/csp1.csp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
channel p
2+
3+
state0 =
4+
p -> state0
5+
6+
state1 =
7+
p -> state1
8+
9+
WCST = state0 -- Main Process, starts the recursion in state0
10+
11+
assert state0; RUN(Events) :[deadlock free]:
12+
assert state0 :[deterministic]:
13+
assert state0 :[divergence free]:

‎tools/csp/csp1.yaml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
---
2+
alphabet: [p]
3+
common_alphabet: [p]
4+
main_process: "state0"
5+
model: "csp1.csp"
6+
trace_file: "log.txt"
7+
name: "random_csp"
8+
mode: "strict"

‎tools/csp/csp10.csp

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
channel j, s, b
2+
3+
state0 =
4+
j -> state0
5+
[]
6+
s -> state0
7+
[]
8+
b -> state0
9+
10+
state1 =
11+
s -> state1
12+
[]
13+
j -> state3
14+
[]
15+
b -> state3
16+
17+
state2 =
18+
j -> state3
19+
[]
20+
s -> state3
21+
[]
22+
b -> state3
23+
24+
state3 =
25+
j -> state3
26+
[]
27+
s -> state3
28+
[]
29+
b -> state3
30+
31+
WCST = state2 -- Main Process, starts the recursion in state2
32+
33+
assert state2; RUN(Events) :[deadlock free]:
34+
assert state2 :[deterministic]:
35+
assert state2 :[divergence free]:

‎tools/csp/csp10.yaml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
---
2+
alphabet: [j, s, b]
3+
common_alphabet: [j, s, b]
4+
main_process: "state2"
5+
model: "csp10.csp"
6+
trace_file: "log.txt"
7+
name: "random_csp"
8+
mode: "strict"

‎tools/csp/csp100.csp

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
channel w, h, j
2+
3+
state0 =
4+
w -> state0
5+
[]
6+
h -> state0
7+
[]
8+
j -> state0
9+
10+
state1 =
11+
w -> state0
12+
[]
13+
h -> state2
14+
[]
15+
j -> state2
16+
17+
state2 =
18+
w -> state2
19+
[]
20+
h -> state2
21+
[]
22+
j -> state2
23+
24+
WCST = state1 -- Main Process, starts the recursion in state1
25+
26+
assert state1; RUN(Events) :[deadlock free]:
27+
assert state1 :[deterministic]:
28+
assert state1 :[divergence free]:

‎tools/csp/csp100.yaml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
---
2+
alphabet: [w, h, j]
3+
common_alphabet: [w, h, j]
4+
main_process: "state1"
5+
model: "csp100.csp"
6+
trace_file: "log.txt"
7+
name: "random_csp"
8+
mode: "strict"

‎tools/csp/csp1000.csp

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
channel x, l, o, j
2+
3+
state0 =
4+
o -> state1
5+
[]
6+
l -> state2
7+
[]
8+
x -> state4
9+
[]
10+
j -> state7
11+
12+
state1 =
13+
o -> state1
14+
[]
15+
x -> state7
16+
[]
17+
l -> state7
18+
[]
19+
j -> state7
20+
21+
state2 =
22+
o -> state1
23+
[]
24+
l -> state2
25+
[]
26+
x -> state4
27+
[]
28+
j -> state7
29+
30+
state3 =
31+
o -> state1
32+
[]
33+
l -> state2
34+
[]
35+
x -> state4
36+
[]
37+
j -> state7
38+
39+
state4 =
40+
l -> state2
41+
[]
42+
x -> state4
43+
[]
44+
o -> state7
45+
[]
46+
j -> state7
47+
48+
state5 =
49+
l -> state2
50+
[]
51+
x -> state4
52+
[]
53+
o -> state7
54+
[]
55+
j -> state7
56+
57+
state6 =
58+
x -> state7
59+
[]
60+
l -> state7
61+
[]
62+
o -> state7
63+
[]
64+
j -> state7
65+
66+
state7 =
67+
x -> state7
68+
[]
69+
l -> state7
70+
[]
71+
o -> state7
72+
[]
73+
j -> state7
74+
75+
WCST = state0 -- Main Process, starts the recursion in state0
76+
77+
assert state0; RUN(Events) :[deadlock free]:
78+
assert state0 :[deterministic]:
79+
assert state0 :[divergence free]:

‎tools/csp/csp1000.yaml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
---
2+
alphabet: [x, l, o, j]
3+
common_alphabet: [x, l, o, j]
4+
main_process: "state0"
5+
model: "csp1000.csp"
6+
trace_file: "log.txt"
7+
name: "random_csp"
8+
mode: "strict"

‎tools/csp/csp1001.csp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
channel
2+
3+
state0 =
4+
5+
6+
WCST = state0 -- Main Process, starts the recursion in state0
7+
8+
assert state0; RUN(Events) :[deadlock free]:
9+
assert state0 :[deterministic]:
10+
assert state0 :[divergence free]:

‎tools/csp/csp1001.yaml

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
---
2+
alphabet: []
3+
common_alphabet: []
4+
main_process: "state0"
5+
model: "csp1001.csp"
6+
trace_file: "log.txt"
7+
name: "random_csp"
8+
mode: "strict"

0 commit comments

Comments
 (0)