Это команда mace4, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
mace4 - ищет конечные контрмодели операторов первого порядка
СИНТАКСИС
mace4 [кредита] входной файл > выходной файл
ОПИСАНИЕ
Эта страница руководства кратко документирует mace4 команда.
Программа mace4 поиск конечных структур, удовлетворяющих
заявления, такие же утверждения, которые испытатель9(1) принимает. Если это утверждение
отрицание некоторой гипотезы, любые структуры, найденные mace4 контрпримеры к
Гипотеза. mace4 может быть ценным дополнением к испытатель9(1), ищем контрпримеры
до (или одновременно с) использованием испытатель9(1) искать доказательство. Это также может быть
используется для отладки предложений ввода и формул для испытатель9(1).
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
Сводка опций приведена ниже. Параметры имеют приоритет над эквивалентными настройками, указанными в
входной файл. Чтобы установить или сбросить флаг, вы должны указать 1 или 0 в качестве значения.
-Помощь Это говорит mace4 чтобы напечатать сводку этих параметров командной строки.
-n n Это дает начальный размер домена для поиска. Значение по умолчанию - 2. Если вы
также дать -N вариант, mace4 будет увеличивать размер домена через -N стоимость,
используя приращение, заданное -I ценить. Иначе, mace4 будет искать только
-n значения.
-N n Это дает размер конечного домена для поиска. По умолчанию - 10.
-i n Это дает приращение размера домена для поиска. По умолчанию 1.
-q n Этот флаг отменяет повторение параметра. Он говорит, что нужно попробовать простые размеры
числа, от -n через -N.
-m n Прекратите поиск, когда nнайдена ая структура. По умолчанию 1.
-t n Прекратить поиск после n секунд.
-s n Разрешить не более n секунд для каждого размера домена. Параметр можно использовать (вместе
-t), чтобы указать общий срок.
-b n Прекратить поиск, когда (о) n были использованы мегабайты памяти.
-V n Требуется правило для отличия переменных от констант в разделах и
формулы со свободными переменными. Если этот флаг снят, переменные начинаются с (нижний
case) от `u 'до` z'. Если этот флаг установлен, переменные в предложениях начинаются с (верхний
case) от `A 'до` Z' или `_ '.
-P n Если этот флаг установлен, все найденные структуры печатаются в "стандартной" форме,
что означает, что они подходят в качестве входных данных для других программ LADR, таких как изофильтр(1)
и интерпформатировать(1).
-p n Если этот флаг установлен, и если -P ясно, все найденные структуры распечатаны
в табличной форме.
-R n Если этот флаг установлен, к поиску применяется кольцевая структура. Операции
Предполагается, что {+, -, *} кольцо целых чисел (mod domain_size). Этот метод ставит
жесткие ограничения на поиск, что позволяет
исследовалась.
-v n Если этот флаг установлен, выходной файл получает информацию о поиске,
включая исходную частичную модель (ту часть модели, которая может быть определена
перед началом поиска с возвратом), а также временную и другую статистику для каждого размера домена.
(Он не дает следов возврата, поэтому не потребляет много файлов
пространство.)
-T n Если установлен флаг трассировки, подробная информация о поиске, включая трассировку
всех присваиваний и возвратов выводится на стандартный вывод. Этот флаг
вызывает много вывода, поэтому его следует использовать только при небольших поисках.
Также существует ряд дополнительных опций, которые используются для экспериментов с
методы поиска. Их могут игнорировать почти все пользователи. Для описания этих
варианты см. оригинал mace4 руководство.
Используйте mace4 онлайн с помощью сервисов onworks.net
