Skip to content

Commit 2f7a8d0

Browse files
author
Jérôme FERET
committed
continuous integration: test cases for the incremental analysis
1 parent 153221a commit 2f7a8d0

66 files changed

Lines changed: 1291 additions & 14 deletions

Some content is hidden

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

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ jobs:
3030
- 4.14.2
3131
additional-packages:
3232
- ''
33-
- labltk
33+
#- labltk
3434
steps:
3535
- name: Checkout
3636
uses: actions/checkout@v5

‎tests/incremental/test1/README‎

Lines changed: 1 addition & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1 @@
1-
Command line:
2-
./KaSaIncremental essai.ka essai2.ka --do-restart-fixpoint-iterations --print-efficiency
3-
4-
On prompt:
5-
> update file essai_diff.ka as essai.ka
6-
7-
8-
9-
10-
11-
#at the beginning everything is possible
12-
#then A is dead, and r2,r5
13-
1+
"${KAPPABIN}"KaSaIncremental -d output counters.ka < (cat command.txt) || true

‎tests/integration/incremental/egfr_paper_example/README‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
cat command.txt|"${KAPPABIN}"KaSaIncremental --verbosity-level-for-reachability-analysis Medium --current-chapter a_before.ka

‎tests/integration/incremental/egfr_paper_example/a_after.ka‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
%init: 10 EGF()
2+
%init: 10 EGFR()
3+
4+
5+
EGF(r[.]),EGFR(l[.]) -> EGF(r[1]),EGFR(l[1]) @ 1
6+
EGFR(l[_],r[.]),EGFR(l[_],r[.]) -> EGFR(l[_],r[1]),EGFR(l[_],r[1]) @ 1
7+
EGFR(r[1],c[.]),EGFR(r[1],n[.]) -> EGFR(r[1],c[2]),EGFR(r[1],n[2]) @1
8+
9+
EGFR(r[1]),EGFR(r[1],c[2]),EGFR(n[2]) -> EGFR(r[1]),EGFR(r[1],c[2]),EGFR(n[2]) @1
10+
11+
EGFR(r[1],c[.],n[.]),EGFR(r[1],c[.],n[.]) -> EGFR(r[.],c[.],n[.]),EGFR(r[.],c[.],n[.]) @ 1

‎tests/integration/incremental/egfr_paper_example/a_before.ka‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
%init: 10 EGF()
2+
%init: 10 EGFR()
3+
4+
EGF(r[.]),EGFR(l[.]) -> EGF(r[1]),EGFR(l[1]) @ 1
5+
EGFR(l[_],r[.]),EGFR(l[_],r[.]) -> EGFR(l[_],r[1]),EGFR(l[_],r[1]) @ 1
6+
EGFR(r[1],c[.]),EGFR(r[1],n[.]) -> EGFR(r[1],c[2]),EGFR(r[1],n[2]) @1
7+
8+
EGFR(r[1]),EGFR(r[1],c[2]),EGFR(n[2]) -> EGFR(r[1]),EGFR(r[1],c[2]),EGFR(n[2]) @1

‎tests/integration/incremental/egfr_paper_example/command.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
update file a_after.ka as a_before.ka
2+
quit

‎tests/integration/incremental/egfr_paper_example/output/LOG.ref‎

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
Parsing a_before.ka...
2+
done
3+
Compiling...
4+
Reachability analysis...
5+
6+
Applying rule #[@rule-2]EGF(r[.]), EGFR(l[.]) -> EGF(r[1]), EGFR(l[1]) (File "a_before.ka", line 4, characters 0-48:):
7+
the precondition is satisfied
8+
9+
rule #[@rule-2]EGF(r[.]), EGFR(l[.]) -> EGF(r[1]), EGFR(l[1]) (File "a_before.ka", line 4, characters 0-48:) is applied for the first time
10+
11+
Applying rule #[@rule-3]EGFR(l[_] r[.]), EGFR(l[_] r[.]) -> EGFR(l[_] r[1]), EGFR(l[_] r[1]) (File "a_before.ka", line 5, characters 0-70:):
12+
the precondition is satisfied
13+
14+
rule #[@rule-3]EGFR(l[_] r[.]), EGFR(l[_] r[.]) -> EGFR(l[_] r[1]), EGFR(l[_] r[1]) (File "a_before.ka", line 5, characters 0-70:) is applied for the first time
15+
16+
Applying rule #[@rule-4]EGFR(r[1] c[.]), EGFR(r[1] n[.]) -> EGFR(r[1] c[2]), EGFR(r[1] n[2]) (File "a_before.ka", line 6, characters 0-69:):
17+
the precondition is satisfied
18+
19+
rule #[@rule-4]EGFR(r[1] c[.]), EGFR(r[1] n[.]) -> EGFR(r[1] c[2]), EGFR(r[1] n[2]) (File "a_before.ka", line 6, characters 0-69:) is applied for the first time
20+
21+
Applying rule #[@rule-5]EGFR(r[1]), EGFR(r[1] c[2]), EGFR(n[2]) -> EGFR(r[1]), EGFR(r[1] c[2]), EGFR(n[2]) (File "a_before.ka", line 8, characters 0-81:):
22+
the precondition is not satisfied yet
23+
24+
Applying rule #[@rule-2]EGF(r[.]), EGFR(l[.]) -> EGF(r[1]), EGFR(l[1]) (File "a_before.ka", line 4, characters 0-48:):
25+
the precondition is satisfied
26+
27+
Applying rule #[@rule-3]EGFR(l[_] r[.]), EGFR(l[_] r[.]) -> EGFR(l[_] r[1]), EGFR(l[_] r[1]) (File "a_before.ka", line 5, characters 0-70:):
28+
the precondition is satisfied
29+
30+
Applying rule #[@rule-4]EGFR(r[1] c[.]), EGFR(r[1] n[.]) -> EGFR(r[1] c[2]), EGFR(r[1] n[2]) (File "a_before.ka", line 6, characters 0-69:):
31+
the precondition is satisfied
32+
33+
------------------------------------------------------------
34+
* There are some non applyable rules
35+
------------------------------------------------------------
36+
rule File "a_before.ka", line 8, characters 0-81: will never be applied.
37+
------------------------------------------------------------
38+
every agent may occur in the model
39+
40+
------------------------------------------------------------
41+
* Non relational properties:
42+
------------------------------------------------------------
43+
EGF() =>
44+
[
45+
EGF(r[l.EGFR])
46+
v EGF(r[.])
47+
]
48+
EGFR() =>
49+
[
50+
EGFR(l[r.EGF])
51+
v EGFR(l[.])
52+
]
53+
EGFR(c) => [ EGFR(c[.]) v EGFR(c[n.EGFR]) ]
54+
EGFR(n) => [ EGFR(n[.]) v EGFR(n[c.EGFR]) ]
55+
EGFR(r) => [ EGFR(r[.]) v EGFR(r[r.EGFR]) ]
56+
57+
------------------------------------------------------------
58+
* Relational properties:
59+
------------------------------------------------------------
60+
EGF() =>
61+
[
62+
EGF(r[l.EGFR])
63+
v EGF(r[.])
64+
]
65+
EGFR(c[n.EGFR]) => EGFR(c[n.EGFR],r[r.EGFR])
66+
EGFR(n[c.EGFR]) => EGFR(n[c.EGFR],r[r.EGFR])
67+
EGFR(r[r.EGFR]) => EGFR(l[r.EGF],r[r.EGFR])
68+
------------------------------------------------------------
69+
* Properties in connected agents
70+
------------------------------------------------------------
71+
EGFR(r[1]),EGFR(r[1]) =>
72+
[
73+
EGFR(c[n.EGFR],r[1]),EGFR(n[c.EGFR],r[1])
74+
v EGFR(c[.],r[1]),EGFR(n[.],r[1])
75+
]
76+
------------------------------------------------------------
77+
* Properties of pairs of bonds
78+
------------------------------------------------------------
79+
EGFR(c[n.EGFR],r[r.EGFR]) => EGFR(c[2],r[1]),EGFR(n[2],r[1])
80+
EGFR(n[c.EGFR],r[r.EGFR]) => EGFR(n[2],r[1]),EGFR(c[2],r[1])
81+
82+
------------------------------------------------------------
83+
* Properties of counters
84+
------------------------------------------------------------
85+
86+
execution finished without any exception
87+
Parsing a_after.ka...
88+
done
89+
90+
Applying rule #[@rule-2]EGF(r[.]), EGFR(l[.]) -> EGF(r[1]), EGFR(l[1]) (File "a_before.ka", line 5, characters 0-48:):
91+
the precondition is satisfied
92+
93+
Applying rule #[@rule-3]EGFR(l[_] r[.]), EGFR(l[_] r[.]) -> EGFR(l[_] r[1]), EGFR(l[_] r[1]) (File "a_before.ka", line 6, characters 0-70:):
94+
the precondition is satisfied
95+
96+
Applying rule #[@rule-4]EGFR(r[1] c[.]), EGFR(r[1] n[.]) -> EGFR(r[1] c[2]), EGFR(r[1] n[2]) (File "a_before.ka", line 7, characters 0-69:):
97+
the precondition is satisfied
98+
99+
Applying rule #[@rule-5]EGFR(r[1]), EGFR(r[1] c[2]), EGFR(n[2]) -> EGFR(r[1]), EGFR(r[1] c[2]), EGFR(n[2]) (File "a_before.ka", line 9, characters 0-81:):
100+
the precondition is not satisfied yet
101+
102+
Applying rule #[@rule-6]EGFR(r[1] c[.] n[.]), EGFR(r[1] c[.] n[.]) -> EGFR(r[.] c[.] n[.]), EGFR(r[.] c[.] n[.]) (File "a_before.ka", line 11, characters 0-90:):
103+
the precondition is satisfied
104+
105+
rule #[@rule-6]EGFR(r[1] c[.] n[.]), EGFR(r[1] c[.] n[.]) -> EGFR(r[.] c[.] n[.]), EGFR(r[.] c[.] n[.]) (File "a_before.ka", line 11, characters 0-90:) is applied for the first time
106+
107+
Applying rule #[@rule-2]EGF(r[.]), EGFR(l[.]) -> EGF(r[1]), EGFR(l[1]) (File "a_before.ka", line 5, characters 0-48:):
108+
the precondition is satisfied
109+
110+
Applying rule #[@rule-3]EGFR(l[_] r[.]), EGFR(l[_] r[.]) -> EGFR(l[_] r[1]), EGFR(l[_] r[1]) (File "a_before.ka", line 6, characters 0-70:):
111+
the precondition is satisfied
112+
113+
Applying rule #[@rule-4]EGFR(r[1] c[.]), EGFR(r[1] n[.]) -> EGFR(r[1] c[2]), EGFR(r[1] n[2]) (File "a_before.ka", line 7, characters 0-69:):
114+
the precondition is satisfied
115+
116+
------------------------------------------------------------
117+
* There are some non applyable rules
118+
------------------------------------------------------------
119+
rule File "a_before.ka", line 9, characters 0-81: will never be applied.
120+
------------------------------------------------------------
121+
every agent may occur in the model
122+
123+
------------------------------------------------------------
124+
* Non relational properties:
125+
------------------------------------------------------------
126+
EGF() =>
127+
[
128+
EGF(r[l.EGFR])
129+
v EGF(r[.])
130+
]
131+
EGFR() =>
132+
[
133+
EGFR(l[r.EGF])
134+
v EGFR(l[.])
135+
]
136+
EGFR(c) => [ EGFR(c[.]) v EGFR(c[n.EGFR]) ]
137+
EGFR(n) => [ EGFR(n[.]) v EGFR(n[c.EGFR]) ]
138+
EGFR(r) => [ EGFR(r[.]) v EGFR(r[r.EGFR]) ]
139+
140+
------------------------------------------------------------
141+
* Relational properties:
142+
------------------------------------------------------------
143+
EGF() =>
144+
[
145+
EGF(r[l.EGFR])
146+
v EGF(r[.])
147+
]
148+
EGFR(c[n.EGFR]) => EGFR(c[n.EGFR],r[r.EGFR])
149+
EGFR(n[c.EGFR]) => EGFR(n[c.EGFR],r[r.EGFR])
150+
EGFR(r[r.EGFR]) => EGFR(l[r.EGF],r[r.EGFR])
151+
EGFR(c,r[.]) => EGFR(c[.],r[.])
152+
EGFR(n,r[.]) => EGFR(n[.],r[.])
153+
------------------------------------------------------------
154+
* Properties in connected agents
155+
------------------------------------------------------------
156+
EGFR(r[1]),EGFR(r[1]) =>
157+
[
158+
EGFR(c[n.EGFR],r[1]),EGFR(n[c.EGFR],r[1])
159+
v EGFR(c[.],r[1]),EGFR(n[.],r[1])
160+
]
161+
------------------------------------------------------------
162+
* Properties of pairs of bonds
163+
------------------------------------------------------------
164+
EGFR(c[n.EGFR],r[r.EGFR]) => EGFR(c[2],r[1]),EGFR(n[2],r[1])
165+
EGFR(n[c.EGFR],r[r.EGFR]) => EGFR(n[2],r[1]),EGFR(c[2],r[1])
166+
167+
------------------------------------------------------------
168+
* Properties of counters
169+
------------------------------------------------------------
170+
171+
execution finished without any exception
172+
>

‎tests/integration/incremental/egfr_paper_example/output/error.log.ref‎

Whitespace-only changes.

‎tests/integration/incremental/test1/README‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
cat command.txt|"${KAPPABIN}"KaSaIncremental essai.ka essai2.ka
2+
3+
#at the beginning everything is possible
4+
#then A is dead, and r2,r5
5+

‎tests/integration/incremental/test1/command.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
update file essai_diff.ka as essai.ka
2+
q

0 commit comments

Comments
 (0)