I am not familiar enough with how systems are specified in process algebra to make an informed comparison. Also, I have never really attempted to spread PlusCal processes over different modules, and I don't think that PlusCal was designed with this kind of modularity in mind. When you do that, the PlusCal translator will produce a TLA+ specification corresponding to each of the parts, and you could in principle take their conjunction to be the specification of the overall system. In fact, the slogan "composition is conjunction" is quite prominent in the TLA(+) literature, and this resembles the process algebra view where you have explicit composition operators for building an overall system model out of individual process specifications.
In practice, we want to use TLC to verify our specification, and it expects specifications to be written in the standard form
Init /\ [Next]_vars /\ L
Therefore, you will want to assemble the overall initial condition and the overall next-state relation as the conjunction, respectively disjunction, of the individual formulas. Similarly, you will assemble the overall fairness conditions to build the one for the complete specification. In that sense, neither the safety nor the liveness part of the specification "get imported" as a whole from the individual modules, but you do get the individual pieces for assembling the specification.
Does this make sense?
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.