vigder@cygnus.sce.carleton.ca (Mark Vigder) (06/20/91)
I've been using LOTOS as a specification language for concurrent
software and I've run into some issues regarding LOTOS semantics which
I'm not sure I understand. I've been reading the LOTOS standard trying
to figure out the answers, and despite the clarity and nice
explanations contained within the standard :-) I'm not sure that my
interpretation of the standard is correct. I would appreciate any
help that people fluent in LOTOS could provide me. The questions are
rather detailed and probably not of general interest, so e-mail
responses may be best to save on net traffic.
Given a LOTOS specification L, the semantics of L is defined by first
applying a 'flattening function' #.#, and then defining the transition
system in terms of the flattened specification #L#. However, the
function #.# is a partial function; LOTOS specifications which are not
in the domain of #.# do not fulfil the static semantic requirements.
Now the way I understand this, there exist LOTOS specifications which
are syntactically correct, but which have no semantics. This leads to
the following questions:
-Is my understanding correct?
-If yes, what are the class of syntactically correct LOTOS
specifications which have no semantics?
-Can it be statically determined whether a specification
satisfies the static semantic requirements? (I sure hope so :-)
My second set of questions deals with the issue of unguarded
recursion. I have been warned by LOTOS experts to avoid the use of
unguarded recursion. However, one of the things which I have done as
part of my research is define a transformation phi, which transforms
one LOTOS spec into another. Given specification L, the transformed
spec phi(L) may contain unguarded recursion. This isn't really a
problem for me, provided that my interpretation of what unguarded
recursion means is correct.
For a specification L, the event a is accepted by L if there exists a
behaviour expression L' such that there exists a finite length
derivation according to the semantics of LOTOS which shows that L-a->L'.
Assume you have the following (pseudo-)LOTOS specification:
P[a]
where
P[a] := a;P[a] ||| P[a]
The following derivation "proves" that P[a] -a-> (P[a]|||P[a]):
a;P[a] -a-> P[a] -axiom b
(a;P[a]|||P[a]) -a-> (P[a]|||P[a]) -inference rule g
P[a] -a-> (P[a]|||P[a]) -inference rule k
(process instantiation)
Further derivations can prove the following:
if P[a] := a;P[a] || P[a]
then P[a] deadlocks
if P[a] := a;P[a] [] P[a]
then P[a] -a-> P[a]
if P[a] := exit ||| P[a]
then P[a] deadlocks
Do I understand unguarded recursion? Are all the above statements
correct? Comments? Suggestions?
Thanks for any help that may be forthcoming.
================================================================
Mark Vigder
vigder@sce.carleton.ca
Dept. of Systems and Computer Engineering
Carleton University
Ottawa, Canada