Подсчет количества Total CounterExamples в Alloy

Вызов

Kodkod.execute()

метод возвращает объект A4Soluiton, который мы можем повторять с помощью метода next(), пока он не достигнет контрпримера, который является неудовлетворительным(). Таким образом, мы можем подсчитать общее количество контрпримеров, найденных решателем.

Мой вопрос заключается в том, можно ли узнать общее количество контрпримеров непосредственно из объекта A4Solution без его повторения.

Большое спасибо заранее за ваш ответ.


alloy
person Narnia_Optimus    schedule 03.09.2013    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы не можете получить общее количество контрпримеров заранее, т. е. без перечисления по одному.

person Aleksandar Milicevic    schedule 03.09.2013
comment
Вы знаете, как это работает внутри? Насколько я понимаю, объект решения, возвращаемый функцией Kodkod.execute(), содержит все контрпримеры. Другими словами, вызов next() для объекта решения не выполняет команду для поиска нового контрпримера, а выполняет обход объекта решения. Я прав? - person Narnia_Optimus; 03.09.2013
comment
Нет, решение, возвращенное Кодкодом, содержит только один контрпример, поэтому ему нужно снова выполнить ту же команду, чтобы найти новые. Он просто добавляет новое ограничение к существующей модели, чтобы гарантировать, что последующие решения (контрпримеры) отличаются от текущего, а затем повторно запускает решатель (т. е. Kodkod.execute()) - person Aleksandar Milicevic; 04.09.2013
comment
В графическом интерфейсе Alloy при выполнении утверждения результат показывает два значения времени, как показано ниже. 2937 vars. 1008 primary vars. 5676 clauses. 555ms. Counterexample found. Assertion is invalid. 117ms. Знаете ли вы, что означают эти две цифры времени? Нужно ли суммировать эти две цифры, чтобы рассчитать общее время для контрпримера? - person Narnia_Optimus; 04.09.2013
comment
Да. Первое число (555 мс) — это время перевода (время, которое требуется Alloy и Kodkod для перевода модели в CNF), а второе число (117 мс) — это время решения. (время, которое требуется решателю SAT, чтобы найти решение для переведенной формулы CNF) - person Aleksandar Milicevic; 04.09.2013