(a) Программа P, которую Slam проверяет на выполнение правил блокировки (б) На первом этапе модификации модели Slam генерирует булеву программу (в) Затем Slam улучшает модель так, чтобы удалить невозможные варианты выполнения, которые порождают ложные результаты («*» указывает, что выбор не определен)