Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
ASLan++ operator
!G
G_1 & G_2
T_1 = T_2
T_1 != T_2
151/190
ASLan predicate
not(G)
G_1.G_2
equal(T_1,T_2)
not(equal(T_1,T_2))
Table 11: Substitutions done by the adaptGuard function
4.9
Translation of Terms
In § 4.7, we presented a procedure for translating ASLan++ statements into ASLan transitions, but we did not apply any translation of terms. There are two reasons behind this:
• Split the translation into a higher level (of statements) and a lower one (of terms
contained in them), allowing for cleaner exposition and ease of understanding.
• In most cases, ASLan++ terms can be easily replaced by equivalent terms in ASLan
by means of semantically equivalent predicates. However, there are a few exceptions
(e.g. set literals and assignment of variables by pattern matching) that can not be
handled by simply replacing the term with another, as they affect the entire resulting
rule for the statement that contains the term.
The approach followed is therefore to defer translation of terms, carrying over the original
ones during translations of statements (and guards included in them), and then apply a term
translation procedure to the generated rule, which we describe in the following.
Consider a rule R of the form
LHS =[exists E]=> RHS
and let us apply the procedure to R. Suppose that R is now in an intermediate state where
both ASLan and ASLan++ predicates (namely, transmission events) may appear, of which
only the latter need be translated but all need be processed recursively for contained terms.
For each predicate in R, we recursively traverse each (sub-)term T according to its syntactic
form, obtaining the following cases:
• T = c, i.e. T is a constant c. In this case we leave c as is.
• T = V, i.e. T is a variable V. The case is similar to the above one for constants, except
that the variable name must be bound to its value. Therefore we add the state fact of
the owner of V to both LHS and RHS of R.
• T = [T_1], i.e. T is a pseudonym term T_1 (which must be of type agent or of a
subtype of it). Then T will be replaced by
defaultPseudonym(T_1’,IID) if T_1 is Actor
T_1’
otherwise
where T_1’ is the recursive translation of T_1 and IID is the instance ID of the current
entity.
FP7-ICT-2007-1
Project No. 216471