Very long message indeed, too long for me 
But, regarding your questions about difficulties, your step predicate and events seem non-standard. You may find this post helpful (stop before the Event Reification section, it’s confusing for a newcomer). This tutorial/lecture notes may also be useful.
Not particularly, the standard way to model such a spec in Alloy (and detailed in the links pointed to above) is similar to TLA+.