[hwayne]

I used LTL because it's simple enough to explain the core ideas without getting bogged down in affordances and details. It's purely a pedagogical choice, just like how nobody explains the halting problem in terms of Java.

Switching to a different notation helps with some of the practical details, but doesn't remove the essential problems that arise in composing specs.

[scotty79]

The sorce of the problem with composability in this post is that you don't have a concept of sub-states and 'partial next' operators.

[hwayne]

Would you be willing to provide a full example, replicating the dependent spec?

[Pet_Ant]

I'm wondering if you could as part of the O operator list all the variables in consideration for the "next"-state asar as that operator is concerned.

like O[a,b,c]X in the next state which is determined by a change to any of a, b, or c, then X will be true. In the case where the set of variables is all of them they can be omitted and thus get the existing behaviour.

I also suspect that the O operator with with a subset of variables will behave identically to other instances with the same set.

However, I feel like this will still hit walls before practical limits, Beth would just need a non-trivial example