fvcrusher.github.io/knowledge.html at master · fvcrusher/fvcrusher.github.io · GitHub

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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
<!DOCTYPE html>
<html lang="en">
<head>
    <link type="image/x-icon" href="favicon.ico" rel="shortcut icon">
    <link type="Image/x-icon" href="favicon.ico" rel="icon">
    <meta charset="UTF-8">
    <meta name="viewport" content="width=device-width, initial-scale=1.0">
    <title>FVCrusher · База знаний</title>
    <link rel="stylesheet" href="styles.css">
</head>
<body>
    <header>
        <div class="header-container">
            <div>
                <button class="home-button" onclick="location.href='/'">FVCrusher</button>
            </div>
            <div>
                <button class="header-button" onclick="toggleNavigation()">
                    Навигация ☰
                </button>
            </div>
            <script>
                function toggleNavigation()
                {
                    let nav_panel = document.getElementById("nav-panel");
                    if (nav_panel.style.height == "0px")
                    {
                        let is_row = window.getComputedStyle(document.getElementById("nav-panel")).flexDirection == "row";
                        nav_panel.style.height = `${nav_panel.scrollHeight * (is_row ? 2 : 1)}px`;
                        nav_panel.style.paddingTop = "10px";
                    }

                    else
                    {
                        nav_panel.style.height = "0px";
                        nav_panel.style.paddingTop = "0px";
                    }
                }
            </script>
        </div>
        <div class="nav-panel" id="nav-panel" style="height: 0px;">
            <button class="nav-button" onclick="location.href='/cnf'">КНФ</button>
            <button class="nav-button inactive" onclick="window.alert('Данный функционал еще не реализован')">Нельсон-Оппен</button>
            <button class="nav-button" onclick="location.href='/ltl2buchi'">LTL → Бюхи</button>
            <button class="nav-button" onclick="location.href='/robdd'">ROBDD</button>
            <button class="nav-button" onclick="location.href='/knowledge'">База знаний</button>
        </div>
    </header>
    <main>
        <div class="contents">
            <h2>Солверы для контрольных</h2>
            <p>
                Всего в курсе две контрольные работы, каждая состоит из 3 задач.
                Для 4 типов задач на данном сайте представлены автоматические солверы,
                позволяющие максимально быстро и подробно решить любые задачи этих
                4 типов. Пользуйтесь солверами на свой страх и риск, они были проверены
                в боевых условиях, но лучше проверяйте, что они нарешали. В любом
                случае рекомендуется перед контрольной погонять знакомые и незнакомые
                задачи в солвере для знакомства с тем, как он работает.
            </p>
            <ul>
                <li><a href="cnf">Построение КНФ по кодировке Цейтина</a></li>
                <li>Разрешающая процедура Нельсона-Оппена</li>
                <li><a href="ltl2buchi">Преобразование LTL → Автомат Бюхи</a></li>
                <li><a href="robdd">Построение ROBDD</a></li>
            </ul>

            <h2>Решения контрольных работ</h2>
            <p>
                Решения контрольных работ пока не завезли...
            </p>

            <h2>Обязательные практикумы</h2>
            <p>
                Обязательных практикумов в курсе 2 - Frama-C и Spin. Все решения,
                которые имеются в наличии, приведены на соответствующих страницах.
            </p>
            <ul>
                <li><a href="framac">Решения практикумов по Frama-C</a></li>
                <li><a href="spin">Решения практикумов по Spin</a></li>
            </ul>
            <p>
                Авторам сайта не удалось найти решения на все задачи, которые были
                в практикумах, поэтому призываем вас добавлять отсутствующие задачи
                и решения. Кроме того, если вы сами решили задачу, у которой уже есть
                решение на сайте, вы поможете будущим поколениям, добавив еще одно
                решение (лишним оно уж точно не будет). Добавлять решения можно как
                через issue в репозитории проекта (это может быть долго), так и через
                pull request. Делать pull request необходимо по инструкциям
                (<a href="spin_database/">Spin</a>, <a href="framac_database/">Frama-C</a>).
            </p>

            <h2>Дополнительные практикумы</h2>
            <p>
                Количество дополнительных практикумов может варьироваться от года
                к году, но в целом их может быть максимум 2. Для этих практикумов
                требуется более творческий подход и к ним предъявляются различные
                требования (по памяти и времени работы). Ниже собраны ссылки на
                различные реализации дополнительных практикумов. Учтите, что не
                все варианты реализаций работают правильно и проходят все лимиты.
            </p>
            <ul>
                <li><b>Реализация алгоритма DPLL</b></li>
                <ul>
                    <li><a href="https://github.com/exesaLigno/DPLLSolver">Солвер на ц++ в исполнении exesaLigno</a></li>
                </ul>
                <li><b>Реализация алгоритма перевода формулы LTL в автомат Бюхи</b></li>
                <ul>
                    <li><a href="https://github.com/exesaLigno/BuchiSolver">
                        Реализация на ц++ в исполнении exesaLigno (есть ветка с
                        автоматической генерацией PDF с подробным решением)
                    </a></li>
                </ul>
            </ul>

            <h2>Литература</h2>
            <ul>
                <li><a href="https://frama-c.com/download/e-acsl/e-acsl.pdf">Туториал по ASCL (первый вариант)</a></li>
                <li><a href="https://frama-c.com/download/acsl-tutorial.pdf">Туториал по ASCL (второй вариант)</a></li>
                <li><a href="https://frama-c.com/download/acsl.pdf">Полный референс гайд по языку ACSL</a></li>
                <li><a href="https://spinroot.com/">Референс по Spin</a></li>

            </ul>
        </div>
    </main>
    <footer>
        <div class="footer-container">
            <div class="footer-text">2025</div>
            <div>
                <button onclick="location.href='https://github.com/fvcrusher/fvcrusher.github.io'" class="footer-link">
                    <svg class="logo" xmlns="http://www.w3.org/2000/svg" width="16" height="16" fill="currentColor" viewBox="0 0 16 16">
                        <path d="M8 0C3.58 0 0 3.58 0 8c0 3.54 2.29 6.53 5.47 7.59.4.07.55-.17.55-.38 0-.19-.01-.82-.01-1.49-2.01.37-2.53-.49-2.69-.94-.09-.23-.48-.94-.82-1.13-.28-.15-.68-.52-.01-.53.63-.01 1.08.58 1.23.82.72 1.21 1.87.87 2.33.66.07-.52.28-.87.51-1.07-1.78-.2-3.64-.89-3.64-3.95 0-.87.31-1.59.82-2.15-.08-.2-.36-1.02.08-2.12 0 0 .67-.21 2.2.82.64-.18 1.32-.27 2-.27s1.36.09 2 .27c1.53-1.04 2.2-.82 2.2-.82.44 1.1.16 1.92.08 2.12.51.56.82 1.27.82 2.15 0 3.07-1.87 3.75-3.65 3.95.29.25.54.73.54 1.48 0 1.07-.01 1.93-.01 2.2 0 .21.15.46.55.38A8.01 8.01 0 0 0 16 8c0-4.42-3.58-8-8-8"></path>
                    </svg>
                    <span class="footer-link-text">Исходники на GitHub</span>
                </button>
            </div>
            <div>
                <button onclick="location.href='https://t.me/ebasoft'" class="footer-link">
                    <svg class="logo" xmlns="http://www.w3.org/2000/svg" width="16" height="16" fill="currentColor" viewBox="0 0 16 16">
                        <path d="M16 8A8 8 0 1 1 0 8a8 8 0 0 1 16 0M8.287 5.906q-1.168.486-4.666 2.01-.567.225-.595.442c-.03.243.275.339.69.47l.175.055c.408.133.958.288 1.243.294q.39.01.868-.32 3.269-2.206 3.374-2.23c.05-.012.12-.026.166.016s.042.12.037.141c-.03.129-1.227 1.241-1.846 1.817-.193.18-.33.307-.358.336a8 8 0 0 1-.188.186c-.38.366-.664.64.015 1.088.327.216.589.393.85.571.284.194.568.387.936.629q.14.092.27.187c.331.236.63.448.997.414.214-.02.435-.22.547-.82.265-1.417.786-4.486.906-5.751a1.4 1.4 0 0 0-.013-.315.34.34 0 0 0-.114-.217.53.53 0 0 0-.31-.093c-.3.005-.763.166-2.984 1.09"></path>
                    </svg>
                    <span class="footer-link-text">Пацанская прога</span>
                </button>
            </div>
        </div>
    </footer>
</body>
</html>