I am at the moment only interested in specifications that have actions in them. For me, an action is a form of abstract vector. And Next is a form of a vector field where at each point , there might be multiple actions.
Can we omit the initial conditions in a spec where Next is a union of actions? In the original specification, the initial conditions were crucial, because they needed to respect a global invariant so that the spec refined TCommit.
In my revised spec, I have made the actions more strict, they have complete information about all the variables. I added an Init so as that TLC would accept it for model checking. Pick any Init value for both TCommit and Two Phase Commit.
You will see that the refinement still holds. In my revised spec, there is no need to prove that a global invariant holds.
The reason we do not want the revised spec is because , in reality , most agents work under incomplete information, so we cannot assume that they know everything.
I am trying to identify certain categories of Specs and their morphisms/refinements. (at the moment without liveness properties)
1. Specs with actions without Init, where no global invariant is needed.
2. Specs with actions with Init because a global invariant is needed.
3.Specs where the restrictions is a general temporal formula (with possible liveness properties)
The question was whether the 2nd category is different from the 1st. It seems to me that it is.
Another interesting question is if the 3rd category didn't have liveness properties, only safety properties would it then collapse to the 2nd category. Are there general safety specifications that cannot be written in the form of actions?