показать контрпример в Alloy

Question

Возможно, это глупый вопрос, но я пытаюсь использовать Разрешить для проверки эквивалентности формул FOL.В случае встречных моделей, есть ли способ показать их?Например,

sig Value {}

pred p [x: Value] {
    // ...
}

assert bla {
  (all x: Value | p [x]) iff (some x: Value | p [x]) 
}

// run p for 2 Value
check bla for 5 Value

Там написано

Executing "Check bla for 5 Value"
   Solver=minisat(jni) Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   16 vars. 5 primary vars. 15 clauses. 1ms.
   Counterexample found. Assertion is invalid. 2ms.

Но когда я нажимаю Counterexample, открывается окно без экземпляров.

Answer 1

Я управлял твоей моделью для тебя.Есть экземпляр.Обратите внимание, что там написано: «Из-за настроек вашей темы каждый атом скрыт. Пожалуйста, нажмите« Тема »и настройте ваши настройки».Это означает, что экземпляр показывается, и если он содержит какие-либо атомы, они не показываются из-за темы, которая настраивает визуализацию.В этом случае это потому, что не связанные целые числа не отображаются в теме по умолчанию.Вы можете увидеть экземпляр, либо просмотрев его другим способом (любой другой вариант - Txt, Table, Tree), либо изменив тему.