====== README ====== Created Monday 09 July 2018

====== Мастерская 9. "Решение головоломок с помощью системы верификации или "Марсоход для козы"" ======

===== Promela и Spin =====

==== Задачи о переправе ====

=== "Лёгкие люди" ===

Переправиться должны 5 человек разного веса (10, 20, 30, 40 и 50 кг). Грузоподъёмность лодки — 60 кг. Однако при загрузке менее 30 кг лодку уносит течением.

Файл спецификации: lh2.pml

=== "Львы_и_террористы" ===

Переправиться должны три скромных льва и три диких террориста. Лодка двухместная. Львы не умеют управлять лодкой, а террористы начинают душить львов, если оказываются в большинстве.

Файл спецификации: Львы_и_террористы.pml

=== "Медленные бабушки" ===

Через ветхий мост тёмной ночью должны перейти четыре бабушки, которые имею разную максимальную скорость. Самая быстрая переходит мост за 1 минуту, остальные — за 2, 5 и 10 минут. Через 27 минут начинается показ очередной серии популярного фильма, но который им надо успеть. У них есть один фонарик, с которым могут идти не более двух бабушек.

Файл спецификации: через_мост.pml

=== Пример спецификации: Миссионеры и каннибалы ===

Переправиться должны три миссионера и три каннибала. Лодка двухместная. Все участники умеют управлять лодкой, а каннибалы нападают на миссионеров, если оказываются в большинстве.

Файл спецификации: river_cannibals.pml

=== Проверка спецификаций из командной строки === Файл run_spin.sh : {{{code: lang="sh" linenumbers="True" #!/bin/bash

if [ "$1" == "" ]; then echo "Usage: $0 file.pml" else # ECHO ON set -x spin -a $1 gcc -DBFS -w -o pan pan.c ./pan spin -t $1 fi }}}

Запуск: ./run_spin.sh ИМЯ_СПЕЦИФИКАЦИИ.pml

Для Windows: файл run_spin.bat : {{{code: lang="sh" linenumbers="True" REM SET UTF-8 chcp 65001 ECHO ON spin -a %1 gcc -DBFS -w -o pan.exe pan.c pan.exe spin -t %1 }}}

(Параметр -DBFS обеспечивает поиск самого короткого пути, ведущего к целевой конфигурации. )

=== Графический интерфейс ispin.tcl === Файл: ispin.tcl

==== C ====

=== Программа, cпрашивающая у пользователя его имя и приветствующая его === Файл: hello_comp/main.c

=== Программа, загадывающая число от 1 до 100 (можно изменить в #define) и отвечающая на попытки пользователя === Файл: number_guesser/main.c

=== Программа, угадывающая загаданное пользователем число от 1 до 100 (можно изменить в #define) === Файл: prog_guesser/main.c

=== Программа, тестирующая готовность пользователя завести шиншиллу === Файл: chay/main.c

=== Программа, загадывающая букву английского алфавита и отвечающая на попытки пользователя === Файл: guess_letter/main.c

==== Javascript ====

Ученики создали картинки для игр, используя программу Krita (бесплатный растровый графический редактор с открытым кодом).

=== Игра-кликер === Веб-страница, показывающая картинку, меняющуюся на другую после нескольких кликов.

Файлы: clicker_game/ clicker.html images/ egg_1.png egg_2.png egg_3.png chi_2.png

=== Игра "Шиншилла, ловец еды" ===

Игра основана на туториале по созданию двумерных игр. ( Исходный туториал (на английском): https://jlongster.com/Making-Sprite-based-Games-with-Canvas Перевод на русский: https://habr.com/post/184666/ Исходный репозиторий: https://github.com/jlongster/canvas-game-bootstrap )

Файлы: food_catcher/ index.html css/ app.css img/ sprites.png try_bg.png js/ app.js input.js resources.js sprite.js