Skip to main content
summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat (limited to 'syntaxes/FIACRE/Compiler/FIACRE2LOTOS.atl')
-rw-r--r--syntaxes/FIACRE/Compiler/FIACRE2LOTOS.atl920
1 files changed, 920 insertions, 0 deletions
diff --git a/syntaxes/FIACRE/Compiler/FIACRE2LOTOS.atl b/syntaxes/FIACRE/Compiler/FIACRE2LOTOS.atl
new file mode 100644
index 0000000..c0fe5c7
--- /dev/null
+++ b/syntaxes/FIACRE/Compiler/FIACRE2LOTOS.atl
@@ -0,0 +1,920 @@
+-- @atlcompiler atl2006
+module FIACRE2LOTOS;
+create OUT : LOTOS from IN : FIACRE;
+
+rule Program2Specification {
+ from
+ s : FIACRE!Program
+ to
+ t : LOTOS!Specification (
+ name <- 'unnamed',
+ types <- s.elements->select(e |
+ e.oclIsKindOf(FIACRE!TypeDeclaration)
+ ),
+ definition <- definition,
+ commentsBefore <- Sequence {
+ '(* ---------------------------------------------------------------------------- *)',
+ '(* Author: FIACRE2LOTOS.atl *)',
+ '(* Automatically generated code *)',
+ '(* ---------------------------------------------------------------------------- *)'
+ }
+ ),
+ definition : LOTOS!Definition (
+ declarations <- s.elements->select(e |
+ e.oclIsKindOf(FIACRE!ProcessDeclaration) or
+ e.oclIsKindOf(FIACRE!ComponentDeclaration)
+ )
+ )
+}
+
+rule Process {
+ from
+ s : FIACRE!ProcessDeclaration
+ to
+ t : LOTOS!Process (
+ name <- s.name,
+ commentsBefore <- Sequence {'(* TODO: implement Process translation rules *)'}
+ )
+}
+
+rule Component {
+ from
+ s : FIACRE!ComponentDeclaration
+ to
+ t : LOTOS!Process (
+ name <- s.name,
+ commentsBefore <- Sequence {'(* TODO: implement Component translation rules *)'}
+ )
+}
+
+
+abstract rule TypeTranslation {
+ from
+ s : FIACRE!TypeDeclaration
+ to
+ t : LOTOS!TypeDefinition (
+ name <- s.name,
+ sorts <- Sequence {s.name} -- TODO: implementedby
+ ),
+
+ ops : LOTOS!Operations (
+ declarations <- Sequence {eqOp, neqOp},
+ parameterTypes <- Sequence {s.name, s.name},
+ returnType <- 'Bool'
+ ),
+ eqOp : LOTOS!OperationDeclaration (
+ name <- '_eq_'
+ ),
+ neqOp : LOTOS!OperationDeclaration (
+ name <- '_neq_'
+ ),
+
+
+ xAndYDecl : LOTOS!VariableDeclarations (
+ declarations <- Sequence {x, y},
+ type <- s.name
+ ),
+ x : LOTOS!VariableDeclaration (
+ name <- 'x'
+ ),
+ y : LOTOS!VariableDeclaration (
+ name <- 'y'
+ ),
+
+
+ opsEq : LOTOS!OfSort (
+ name <- 'Bool',
+ equations <- Sequence {opsEq1, opsEq2, opsEq3}
+ ),
+ opsGuard : LOTOS!EqualityTestGuardExp (
+ left <- opsGuardX,
+ right <- opsGuardY
+ ),
+ opsGuardX : LOTOS!Variable (
+ declaration <- x
+ ),
+ opsGuardY : LOTOS!Variable (
+ declaration <- y
+ ),
+
+ opsEq1 : LOTOS!GuardedEquation (
+ guard <- opsGuard,
+ equation <- opsEq1SE
+ ),
+ opsEq1SE : LOTOS!SimpleEquation (
+ left <- opsEq1OC,
+ right <- opsEq1T
+ ),
+ opsEq1OC : LOTOS!OperatorCall (
+ operatorName <- 'eq',
+ left <- opsEq1OCX,
+ right <- opsEq1OCY
+ ),
+ opsEq1OCX : LOTOS!Variable (
+ declaration <- x
+ ),
+ opsEq1OCY : LOTOS!Variable (
+ declaration <- y
+ ),
+ opsEq1T : LOTOS!BooleanVal (
+ value <- true
+ ),
+
+ opsEq2 : LOTOS!SimpleEquation (
+ left <- opsEq2OC,
+ right <- opsEq2F
+ ),
+ opsEq2OC : LOTOS!OperatorCall (
+ operatorName <- 'eq',
+ left <- opsEq2OCX,
+ right <- opsEq2OCY
+ ),
+ opsEq2OCX : LOTOS!Variable (
+ declaration <- x
+ ),
+ opsEq2OCY : LOTOS!Variable (
+ declaration <- y
+ ),
+ opsEq2F : LOTOS!BooleanVal (
+ value <- false
+ ),
+
+ opsEq3 : LOTOS!SimpleEquation (
+ left <- opsEq3OC,
+ right <- opsEq3N
+ ),
+ opsEq3OC : LOTOS!OperatorCall (
+ operatorName <- 'neq',
+ left <- opsEq3OCX,
+ right <- opsEq3OCY
+ ),
+ opsEq3OCX : LOTOS!Variable (
+ declaration <- x
+ ),
+ opsEq3OCY : LOTOS!Variable (
+ declaration <- y
+ ),
+ opsEq3N : LOTOS!OperationCall (
+ operationName <- 'not',
+ arguments <- Sequence {opsEq3NOC}
+ ),
+ opsEq3NOC : LOTOS!OperatorCall (
+ operatorName <- 'eq',
+ left <- opsEq3NOCX,
+ right <- opsEq3NOCY
+ ),
+ opsEq3NOCX : LOTOS!Variable (
+ declaration <- x
+ ),
+ opsEq3NOCY : LOTOS!Variable (
+ declaration <- y
+ )
+}
+
+rule Interval extends TypeTranslation {
+ from
+ s : FIACRE!TypeDeclaration (
+ s.type.oclIsKindOf(FIACRE!IntervalType)
+ )
+ to
+ t : LOTOS!TypeDefinition (
+ types <- Sequence {'Boolean', 'IntegerNumber'},
+ operations <- Sequence {cons, checkBounds, toInt, fromInt, error, ops},
+ equations <- Sequence {eqns}
+ ),
+
+-- @begin Operations
+ cons : LOTOS!Operations (
+ declarations <- Sequence {consDecl},
+ parameterTypes <- Sequence {'Int'},
+ returnType <- s.name
+ ),
+ consDecl : LOTOS!OperationDeclaration (
+ name <- s.name,
+ commentsAfter <- Sequence {'(*! constructor *)'}
+ ),
+
+ checkBounds : LOTOS!Operations (
+ declarations <- Sequence {checkBoundsDecl},
+ parameterTypes <- Sequence {'Int'},
+ returnType <- 'Bool'
+ ),
+ checkBoundsDecl : LOTOS!OperationDeclaration (
+ name <- 'In' + s.name
+ ),
+
+ toInt : LOTOS!Operations (
+ declarations <- Sequence {toIntDecl},
+ parameterTypes <- Sequence {s.name},
+ returnType <- 'Int'
+ ),
+ toIntDecl : LOTOS!OperationDeclaration (
+ name <- s.name + 'ToInt'
+ ),
+
+ fromInt : LOTOS!Operations (
+ declarations <- Sequence {fromIntDecl},
+ parameterTypes <- Sequence {'Int'},
+ returnType <- s.name
+ ),
+ fromIntDecl : LOTOS!OperationDeclaration (
+ name <- 'IntTo' + s.name
+ ),
+
+ error : LOTOS!Operations (
+ declarations <- Sequence {errorDecl},
+ parameterTypes <- Sequence {},
+ returnType <- s.name
+ ),
+ errorDecl : LOTOS!OperationDeclaration (
+ name <- 'Error' + s.name,
+ commentsAfter <- Sequence {'(*! implementedby Error' + s.name + ' external *)'}
+ ),
+-- @end Operations
+
+-- @begin Equations
+ eqns : LOTOS!Equations (
+ declarations <- Sequence {xAndYDecl, zDecl},
+ ofSorts <- Sequence {checkBoundsEq, toIntEq, fromIntEq, opsEq}
+ ),
+ zDecl : LOTOS!VariableDeclarations (
+ declarations <- Sequence {z},
+ type <- 'Int'
+ ),
+ z : LOTOS!VariableDeclaration (
+ name <- 'z'
+ ),
+
+ checkBoundsEq : LOTOS!OfSort (
+ name <- 'Bool',
+ equations <- Sequence {cbEq1, cbEq2}
+ ),
+ cbGuard : LOTOS!EqualityTestGuardExp (
+ left <- cbGuardAnd,
+ right <- cbGuardT
+ ),
+ cbGuardAnd : LOTOS!OperatorCall (
+ operatorName <- 'and',
+ left <- cbGuardInf,
+ right <- cbGuardSup
+ ),
+ cbGuardInf : LOTOS!OperatorCall (
+ operatorName <- '>=',
+ left <- cbGuardInfV,
+ right <- cbGuardInfCB
+ ),
+ cbGuardInfV : LOTOS!Variable (
+ declaration <- z
+ ),
+ cbGuardInfCB : LOTOS!CastVal (
+ value <- cbGuardInfB,
+ toType <- 'Int'
+ ),
+ cbGuardInfB : LOTOS!IntegerVal (
+ value <- s.type.lower
+ ),
+ cbGuardSup : LOTOS!OperatorCall (
+ operatorName <- '<=',
+ left <- cbGuardSupV,
+ right <- cbGuardSupCB
+ ),
+ cbGuardSupV : LOTOS!Variable (
+ declaration <- z
+ ),
+ cbGuardSupCB : LOTOS!CastVal (
+ value <- cbGuardSupB,
+ toType <- 'Int'
+ ),
+ cbGuardSupB : LOTOS!IntegerVal (
+ value <- s.type.upper
+ ),
+
+ cbGuardT : LOTOS!BooleanVal (
+ value <- true
+ ),
+
+ cbEq1 : LOTOS!GuardedEquation (
+ guard <- cbGuard,
+ equation <- cbEq1SE
+ ),
+ cbEq1SE : LOTOS!SimpleEquation (
+ left <- cbEq1OpCall,
+ right <- cbEq1T
+ ),
+ cbEq1OpCall : LOTOS!OperationCall (
+ operationName <- 'In' + s.name,
+ arguments <- Sequence {cbEq1OpCallArg}
+ ),
+ cbEq1OpCallArg : LOTOS!Variable (
+ declaration <- z
+ ),
+
+ cbEq1T : LOTOS!BooleanVal (
+ value <- true
+ ),
+
+ cbEq2 : LOTOS!SimpleEquation (
+ left <- cbEq2OpCall,
+ right <- cbEq2F
+ ),
+ cbEq2OpCall : LOTOS!OperationCall (
+ operationName <- 'In' + s.name,
+ arguments <- Sequence {cbEq2OpCallArg}
+ ),
+ cbEq2OpCallArg : LOTOS!Variable (
+ declaration <- z
+ ),
+
+ cbEq2F : LOTOS!BooleanVal (
+ value <- false
+ ),
+
+ toIntEq : LOTOS!OfSort (
+ name <- 'Int',
+ equations <- Sequence {tiEq}
+ ),
+ tiEq : LOTOS!SimpleEquation (
+ left <- tiEqOpCall,
+ right <- tiEqZ
+ ),
+ tiEqOpCall : LOTOS!OperationCall (
+ operationName <- s.name + 'ToInt',
+ arguments <- Sequence {tiEqOpCall2}
+ ),
+ tiEqOpCall2 : LOTOS!OperationCall (
+ operationName <- s.name,
+ arguments <- Sequence {tiEqOpCall2Z}
+ ),
+ tiEqOpCall2Z : LOTOS!Variable (
+ declaration <- z
+ ),
+ tiEqZ : LOTOS!Variable (
+ declaration <- z
+ ),
+
+ fromIntEq : LOTOS!OfSort (
+ name <- s.name,
+ equations <- Sequence {fiEq1, fiEq2}
+ ),
+ fiGuard : LOTOS!EqualityTestGuardExp (
+ left <- fiGuardOC,
+ right <- fiGuardT
+ ),
+ fiGuardOC : LOTOS!OperationCall (
+ operationName <- 'In' + s.name,
+ arguments <- Sequence {fiGuardV}
+ ),
+ fiGuardV : LOTOS!Variable (
+ declaration <- z
+ ),
+
+ fiGuardT : LOTOS!BooleanVal (
+ value <- true
+ ),
+
+ fiEq1 : LOTOS!GuardedEquation (
+ guard <- fiGuard,
+ equation <- fiEq1SE
+ ),
+ fiEq1SE : LOTOS!SimpleEquation (
+ left <- fiEq1OCL,
+ right <- fiEq1OCR
+ ),
+ fiEq1OCL : LOTOS!OperationCall (
+ operationName <- 'IntTo' + s.name,
+ arguments <- Sequence {fiEq1OCLArg}
+ ),
+ fiEq1OCLArg : LOTOS!Variable (
+ declaration <- z
+ ),
+
+ fiEq1OCR : LOTOS!OperationCall (
+ operationName <- s.name,
+ arguments <- Sequence {fiEq1OCRArg}
+ ),
+ fiEq1OCRArg : LOTOS!Variable (
+ declaration <- z
+ ),
+
+ fiEq2 : LOTOS!SimpleEquation (
+ left <- fiEq2OpCall,
+ right <- fiEq2V
+ ),
+ fiEq2OpCall : LOTOS!OperationCall (
+ operationName <- 'IntTo' + s.name,
+ arguments <- Sequence {fiEq2OpCallZ}
+ ),
+ fiEq2OpCallZ : LOTOS!Variable (
+ declaration <- z
+ ),
+ fiEq2V : LOTOS!Variable (
+ declaration <- errorDecl
+ )
+-- @end Equations
+}
+
+rule Enumeration extends TypeTranslation {
+ from
+ s : FIACRE!TypeDeclaration (
+ s.type.oclIsKindOf(FIACRE!EnumerationType)
+ )
+ to
+ t : LOTOS!TypeDefinition (
+ types <- Sequence {'Boolean'},
+ operations <- Sequence {cons, ops},
+ equations <- Sequence {eqns}
+ ),
+
+ cons : LOTOS!Operations (
+ declarations <- s.type.literals,
+ parameterTypes <- Sequence {},
+ returnType <- s.name
+ ),
+
+ eqns : LOTOS!Equations (
+ declarations <- Sequence {xAndYDecl},
+ ofSorts <- Sequence {opsEq}
+ )
+}
+
+rule EnumLiteral {
+ from
+ s : FIACRE!EnumLiteral
+ to
+ t : LOTOS!OperationDeclaration (
+ name <- s.name,
+ commentsAfter <- Sequence {'(*! constructor *)'}
+ )
+}
+
+helper context FIACRE!RecordType def: allFields : Sequence(FIACRE!RecordField) =
+ self.fields->iterate(e; acc : Sequence(FIACRE!RecordField) = Sequence {} |
+ acc->union(e.fields)
+ );
+
+helper context FIACRE!RecordField def: type : FIACRE!Type =
+ self.refImmediateComposite().type;
+
+helper context FIACRE!RecordType def: types : Sequence(String) =
+ self.allFields->collect(e | e.type.toStringH());
+
+rule Record extends TypeTranslation {
+ from
+ s : FIACRE!TypeDeclaration (
+ s.type.oclIsKindOf(FIACRE!RecordType)
+ )
+ to
+ t : LOTOS!TypeDefinition (
+ types <- s.type.types->append('Boolean'),
+ operations <- s.type.allFields->collect(e |
+ thisModule.RecordField2GetOperations(e)
+ )->union(
+ s.type.allFields->collect(e |
+ thisModule.RecordField2SetOperations(e)
+ )
+ )->prepend(cons)->append(ops),
+ equations <- Sequence {eqns}
+ ),
+
+ cons : LOTOS!Operations (
+ declarations <- consDecl,
+ parameterTypes <- s.type.types,
+ returnType <- s.name
+ ),
+ consDecl : LOTOS!OperationDeclaration (
+ name <- s.name,
+ commentsAfter <- Sequence {'(*! constructor *)'}
+ ),
+
+ eqns : LOTOS!Equations (
+ declarations <- s.type.allFields->collect(e |
+ thisModule.RecordField2VariableDeclarations(e)
+ )->append(xAndYDecl),
+ ofSorts <- s.type.allFields->collect(e |
+ thisModule.RecordField2GetEqn(e)
+ )->union(Sequence {setEq, opsEq})
+ ),
+ setEq : LOTOS!OfSort (
+ name <- s.name,
+ equations <- s.type.allFields->collect(e |
+ thisModule.RecordField2SetEqn(e)
+ )
+ )
+}
+
+helper context FIACRE!RecordField def: typeDecl : FIACRE!TypeDeclaration =
+ self.recordType.refImmediateComposite();
+
+helper context FIACRE!RecordField def: recordType : FIACRE!RecordType =
+ self.refImmediateComposite().refImmediateComposite();
+
+helper context FIACRE!RecordField def: typeDeclName : String =
+ self.typeDecl.name;
+
+helper context FIACRE!RecordField def: opSuffix : String =
+ self.typeDeclName + '_' + self.name;
+
+unique lazy rule RecordField2GetOperations {
+ from
+ s : FIACRE!RecordField
+ to
+ t : LOTOS!Operations (
+ declarations <- Sequence {decl},
+ parameterTypes <- Sequence {s.typeDeclName},
+ returnType <- s.type.toString()
+ ),
+ decl : LOTOS!OperationDeclaration (
+ name <- 'Get' + s.opSuffix
+ )
+}
+
+unique lazy rule RecordField2SetOperations {
+ from
+ s : FIACRE!RecordField
+ to
+ t : LOTOS!Operations (
+ declarations <- Sequence {decl},
+ parameterTypes <- Sequence {s.typeDeclName, s.type.toString()},
+ returnType <- s.typeDeclName
+ ),
+ decl : LOTOS!OperationDeclaration (
+ name <- 'Set' + s.typeDeclName + '_' + s.name
+ )
+}
+
+helper context FIACRE!RecordField def: index : String =
+ self.recordType.allFields->indexOf(self).toString();
+
+unique lazy rule RecordField2VariableDeclarations {
+ from
+ s : FIACRE!RecordField
+ to
+ t : LOTOS!VariableDeclarations (
+ declarations <- Sequence {
+ thisModule.RecordField2X(s),
+ thisModule.RecordField2Y(s)
+ },
+ type <- s.type.toString()
+ )
+}
+
+unique lazy rule RecordField2X {
+ from
+ s : FIACRE!RecordField
+ to
+ x : LOTOS!VariableDeclaration (
+ name <- 'x' + s.index
+ )
+}
+
+unique lazy rule RecordField2Y {
+ from
+ s : FIACRE!RecordField
+ to
+ x : LOTOS!VariableDeclaration (
+ name <- 'y' + s.index
+ )
+}
+
+unique lazy rule RecordField2GetEqn {
+ from
+ s : FIACRE!RecordField
+ to
+ t : LOTOS!OfSort (
+ name <- s.type.toString(),
+ equations <- eq
+ ),
+ eq : LOTOS!SimpleEquation (
+ left <- oc,
+ right <- thisModule.RecordField2XVariable(s)
+ ),
+ oc : LOTOS!OperationCall (
+ operationName <- 'Get' + s.opSuffix,
+ arguments <- Sequence {cc}
+ ),
+ cc : LOTOS!OperationCall (
+ operationName <- s.typeDeclName,
+ arguments <- s.recordType.allFields->collect(e |
+ thisModule.RecordField2XVariable(e)
+ )
+ )
+}
+
+unique lazy rule RecordField2SetEqn {
+ from
+ s : FIACRE!RecordField
+ to
+ t : LOTOS!SimpleEquation (
+ left <- oc,
+ right <- right
+ ),
+ oc : LOTOS!OperationCall (
+ operationName <- 'Set' + s.opSuffix,
+ arguments <- Sequence {cc, thisModule.RecordField2YVariable(s)}
+ ),
+ cc : LOTOS!OperationCall (
+ operationName <- s.typeDeclName,
+ arguments <- s.recordType.allFields->collect(e |
+ thisModule.RecordField2XVariable(e)
+ )
+ ),
+ right : LOTOS!OperationCall (
+ operationName <- s.typeDeclName,
+ arguments <- s.recordType.allFields->collect(e |
+ if e = s then
+ thisModule.RecordField2YVariable(e)
+ else
+ thisModule.RecordField2XVariable(e)
+ endif
+ )
+ )
+}
+
+-- not unique because called several times
+lazy rule RecordField2XVariable {
+ from
+ s : FIACRE!RecordField
+ to
+ t : LOTOS!Variable (
+ declaration <- thisModule.RecordField2X(s)
+ )
+}
+
+-- not unique because called several times
+lazy rule RecordField2YVariable {
+ from
+ s : FIACRE!RecordField
+ to
+ t : LOTOS!Variable (
+ declaration <- thisModule.RecordField2Y(s)
+ )
+}
+
+helper context FIACRE!IntegerType def: toString() : String =
+ 'Int';
+
+helper context FIACRE!BooleanType def: toString() : String =
+ 'Bool';
+
+helper context FIACRE!TypeRef def: toString() : String =
+ self.declaration.name;
+
+helper context FIACRE!IntegerType def: toStringH() : String =
+ 'IntegerNumber';
+
+helper context FIACRE!BooleanType def: toStringH() : String =
+ 'Boolean';
+
+helper context FIACRE!TypeRef def: toStringH() : String =
+ self.declaration.name;
+
+helper context Integer def: sequenceTo(other : Integer) : Sequence(Integer) =
+ if self > other then
+ Sequence {}
+ else
+ Sequence {self}->union((self + 1).sequenceTo(other))
+ endif;
+
+rule Array extends TypeTranslation {
+ from
+ s : FIACRE!TypeDeclaration (
+ s.type.oclIsKindOf(FIACRE!ArrayType)
+ )
+ using {
+ indices : Sequence(Integer) = 1 .sequenceTo(s.type.size);
+ xs : Sequence(LOTOS!VariableDeclaration) = OclUndefined;
+ }
+ to
+ t : LOTOS!TypeDefinition (
+ types <- Sequence {s.type.elementType.toStringH(), 'Boolean', 'Natural'},
+ operations <- Sequence {cons, get, set, error1, error2, ops},
+ equations <- Sequence {eqns}
+ ),
+
+ cons : LOTOS!Operations (
+ declarations <- consDecl,
+ parameterTypes <- indices->collect(e |
+ s.type.elementType.toString()
+ ),
+ returnType <- s.name
+ ),
+ consDecl : LOTOS!OperationDeclaration (
+ name <- s.name,
+ commentsAfter <- Sequence {'(*! constructor *)'}
+ ),
+
+ get : LOTOS!Operations (
+ declarations <- Sequence {getDecl},
+ parameterTypes <- Sequence {s.name, 'Nat'},
+ returnType <- s.type.elementType.toString()
+ ),
+ getDecl : LOTOS!OperationDeclaration (
+ name <- 'Get' + s.name
+ ),
+
+ set : LOTOS!Operations (
+ declarations <- Sequence {setDecl},
+ parameterTypes <- Sequence {s.name, 'Nat', s.type.elementType.toString()},
+ returnType <- s.name
+ ),
+ setDecl : LOTOS!OperationDeclaration (
+ name <- 'Set' + s.name
+ ),
+
+ error1 : LOTOS!Operations (
+ declarations <- Sequence {error1Decl},
+ parameterTypes <- Sequence {},
+ returnType <- s.type.elementType.toString()
+ ),
+ error1Decl : LOTOS!OperationDeclaration (
+ name <- 'Error' + s.name + '_1',
+ commentsAfter <- Sequence {'(*! implementedby Error' + s.name + '_1 external *)'}
+ ),
+
+ error2 : LOTOS!Operations (
+ declarations <- Sequence {error2Decl},
+ parameterTypes <- Sequence {},
+ returnType <- s.name
+ ),
+ error2Decl : LOTOS!OperationDeclaration (
+ name <- 'Error' + s.name + '_2',
+ commentsAfter <- Sequence {'(*! implementedby Error' + s.name + '_2 external *)'}
+ ),
+
+
+ eqns : LOTOS!Equations (
+ declarations <- Sequence {xsAndZDecl, xAndYDecl, pDecl},
+ ofSorts <- Sequence {getEq, setEq, opsEq}
+ ),
+ xsAndZDecl : LOTOS!VariableDeclarations (
+ type <- s.type.elementType.toString()
+ ),
+ z : LOTOS!VariableDeclaration (
+ name <- 'z'
+ ),
+ pDecl : LOTOS!VariableDeclarations (
+ declarations <- Sequence {p},
+ type <- 'Nat'
+ ),
+ p : LOTOS!VariableDeclaration (
+ name <- 'p'
+ ),
+
+ getEq : LOTOS!OfSort (
+ name <- s.type.elementType.toString()
+ ),
+ setEq : LOTOS!OfSort (
+ name <- s.name
+ )
+ do {
+ xs <- indices->collect(e |
+ LOTOS!VariableDeclaration
+ .newInstance()
+ .refSetValue('name', 'x' + e.toString())
+ );
+ xsAndZDecl.declarations <- xs->append(z);
+
+ -- Get equations
+ for(i in indices) {
+ getEq.equations <- thisModule.CreateIndexedGetEquation(p, i, xs, s.name);
+ }
+ getEq.equations <- thisModule.CreateErrorGetEquation(p, error1Decl, xs, s.name);
+
+ -- Set equations
+ for(i in indices) {
+ setEq.equations <- thisModule.CreateIndexedSetEquation(z, p, i, xs, s.name);
+ }
+ setEq.equations <- thisModule.CreateErrorSetEquation(z, p, error2Decl, xs, s.name);
+ }
+}
+
+rule CreateIndexedGetEquation(p : LOTOS!VariableDeclaration, index : Integer, xs : Sequence(LOTOS!VariableDeclaration), typeName : String) {
+ to
+ t : LOTOS!GuardedEquation (
+ guard <- guard
+ ),
+ guard : LOTOS!EqualityTestGuardExp (
+ left <- pv,
+ right <- idx
+ ),
+ pv : LOTOS!Variable (
+ declaration <- p
+ ),
+ idx : LOTOS!IntegerVal (
+ value <- index
+ )
+ do {
+ t.equation <- thisModule.CreateGetEquation(p, xs->at(index), xs, typeName);
+ t;
+ }
+}
+
+rule CreateErrorGetEquation(p : LOTOS!VariableDeclaration, error : LOTOS!Declaration, xs : Sequence(LOTOS!VariableDeclaration), typeName : String) {
+ do {
+ thisModule.CreateGetEquation(p, error, xs, typeName);
+ }
+}
+
+rule CreateGetEquation(p : LOTOS!VariableDeclaration, resultDecl : LOTOS!VariableDeclaration, xs : Sequence(LOTOS!VariableDeclaration), typeName : String) {
+ to
+ t : LOTOS!SimpleEquation (
+ left <- oc,
+ right <- xi
+ ),
+ oc : LOTOS!OperationCall (
+ operationName <- 'Get' + typeName,
+ arguments <- Sequence {consCall, idx}
+ ),
+ consCall : LOTOS!OperationCall (
+ operationName <- typeName
+ ),
+ xi : LOTOS!Variable (
+ declaration <- resultDecl
+ ),
+ idx : LOTOS!Variable (
+ declaration <- p
+ )
+ do {
+ consCall.arguments <- xs->collect(e |
+ LOTOS!Variable
+ .newInstance()
+ .refSetValue('declaration', e)
+ );
+ t;
+ }
+}
+
+rule CreateIndexedSetEquation(z : LOTOS!VariableDeclaration, p : LOTOS!VariableDeclaration, index : Integer, xs : Sequence(LOTOS!VariableDeclaration), typeName : String) {
+ to
+ t : LOTOS!GuardedEquation (
+ guard <- guard
+ ),
+ guard : LOTOS!EqualityTestGuardExp (
+ left <- pv,
+ right <- idx
+ ),
+ pv : LOTOS!Variable (
+ declaration <- p
+ ),
+ idx : LOTOS!IntegerVal (
+ value <- index
+ ),
+ right : LOTOS!OperationCall (
+ operationName <- typeName
+ ),
+ zv : LOTOS!Variable (
+ declaration <- z
+ )
+ do {
+ right.arguments <- xs->collect(e |
+ if e.name = 'x' + index.toString() then
+ zv
+ else
+ LOTOS!Variable
+ .newInstance()
+ .refSetValue('declaration', e)
+ endif
+ );
+ t.equation <- thisModule.CreateSetEquation(p, z, right, xs, typeName);
+ t;
+ }
+}
+
+rule CreateErrorSetEquation(z : LOTOS!VariableDeclaration, p : LOTOS!VariableDeclaration, error : LOTOS!Declaration, xs : Sequence(LOTOS!VariableDeclaration), typeName : String) {
+ to
+ errorVal : LOTOS!Variable (
+ declaration <- error
+ )
+ do {
+ thisModule.CreateSetEquation(p, z, errorVal, xs, typeName);
+ }
+}
+
+rule CreateSetEquation(p : LOTOS!VariableDeclaration, z : LOTOS!VariableDeclaration, right : LOTOS!Value, xs : Sequence(LOTOS!VariableDeclaration), typeName : String) {
+ to
+ t : LOTOS!SimpleEquation (
+ left <- oc,
+ right <- right
+ ),
+ oc : LOTOS!OperationCall (
+ operationName <- 'Set' + typeName,
+ arguments <- Sequence {consCall, idx, zv}
+ ),
+ consCall : LOTOS!OperationCall (
+ operationName <- typeName
+ ),
+ zv : LOTOS!Variable (
+ declaration <- z
+ ),
+ idx : LOTOS!Variable (
+ declaration <- p
+ )
+ do {
+ consCall.arguments <- xs->collect(e |
+ LOTOS!Variable
+ .newInstance()
+ .refSetValue('declaration', e)
+ );
+ t;
+ }
+}

Back to the top