This is a "best practices" question, rather than a question on the language itself.
I am working on breaking my project into modules, following the advice in the Software Abstraction book. I have signatures, facts and predicates for each small piece of my larger model in their own separate files. I have them properly included in my "main file".
For a few of the smaller modules, I found it useful to "prove out" the design by adding traces at that level. Traces are just facts though, so when I run the traces I have created in my main file, I get odd results ("two time steps at once", etc).
I see two options (after either of which I can just complete my main file traces):
Do either of these look correct? Or is this usually done differently?
One of the best things I discovered while using Alloy is to not use facts but use predicates instead. You can control which predicates are active in a run or assert. You can always combine predicates so it is not much of an inconvenience.