[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: Composing modules written in PlusCal
Thank you for the responses. All the details you provided have been useful and helpful in getting me better oriented around this problem. It will take me some time to integrate everything you've highlighted, but I no longer feel stuck, and can proceed in exploring the directions you've pointed me to. I will consolidate around a single PlusCal module for now, but I also have a path towards exploring how to modularize correctly if/when needed.
What does it mean to compose two systems? TLA+ models an execution of a system as a sequence of atomic actions. When systems are modeled in this way, the only general definition of the composition of two systems I know if is that it is a system whose executions are sequences of atomic actions, each of which is an action of one of the two systems.
Let Next1 and Next2 be the next-state relations of the two systems. If both systems are described with the same collection of variables then this definition of composition means that their composition has the next-state relation Next1 \/ Next2. If each has private variables that don't appear in the other spec, as well as variables that appear in both, then one usually defines composition to mean that actions of one of the systems leaves unchanged the private variables of the other. Their composition then has the next-state relation
\/ Next1 /\ UNCHANGED pvars1
\/ Next2 /\ UNCHANGED pvars2
where pvars1 and pvars2 are the tuples of private variables of the two systems.
Ioannis asks the right questions about why you are decomposing the specification. I will point out that re-use of specifications should not be a concern. Specifications are short enough that cut-and-paste is a perfectly satisfactory method of re-using a spec. Re-use of the implementation of a specification may be important. This means that you would like to write a specification of a component, and be able to verify the correctness of a system that uses the component looking only at the component's specification. That problem is what the "Conjoining Specifications" paper is about.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/RCVAYanYY_o/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.