Your approach looks interesting: care to share a minimal working example?
Regarding state machines, let me link to this post which describes an approach that works well in practice.
Finally, regarding your question, as I said in the thread you referred to, nothing prevents you to add a fact in this style:
fact { always all m: Machine | m = m' implies m.field' = m.field }
Depending on the context, it may be ok.