Skip to content

Commit c95d523

Browse files
exesaLignoexesaLigno
committed
Added new solutions
1 parent 8990ba7 commit c95d523

File tree

4 files changed

+229
-0
lines changed

4 files changed

+229
-0
lines changed

‎framac_database/index.json

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,12 @@
1717
"accepted": false
1818
},
1919

20+
"gnome_lr.c": {
21+
"strategy": "",
22+
"comment": "",
23+
"accepted": true
24+
},
25+
2026
"shell_rl.c": {
2127
"strategy": "",
2228
"comment": "",

‎framac_database/solutions/gnome_lr.c

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,166 @@
1+
/*@ predicate Sorted{L}(int *arr, integer begin, integer end) =
2+
\forall integer i;
3+
begin <= i < end - 1 ==> arr[i] <= arr[i + 1];
4+
*/
5+
6+
/*@ predicate Swap{L1, L2}(int *arr, integer n, integer i, integer j) =
7+
0 <= i < n && 0 <= j < n &&
8+
\at(arr[i], L1) == \at(arr[j], L2) &&
9+
\at(arr[j], L1) == \at(arr[i], L2) &&
10+
\forall integer k; (0 <= k < n && k != i && k != j) ==> \at(arr[k], L1) == \at(arr[k], L2);
11+
*/
12+
13+
/*@ inductive Permuted{L1,L2}(int *arr, integer l, integer r) {
14+
case Permuted_refl{L}:
15+
\forall int *arr, integer l, r;
16+
Permuted{L,L}(arr, l, r);
17+
18+
case Permuted_sym{L1,L2}:
19+
\forall int *arr, integer l, r;
20+
Permuted{L1,L2}(arr, l, r)
21+
==> Permuted{L2,L1}(arr, l, r);
22+
23+
case Permuted_trans{L1,L2,L3}:
24+
\forall int *arr, integer l, r;
25+
Permuted{L1,L2}(arr, l, r) && Permuted{L2,L3}(arr, l, r)
26+
==> Permuted{L1,L3}(arr, l, r);
27+
28+
case Permuted_swap{L1,L2}:
29+
\forall int *arr, integer n, l, r, i, j;
30+
l <= i <= r &&
31+
l <= j <= r &&
32+
Swap{L1,L2}(arr, n, i, j)
33+
==> Permuted{L1,L2}(arr, l, r);
34+
}
35+
*/
36+
37+
/*@
38+
logic integer inversions_for_one_elem{L}(int* arr, integer n, integer i, integer j) =
39+
(n < 2 || i < 0 || i > n - 1 || i > j || j > n - 1) ? 0
40+
: (\at(arr[i], L) > \at(arr[j], L) ? 1 : 0) + inversions_for_one_elem{L}(arr, n, i, j + 1);
41+
*/
42+
43+
/*@ ghost
44+
/@ lemma
45+
requires \valid(arr+(0..(n-1)));
46+
requires n >= 2;
47+
requires 0 <= i <= j <= n;
48+
decreases n - j;
49+
50+
ensures inversions_for_one_elem(arr, n, i, j) >= 0; @/
51+
52+
void inversions_for_one_elem_nonneg(int *arr, int n, int i, int j) {
53+
if (j <= n - 1) {
54+
inversions_for_one_elem_nonneg(arr, n, i, j + 1);
55+
}
56+
}
57+
*/
58+
59+
/*@
60+
axiomatic Inversions{
61+
logic integer inversions{L}(int* arr, integer n, integer i) =
62+
(n < 2 || i < 0 || i > n - 1) ? 0
63+
: inversions_for_one_elem{L}(arr, n, i, i + 1) + inversions{L}(arr, n, i + 1);
64+
65+
axiom inversions_axiom{L1, L2}:
66+
\forall int *a, integer n, k;
67+
(\valid{L1}(a + (0..(n - 1))) &&
68+
\valid{L2}(a + (0..(n - 1))) &&
69+
0 <= k < n - 1 &&
70+
\at(a[k], L1) > \at(a[k + 1], L1) &&
71+
\at(a[k], L2) <= \at(a[k + 1], L2) &&
72+
Swap{L1, L2}(a, n, k, k + 1))
73+
==> inversions{L1}(a, n, 0) > inversions{L2}(a, n, 0);
74+
}
75+
*/
76+
77+
/*@ ghost
78+
/@ lemma
79+
requires \valid(arr+(0..(n-1)));
80+
requires n >= 2;
81+
requires 0 <= i <= n;
82+
decreases n - i;
83+
84+
ensures inversions(arr, n, i) >= 0; @/
85+
86+
void inversions_nonneg(int *arr, int n, int i) {
87+
if (i <= n - 1) {
88+
inversions_nonneg(arr, n, i + 1);
89+
}
90+
}
91+
*/
92+
93+
/*@ requires n >= 2;
94+
requires \valid(arr + (0..n-1));
95+
96+
ensures Permuted{Pre, Post}(arr, 0, n - 1);
97+
ensures Sorted{Post}(arr, 0, n);
98+
*/
99+
100+
void gnome_lr(int *arr, int n) {
101+
int tmp, idx = 0;
102+
//@ ghost start : ;
103+
104+
/*@
105+
loop invariant 0 <= idx <= n;
106+
loop invariant Permuted{Pre, Here}(arr, 0, n - 1);
107+
loop invariant Sorted(arr, 0, idx);
108+
loop invariant inversions(arr, n, 0) >= 0;
109+
loop invariant \valid(arr+(0..n-1));
110+
//loop invariant n == \at(n, start);
111+
112+
loop variant 2 * inversions(arr, n, 0) + n - idx;
113+
*/
114+
while (idx < n) {
115+
//@ ghost int elems_swapped = 0;
116+
if (idx == 0) {
117+
idx++;
118+
//@ assert \at(idx, LoopCurrent) < idx;
119+
//@ assert inversions{LoopCurrent}(arr, n, 0) == inversions(arr, n, 0);
120+
//@ assert inversions{LoopCurrent}(arr, n, 0) + n - \at(idx, LoopCurrent) > inversions(arr, n, 0) + n - idx;
121+
//@ assert Permuted{Pre, Here}(arr, 0, n - 1);
122+
}
123+
if (arr[idx] >= arr[idx - 1]) {
124+
idx++;
125+
//@ assert \at(idx, LoopCurrent) < idx;
126+
//@ assert inversions{LoopCurrent}(arr, n, 0) == inversions(arr, n, 0);
127+
//@ assert 2 * inversions{LoopCurrent}(arr, n, 0) + n - \at(idx, LoopCurrent) > 2 * inversions(arr, n, 0) + n - idx;
128+
//@ assert Permuted{Pre, Here}(arr, 0, n - 1);
129+
} else {
130+
//@ ghost int q = idx - 1;
131+
//@ ghost label: ;
132+
tmp = arr[idx];
133+
arr[idx] = arr[idx - 1];
134+
arr[idx - 1] = tmp;
135+
//@ ghost elems_swapped = 1;
136+
137+
//@ assert Swap{LoopCurrent, Here}(arr, n, idx - 1, idx);
138+
//@ assert Permuted{Pre, Here}(arr, 0, n - 1);
139+
//@ assert \valid(arr+(0..(n-1)));
140+
141+
//@ assert \at(arr[idx], label) < \at(arr[idx - 1], label) && arr[idx] >= arr[idx - 1] && Swap{label, Here}(arr, n, idx - 1, idx);
142+
//@ ghost q = idx - 1;
143+
//@ assert \at(arr[q + 1], label) < \at(arr[q], label) && arr[q + 1] >= arr[q] && Swap{label, Here}(arr, n, q, q + 1);
144+
145+
// assert \exists integer k; (k == idx - 1 && \at(arr[k + 1], label) < \at(arr[k], label) && arr[k + 1] >= arr[k] && Swap{label, Here}(arr, n, k, idx));
146+
// assert inversions{label}(arr, idx - 1, 0) > inversions(arr, idx - 1, 0);
147+
//@ assert inversions{label}(arr, n, 0) > inversions(arr, n, 0);
148+
149+
//@ assert 2 * inversions{LoopCurrent}(arr, n, 0) + n - \at(idx, LoopCurrent) > 2 * inversions(arr, n, 0) + n - idx;
150+
151+
//@ assert Swap{LoopCurrent, Here}(arr, n, idx - 1, idx);
152+
//@ assert Permuted{Pre, Here}(arr, 0, n - 1);
153+
154+
idx--;
155+
//@ assert 2 * inversions{LoopCurrent}(arr, n, 0) + n - \at(idx, LoopCurrent) > 2 * inversions(arr, n, 0) + n - idx;
156+
//@ assert Swap{LoopCurrent, Here}(arr, n, idx, idx + 1);
157+
//@ assert Permuted{Pre, Here}(arr, 0, n - 1);
158+
}
159+
160+
//@ assert 2 * inversions{LoopCurrent}(arr, n, 0) + n - \at(idx, LoopCurrent) > 2 * inversions(arr, n, 0) + n - idx;
161+
//@ assert elems_swapped == 1 ==> Swap{LoopCurrent, Here}(arr, n, idx, idx + 1);
162+
//@ assert Permuted{Pre, Here}(arr, 0, n - 1);
163+
}
164+
return;
165+
}
166+

‎spin_database/solutions/6.pml

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
// Решите с помощью SPIN следующую головоломку («Отец и сыновья»). Отец вместе с
2+
// двумя сыновьями и лодкой находится на берегу реки. Переправиться через реку
3+
// можно только в лодке, грузоподъемность которой составляет 200 фунтов. Все
4+
// трое умеют управлять лодкой. Отец весит 200 фунтов, а оба сына — по 100
5+
// фунтов. Как им переправиться вместе с лодкой через реку?
6+
7+
// Вариант решения:
8+
// 1. Оба сына переправляются на второй берег
9+
// 2. Один сын остается на береге, а второй возвращается.
10+
// 3. Отец переплывает на второй берег
11+
// 4. Сын возвращается на первый берег
12+
// 5. Оба сына переправляются на второй берег
13+
14+
bit boat = 0;
15+
bit father = 0;
16+
bit son_1 = 0;
17+
bit son_2 = 0;
18+
19+
#define GOAL (boat && father && son_1 && son_2)
20+
21+
active proctype main() {
22+
do
23+
:: (boat == father) -> atomic {
24+
printf("Отец переплывает\n");
25+
boat = 1 - boat;
26+
father = boat;
27+
}
28+
29+
:: (boat == son_1) -> atomic {
30+
printf("Сын 1 переплывает\n");
31+
boat = 1 - boat;
32+
son_1 = boat;
33+
}
34+
35+
:: (boat == son_2) -> atomic {
36+
printf("Сын 2 переплывает\n");
37+
boat = 1 - boat;
38+
son_2 = boat;
39+
}
40+
41+
:: (boat == son_1 && boat == son_2) -> atomic {
42+
printf("Оба сына переплывают\n");
43+
boat = 1 - boat;
44+
son_1 = boat;
45+
son_2 = boat;
46+
}
47+
48+
od
49+
}
50+
51+
ltl { !(<>GOAL) }

‎spin_database/solutions/index.json

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,5 +53,11 @@
5353
"startup_cmd": "spin -run -i 10_1.pml",
5454
"comment": "",
5555
"accepted": true
56+
},
57+
"6.pml": {
58+
"task_id": "father_and_sons_2024",
59+
"startup_cmd": "spin -run -i 6.pml",
60+
"comment": "",
61+
"accepted": true
5662
}
5763
}

0 commit comments

Comments
 (0)