В данной базе собраны все имеющиеся задачи по Spin и их решения. Для удобного просмотра рекомендуется использовать соответствующий раздел сайта
Задачи с описаниями вносятся в файл tasks.json. Схема файла:
[
{
"id": <идентификатор_задачи>,
"name": <имя_задачи>,
"task": <текст_задачи>
},
...
]
Идентификатором задачи в данном случае - это название задачи на английском языке в snake case с годом добавления задачи. Например для задачи “Ханойская башня”, добавленной в 2024 году идентификатор - это tower_of_hanoi_2024.
Если появилась задача, которой не было до этого, рекомендуем сразу создавать pull request, добавляющий эту задачу. Возможно, у нас будут силы и желание ее решить до дедлайна по заданию.
Решения хранятся в папке solutions в виде отдельных файлов в формате .pml. В данном файле может содержаться любой код на языке Promela и любые комментарии, главное, чтобы этот код решал соответствующую задачу. Помимо добавления файла в формате .pml, необходимо внести информацию о созданном файле в файл index.json. Схема данного файла приведена ниже.
{
<название_файла>: {
"task_id": <идентификатор_задачи>,
"startup_cmd": <команда_запуска_spin>,
"comment": <комментарий_к_решению>,
"accepted": <true|false>
},
...
}
При добавлении необходимо добавить запись для каждого добавляемого решения в данный json в соответствии с его схемой. В качестве идентификатора задачи берется идентификатор задачи, для которой добавляется решение (можно посмотреть на сайте или в файле tasks.json). Команду запуска spin необходимо указывать, так как в некоторых (пусть и редких) случаях запуск может отличаться от стандартного. В комментарии крайне рекомендуется указать какие-то комментарии - вопросы, которые задавались к решению, проблемы, которые не удалось решить и прочие подводные данного решения. Также необходимо проставить поле accepted, показывающее, была ли задача успешно сдана. Это поможет другим выбирать проверенные и надежные решения.