====================================================================== As this file is an ASCII conversion of a WORD file, the following notation has been used: - accents have been appended as quotes (' or `) or as ~ - bullets has been replaced by hyphens - OMEGA stands for Courtiat's omega operator - FORALL stands for the corresponding logic operator ====================================================================== ISO/IEC JTC1/SC21/WG7/E-LOTOS interim meeting Paris, 6th-8th of February 1995 0. Attendance list Arnaud Fe'vrier, E.N.S.T., France, fevrier@res.enst.fr Hubert Garavel, INRIA, France, hubert.garavel@imag.fr Alan Jeffrey, University of Sussex, United Kingdom, alanje@cogs.susx.ac.uk Guy Leduc, University of Lie`ge, Belgium, leduc@montefiore.ulg.ac.be Luc Le'onard, University of Lie`ge, Belgium, leonard@montefiore.ulg.ac.be Luigi Logrippo, University of Ottawa, Canada, luigi@csi.uottawa.ca Eric Madelaine, INRIA, France, Eric.Madelaine@sophia.inria.fr Jose Man~as, University of Madrid, Spain, pepe@dit.upm.es Elie Najm, E.N.S.T., France, najm@res.enst.fr Abdelbarim Nimour, E.N.S.T., France, krimo@res.enst.fr Koji Okada, Electrotechnical Laboratory, Japan, kokada@etl.go.jp Juan Quemada, Tech. Univ. of Madrid, Spain, jquemada@dit.upm.es Jan Tretmans, University of Twente, The Netherlands, tretmans@cs.utwente.nl 1. Appointment of a secretary L. Logrippo and G. Leduc volunteer. 2. Agenda The following agenda is agreed on: - List of input documents - Rapporteur's report - Presentation of input documents - Progression of work item - The behavioural and data models of E-LOTOS - Planning of revised working draft - Coordination and liaison issues - Closing 3. List of input documents PAR1: Comments from Japan on "Enhancements to LOTOS" (Japanese experts) PAR2: Generalized termination, enabling and disabling (AENOR & Canadian expe= rts) PAR3: Defining equivalences between time/action graphs and timed actions graphs (Spanish experts) PAR4: Progress of E-LOTOS (AFNOR) PAR5: Comments on Belgian Spanish proposal for a time-extended LOTOS (AFNOR) PAR6: Integrating Timing and Mobility in LOTOS: MT-LOTOS (AFNOR) PAR7: Extending Gate Typing to Mobile LOTOS (AFNOR) 4. Introduction J. Quemada reports on the last period. WG1 is disbanded and the E-LOTOS project is moving to WG7, starting with the SC21 plenary in Ottawa. 5. Presentation of contributions PAR1: K. Okada presents the paper. Main concerns are: "batch" approach for progression and upward compatibility. Comments are provided on enhancements. PAR2: J. Quemada presents the joint Canadian-Spanish contribution. It combines "generalized termination" with the "suspend-resume" operator. PAR3: J. Quemada presents the contribution, which addresses the equivalence between time/action graphs and timed action graphs. The aim is to show equivalence between Spanish and Belgian proposals of Timed LOTOS. PAR4: E. Najm presents this contribution on the progress of E-LOTOS. Main concerns are: the selection of important items, proper link to ODP, and integration of extensions in the language. PAR5: E. Najm presents a contribution on time in E-LOTOS. Main concern is the increased semantic complexity of the combined Belgian-Spanish proposal. 6. Progression of the E-LOTOS project There appears to be a wide support for a batch approach where a set of needed, mature, compatible, and widely accepted enhancements is selected for inclusion and progression in the amended standard. It has been envisaged that the next ISO meeting in Ottawa will be the appropriate place to assess the various enhancements and decide on the content of a first draft. Agreement on time seems to have been reached , but conflicts are seen in data types and gate typing and tagging. The following list of discussion items was agreed on in the following order: - Data types (annexes F, H, I) - Time (annex E, PAR6) - Mobility (annex J, PAR6 and PAR7) - Tagged and typed gates (annexes C and D, PAR7) - Modules (annexes F, G) - New operators (annexes A, B, PAR2) - Six improvements (annex K) 7. Data types G. Leduc explains the idea of annex H. The proposed data formalism includes an algebraic data model, on which a functional "core language" is defined. On this, an "extended language" involving syntactic sugar such as "if-then-else" and "case" can be defined. J. Ma=F1as explains the rational behind annex I, and his criteria to choose = a data type mechanism for E-LOTOS. Emphasis is on equational versus rewrite/functional semantics and locality of definition. Upward compatibility considerations then generate a discussion on the idea of having both algebraic and functional definitions (Larch, ACT ONE and Extended ML were cited as possibilities). 8. Time The formal properties of the Belgian-Spanish proposal (annex F) were discussed. A weak timed bisimulation congruence may be needed. Discussion continues on PAR5, and on time-related aspects of PAR1. Various assessments were given of the appropriateness of the technical comments. These comments will be further resolved and answers will be provided. =46ebruary 7, 1995 9. Mobility E. Najm introduces the discussion on mobility in LOTOS. The proposal is deemed sound and fairly mature. PAR6 integrates time and mobility in E-LOTOS. This integration can be made upward compatible with standard LOTOS. An advantage is to combine the expressiveness of p-calculus and the one of standard LOTOS, but the model features the simultaneous existence of two different parallel composition operators (the LOTOS one and a CCS-like one), which raised questions of uniformity and added complexity. Further studies are also needed to compare M-LOTOS and LOTOS specifications on case-studies (e.g. ODP computational viewpoint). 10. Typed tagged gates J. Man~as presents the ideas of annex D. In this extension, it is possible to restrict experiments to certain data types. It is also possible to define gate types as "union" of other types. A possible semantic model is to add tags to events in the labelled transition system. The impact of that on the whole semantics of LOTOS is unclear. Another semantic model is based on static analysis of gate typing. H. Garavel presents a related proposal (annex C) which differs from the previous one in that it allows mixing of positional and tagged representations, and also untyped gates. E. Najm also presented a related proposal, which uses an explicit order of fields for type union, plus allowing static treatment of behaviour analysis. This feature is based on the use of the subtyping relation. The three experts are requested to work towards an agreement on this topic. 11. Modularity J. Man~as explains the concepts of annex G. Problems of ambiguities and transitivity of exporting were discussed. It is claimed that this proposal is simpler and more homogeneous than the proposal of appendix F. Further discussion dealt with problems of separate compilation and module reusability. The committee encourages J. Man~as to develop a more complete proposal. 12. New operators J. Quemada presents the concepts of generalized termination, enabling and disabling. This combines two independent contributions by Spain and Canada. Ways to clarify the presentation of the inference rules were suggested. The extension with time is still to be considered, because after suspended process is resumed, time has elapsed. Alternatives were discussed to eliminate compound events. 13. Six improvements H. Garavel discusses the six improvements proposed in annex K. It appears that these improvements are on static semantics concerns, and it is premature to consider them at this point. Annex K will be kept as is until all the main design choices are made. =46ebruary 8, 1995 A discussion took place on how to progress work on enhancements. Because of the fact that the LOTOS group is joining WG7, and else because of growing importance of the area of Open Distributed Processing, it was decided that an output statement be sent to WG7, asking for requirements on how to make the language more tailored to ODP applications. 14. Data type part The following approach for the data part was discussed and adopted: Integrated use of equational requirements and functional semantics (with a clear interface to external languages). A working group, coordinated by A. Jeffrey and initially composed of H. Garavel, E. Najm, J. Man~as, J. Tretmans, K. Okada and G. Leduc will make a proposal for the Ottawa meeting. The milestones are: - end of April: skeleton proposal to be included in the output document of this meeting - end of June: first draft of the document. Another group is selected, composed of H. Garavel, E. Najm and J. Man~as, to make a common proposal on typed/tagged gates. To help to resolve conflicts among the existing proposals, the following list of items were discussed: - untyped gates - mixing positional and tags in action structures - the '...' notation - merge of types - changes in dynamic semantics - structural subtypes Untyped gates: a majority is in favor of keeping untyped gates in addition to typed ones. Mixing positional and tags: question undecided The '...' notation is approuved. The discussion on the remaining points was postponed. 15. Structure of the output document The output document will contain the following annexes: - data types (skeleton proposal) - typed/tagged gates (containing references to three existing documents and stating that the question is on hold until a proposal exists for data types) - time - mobility - modules - operators - six improvements - integration issues The deadline for contributions is April 30, 1995. 16. Next meeting Ottawa, 20th to 26th of July 1995. ------------------------ANNEX----------------- Resolution of AFNOR comments (ISO/IEC JTC1/SC21/WG1 N1355) Technical comment 1 These comments do not require any resolution. They simply state neutral facts about the language. We could even provide other possible equivalent behaviour expressions such as: a {t} [t ge d1 and t le d2]; P Technical comment 2 This comment is a well-known fact described in the proposal. It is recognized that nondeterministic delays introduced by i{d1..d2} may have side effects in choice contexts, viz. they may resolve the choice. We acknowledge that there is also a discussion about that in [CdO94]. Basically, this problem has its roots in standard LOTOS where a distinguished internal event is used to model nondeterministic choices in general. Technical comment 3 This comment is a well-known fact described in the proposal. Although not mentioned in the proposal, it is clear that congruence is also lost in enabling contexts because the enabling operator is just a special kind of hiding operator. Technical comment 4 Correct. This is a minor problem that will be fixed. Technical comment 5 These rules have not been modified to get time additivity. In fact, these rules had been changed in ET-LOTOS before it has been merged with T-LOTOS for another reason. We then realized afterwards that time additivity was achievable without additional cost. The basic reason for changing these rules is that the previous rules were based on the assumption that the so-called reverse persistency property was fullfilled. This was true in Basic ET-LOTOS, but it was unfortunately impossible to preserve it in full ET-LOTOS due to the presence of selection predicates in action-prefix expressions. Technical comment 6 The only motivation is to allow the description of an infinite number of interleaved parallel processes. The following Time Extended LOTOS expression is not adequate because, as any unguarded recursion, it blocks time: Ps :=3D P ||| Ps. Technical comment 7 It is a matter of syntactic taste on which the group has not reached a consensus yet. Proposal 1 Semi-open intervals do not seem necessary. Precluding time sorts in choice expressions would be too restrictive. This construct allows very nice specifications of periodic offers like in: P (n:nat) :=3D choice t:discrete_time [] a{n*t..n*t}; P' Proposal 2 The latency operator proposed in [CdO94] does not solve the problem in general. It is useful in very few cases, but on the other hand adds unacceptable complexity in the semantics. In the semantics presented in [CdO94], actions are decorated with a parameter that indicates whether they are subject to maximal progress or not, when being hidden. The natural state for an action is to be subject to maximal progress. However the effect of (OMEGA d P) is that for d time units, the actions of P are not subject to the maximal progress. For example: in (hide a in a;P) the hidden a must occur immediately, but in (OMEGA 5 a;P), for the first 5 time units, a is not subject to the maximal progress. The result is that in (hide a in OMEGA 5 a;P), the hidden a can occur at any time before 5 and only becomes urgent at time 5 if it has not occurred yet. The situation is similar in (hide a in (a;P |[a]| OMEGA 5 a;Q)). In fact, in these last two processes, OMEGA 5 simulates the effect of a nondeterministic delay between 0 and 5. It is clear that OMEGA d does not really introduce a delay. But in some contexts, it gives a result similar to the one that can be obtained with i{0..d}, with the advantage that it does not cause the occurrence of an internal event. The contexts where (OMEGA d) can be used to simulate a nondeterministic delay are however very restricted. In i{0..d}; P, P does not evolve in time as long as i has not occurred. This is not the case with (OMEGA d P): P immediately evolves in time. (OMEGA d P) thus only simulates the introduction of a delay d before P in cases where FORALL t:time, we have P -t-> P; in other words when the passing of time has no influence on P. It does not work for example with OMEGA d a{d1..d2); P, or with OMEGA d a{t}; P(t). Another restriction of the approach of [CdO94] is illustrated by the following example: i{0..5}; (a;P ||| b;Q) is not similar to OMEGA 5 (a;P ||| b;Q). In i{0..5}; (a;P ||| b;Q), a and b are enabled at the same time, fixed by the occurrence of i. On the other hand, OMEGA 5 (a;P ||| b;Q) is in fact similar to (OMEGA 5 a;P ||| OMEGA 5 b;Q) the "delay" it introduces can be different for a and b. In (hide a,b in (i{0..5}; (a;P ||| b;Q))), a and b will be occur at the same time, what is the logical effect. This is not the case with (hide a,b in OMEGA 5 (a;P ||| b;Q)). In fact, (OMEGA d P) is only similar to the introduction of a nondeterministic delay before P in the cases where P can just do a single action. In conclusion, the only cases where (OMEGA d) brings an advantage to simulate a nondeterministic delay are (OMEGA d a;P) (without any time attribute on a) and (OMEGA d exit). In the other cases, i{0..d} is still necessary. On the other hand, the introduction of (OMEGA d) is obtained by an important increase of the complexity of the semantics, as the action labels must be decorated with an auxiliary parameter. Proposal 3 It is a solution to a non-problem, and is therefore rejected. Proposal 4 Not resolved. Proposal 5 Not resolved. Proposal 6 The operator proposed in [CdO94] adds unacceptable complexity in the semantics, whereas no convincing evidence of its suitability is presented.