Checking your assertions

You may be making some wrong assumptions about the role of assertions, facts, check instructions, etc.

The Alloy Analyser doesn't check assertions except when you specifically ask it to; assertions are typically used to claim that a particular state of affairs follows logically from other constraints in the model, so there is no need to check assertions on each run.  

You have several unnamed assertions, but no check commands for them.   In my version of Alloy, at least (v 4.1.9, about a year old and so possibly a bit out of date), an assertion like assert { some s1,s2:SyncGraph | s1.edge != s2.edge } not only is not checked automatically by Alloy, but since there's no check command, there's no way to ask Alloy to check the assertion.  

When I add a name to the assertion (so it reads assert a1 { some s1,s2:SyncGraph | s1.edge != s2.edge }), and then add a check command for it (check a1) the Analyser adds the entry "Check a1" to the Execute menu.  (Or you can just change assert to check, and the menu item will generate an identifier for it.)

And when I ask Alloy to check that first assertion, yes, it quickly finds a counterexample.

So I think the most likely explanation is that the assertions in your model did not, in fact, "all ... pass ... as assertions".  The assertions are inert until you explicitly ask the Analyser to check them, just as predicates are inert until you explicitly ask the Analser to run them. THEN counterexamples or instances are sought.

Good luck, and keep going!  

I hope this helps.

--C. M. Sperberg-McQueen
  cmsmcq@blackmesatech.org
  http://cmsmcq.com/mib