Вы видите только SAT4J? Просто проверка работоспособности: вы нажимаете на меню «Параметры», а затем на строку с надписью «Решатель: SAT4J», верно?
Когда вы это сделаете, вы должны получить подменю со списком решателей SAT; в моей системе это выглядит примерно так:
Надеюсь, это поможет. Если это не так, я ожидаю, что следующее, что нужно спросить, это то, что показывает диалоговое окно About Alloy. (Для сравнения: только что приведенный скриншот был произведен билдом 2014-05-16.)
[Постскриптум]
Ах. Верно. Ваш опыт ясно показывает, что подразумевается под примечанием в документации. :
По умолчанию выбран чисто Java-решатель "SAT4J", поскольку он работает на любой платформе и в любой операционной системе. Если вам требуется более высокая производительность, вы можете попробовать один из собственных решателей, например MiniSat или ZChaff.
Из этого (сейчас) я делаю вывод, что решатели, отличные от SAT4J, не все (или, возможно, некоторые из них) являются чистой Java, а требуют собственного интерфейса (т.е. интерфейса для кода, написанного на других языках). Если JNI не работает на вашей платформе, как указано в предупреждающем сообщении, SAT4J может быть единственным доступным решателем.
Возможно, кто-то из команды разработчиков сможет прокомментировать.
Поэтому, если вы не можете переключиться на Unsat Core, чтобы выяснить, почему в вашей модели нет экземпляров, вы вынуждены использовать другие методы.
Один метод очевиден (хотя и довольно утомителен): бинарный поиск по набору ограничений в модели.
Если вы понимаете, о чем я, и не можете придумать лучшего подхода, то пока и удачи.
Если вы понимаете, что я имею в виду, и можете придумать лучший подход, расскажите остальным, что это такое.
Если вы не понимаете, что я имею в виду, метод, который я имею в виду, напоминает широко используемый метод поиска синтаксических ошибок в программе, когда вы понятия не имеете, где они находятся. (Смутная память подсказывает мне, что я, возможно, узнал об этом, читая книгу Джона Бентли Programming Pearls. Возможно.) Вот один из способов сделать это.
Сделайте резервную копию модели в ее текущем состоянии. Он понадобится вам позже, когда вы начнете задаваться вопросом, изменилась ли та или иная крошечная деталь или нет.
Измените все ваши именованные факты на именованные предикаты. (Если окажется необходимым, также измените все свои подписные факты и даже другие ограничения на именованные предикаты. Я делаю это только тогда, когда у меня нет альтернативы, так как это требует переписывания большей части модели, чем я. хотел бы.)
Создайте новый предикат И объедините все ваши именованные предикаты. В дальнейшем я буду называть это AllTogetherNow. Он будет иметь форму что-то вроде
pred AllTogetherNow {
P1
P2
P3
...
Pn
}
На этом этапе ваша модель должна состоять из сигнатур (с фактами сигнатуры или без них) и именованных предикатов, а не из фактов.
Убедитесь, что модель может быть создана, когда AllTogetherNow не соответствует действительности.
Если его невозможно создать, а у вас все еще есть сигнатурные факты, вернитесь к шагу 2 и вынесите некоторые или все из них. Пересмотрите AllTogetherNow, чтобы включить новые факторизованные ограничения.
Если его невозможно создать и у вас нет никаких фактов подписи, вернитесь к шагу 2 и вынесите ограничения, неявные в ограничениях количества элементов для ваших подписей. Пересмотрите AllTogetherNow, чтобы включить новые факторизованные ограничения.
Проверьте, можно ли создать экземпляр AllTogetherNow.
Если его можно создать, значит что-то изменилось между вашей исходной моделью и настоящей. Изменилось то, что было не так в исходной модели.
Закомментируйте половину предикатов, находящихся в настоящее время в AllTogetherNow, выбранных либо хитростью, либо случайным образом.
Проверьте, можно ли создать экземпляр AllTogetherNow.
Если это невозможно, то какое-то подмножество предикатов, действующих в настоящее время в AllTogetherNow, содержит противоречие. Вернитесь к шагу 6, чтобы закомментировать еще несколько предикатов.
Если теперь можно создать экземпляр AllTogetherNow, то некоторое подмножество предикатов, которые вы только что закомментировали, является причиной того, что модель не может быть создана в том виде, в каком она была написана изначально. Перейдите к шагу 8.
Раскомментируйте половину ограничений, закомментированных в настоящее время в AllTogetherNow, выбранных либо случайно, либо хитростью. Вернитесь к шагу 7.
Мой опыт показывает, что несколько циклов по шагам 6-8 обычно помогают сосредоточить мое внимание достаточно, чтобы я мог в конечном итоге увидеть, в чем заключается противоречие. Основные трудности, с которыми я столкнулся (YMMV), заключаются в том, что (1) первоначальный набросок модели не ограничивается одним противоречием, (2) противоречия могут возникать из-за неудачных комбинаций предикатов, которые по отдельности безвредны, и (3) существует может быть более чем один способ создать противоречивую комбинацию (предикаты A, B, C и D хороши каждый; A фатален в сочетании с B или C...).
Одна психологическая трудность, которая может возникнуть, заключается в том, что противоречия возникают не в «интересной» части модели, а в попытке подготовить почву для интересных вопросов. Я не знаю другого лекарства от этого, кроме как сказать себе, что любое неожиданное противоречие автоматически интересно и стоит того, чтобы на него потратить время. Иногда мне удается себя уговорить.
person
C. M. Sperberg-McQueen
schedule
26.03.2015
