no instances in a counterexample

[arademaker]

See https://stackoverflow.com/questions/58147352/show-counterexample-in-alloy/58156811#58156811

[dnjackson]

Hi Alexandre,

I ran your model for you. There is an instance. Notice that it says "Due to your theme settings, every atom is hidden. Please click Theme and adjust your settings". This means that an instance is being shown, and that if it contains any atoms, they're not shown because of the theme that customizes the visualization. In this case, it's because unconnected integers are not shown in the default theme. You can see the instance either by viewing it in a different way (any of the other options -- Txt, Table, Tree), or by changing the theme.

Daniel

On Sep 29, 2019, at 2:25 PM, Alexandre Rademaker notifications@github.com wrote:

See https://stackoverflow.com/questions/58147352/show-counterexample-in-alloy/58156811#58156811 https://stackoverflow.com/questions/58147352/show-counterexample-in-alloy/58156811#58156811 — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AlloyTools/org.alloytools.alloy/issues/94?email_source=notifications&email_token=AAHAEYW7MI2OQLTP4RRULB3QMDXH5A5CNFSM4I3TPUR2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HOMVIZQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AAHAEYWIOD4WCCSPYSLFSTTQMDXH5ANCNFSM4I3TPURQ.

[arademaker]

Thank you @dnjackson, but if I asked for the Txt or Tree view, I only get empty models.

[aleksandarmilicevic]

An empty model is still an instance. (in which your "all p: Value | ..." assertion trivially holds)

If you want to disallow empty models, add "some Value" to your assertion.

On Sat, Oct 5, 2019, 9:55 AM Alexandre Rademaker notifications@github.com wrote:

Thank you @dnjackson https://github.com/dnjackson, but if I asked for the Txt or Tree view, I only get empty models.

[image: image] https://user-images.githubusercontent.com/86403/66258107-ae207d00-e777-11e9-9930-01b1c6befe87.png

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AlloyTools/org.alloytools.alloy/issues/94?email_source=notifications&email_token=AA3QGLOW4NYL2ZORRB4X3OTQNDBGNA5CNFSM4I3TPUR2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEANWU6A#issuecomment-538667640, or mute the thread https://github.com/notifications/unsubscribe-auth/AA3QGLJJ4Z5MSPJ5PPKO46LQNDBGNANCNFSM4I3TPURQ .

[hwayne]

The empty model is a counterexample to the statement

  (all x: Value | p [x]) iff (some x: Value | p [x]) 

(∀ x ∈ {}: F) /\ !(∃ x ∈ {}: F) is a counterexample to your assertion.

[pkriens]

thinks this was answered ?