diff --git a/asmetal2java_codegen/examples/ATM3.asm b/asmetal2java_codegen/examples/ATM3.asm index 6a43f49..ddda5f3 100644 --- a/asmetal2java_codegen/examples/ATM3.asm +++ b/asmetal2java_codegen/examples/ATM3.asm @@ -230,4 +230,4 @@ default init s0: case card2 : 1652 case card3 : 548 endswitch - function accessible($c in NumCard) = true + function accessible($c in NumCard) = true \ No newline at end of file diff --git a/asmetal2java_codegen/input/CTLLibrary.asm b/asmetal2java_codegen/input/CTLLibrary.asm new file mode 100644 index 0000000..53a7434 --- /dev/null +++ b/asmetal2java_codegen/input/CTLLibrary.asm @@ -0,0 +1,65 @@ +module CTLLibrary + +import StandardLibrary + +export * + +signature: + /*-----------CTL formulas------------*/ + static eg: Boolean -> Boolean //exists globally + static ex: Boolean -> Boolean //exists next state + static ef: Boolean -> Boolean //exists finally + static ag: Boolean -> Boolean //forall globally + static ax: Boolean -> Boolean //forall next state + static af: Boolean -> Boolean //forall finally + static eu: Prod(Boolean, Boolean) -> Boolean //exists until + static au: Prod(Boolean, Boolean) -> Boolean //forall until + + /*-----------Patterns------------*/ + static ew: Prod(Boolean, Boolean) -> Boolean //exists weak until -- E[p U q] | EGp. + static aw: Prod(Boolean, Boolean) -> Boolean //forall weak until -- !E[!q U !(p | q)]. + + + //http://patterns.projects.cis.ksu.edu/documentation/patterns/ctl.shtml + //Absence (P is false) + //Globally - AG(!P) + static absenceG: Boolean -> Boolean + //(*) Before R - A[(!P | AG(!R)) W R] + static absenceBefore: Prod(Boolean, Boolean) -> Boolean // absenceBefore(P, R) + //After Q - AG(Q -> AG(!P)) + static absenceAfter: Prod(Boolean, Boolean) -> Boolean // absenceAfter(P, Q) + //(*) Between Q and R - AG(Q & !R -> A[(!P | AG(!R)) W R]) + static absenceBetween: Prod(Boolean, Boolean, Boolean) -> Boolean // absenceBetween(P, Q, R) + //(*) After Q until R - AG(Q & !R -> A[!P W R]) + static absenceAfterUntil: Prod(Boolean, Boolean, Boolean) -> Boolean // absenceAfterUntil(P, Q, R) + + //Precedence (S precedes P) + //(*) Globally + //A[!P W S] + static ap: Prod(Boolean, Boolean) -> Boolean // ap(P, S) + //(*) Before R + //A[(!P | AG(!R)) W (S | R)] + static pb: Prod(Boolean, Boolean, Boolean) -> Boolean // pb(P, S, R) + //(*) After Q + //A[!Q W (Q & A[!P W S])] + //(*) Between Q and R + //AG(Q & !R -> A[(!P | AG(!R)) W (S | R)]) + //(*) After Q until R + //AG(Q & !R -> A[!P W (S | R)]) + + //Response (S responds to P) + //Globally + //AG(P -> AF(S)) + //(*) Before R + //A[((P -> A[!R U (S & !R)]) | AG(!R)) W R] + //(*) After Q + //A[!Q W (Q & AG(P -> AF(S))] + //(*) Between Q and R + //AG(Q & !R -> A[((P -> A[!R U (S & !R)]) | AG(!R)) W R]) + //(*) After Q until R + //AG(Q & !R -> A[(P -> A[!R U (S & !R)]) W R]) + + /*-----------My CTL formulas------------*/ + static exN: Prod(Boolean, Natural) -> Boolean //exists after N states + static axN: Prod(Boolean, Natural) -> Boolean //forall paths, after N states +definitions: diff --git a/asmetal2java_codegen/input/LTLLibrary.asm b/asmetal2java_codegen/input/LTLLibrary.asm new file mode 100644 index 0000000..e114890 --- /dev/null +++ b/asmetal2java_codegen/input/LTLLibrary.asm @@ -0,0 +1,21 @@ +module LTLLibrary + +export * + +signature: + /*-----------LTL formulas------------*/ + //Future + static x: Boolean -> Boolean //next state + static g: Boolean -> Boolean //globally + static f: Boolean -> Boolean //finally + static u: Prod(Boolean, Boolean) -> Boolean //until + static v: Prod(Boolean, Boolean) -> Boolean //releases + //Past + static y: Boolean -> Boolean //previous state + static z: Boolean -> Boolean //not previous state not + static h: Boolean -> Boolean //historically + static o: Boolean -> Boolean //once + static s: Prod(Boolean, Boolean) -> Boolean //since + static t: Prod(Boolean, Boolean) -> Boolean //triggered + +definitions: \ No newline at end of file diff --git a/asmetal2java_codegen/src/org/asmeta/asm2java/RuleToJava.xtend b/asmetal2java_codegen/src/org/asmeta/asm2java/RuleToJava.xtend index 5ac06e1..dca1ea9 100644 --- a/asmetal2java_codegen/src/org/asmeta/asm2java/RuleToJava.xtend +++ b/asmetal2java_codegen/src/org/asmeta/asm2java/RuleToJava.xtend @@ -166,10 +166,15 @@ class RuleToJava extends RuleVisitor { append('''«new TermToJava(res,true).visit(object.location)» = «new TermToJava(res,false).visit(object.updatingTerm)»; ''') - else if (object.updatingTerm.domain instanceof ConcreteDomain) + /*else if (object.updatingTerm.domain instanceof ConcreteDomain) result. append('''«new TermToJava(res,true).visit(object.location)»«new TermToJava(res,false).visit(object.updatingTerm)».value); «new TermToJavaInUpdateRule(res,false).visit(object.location)» + ''')*/ + else if (object.updatingTerm.domain instanceof ConcreteDomain) + result. + append('''«new TermToJava(res,true).visit(object.location)»«new TermToJava(res,false).visit(object.updatingTerm)»); + «new TermToJavaInUpdateRule(res,false).visit(object.location)» ''') else { var String varName = object.hashCode.toString diff --git a/asmetal2java_codegen/src/org/asmeta/asm2java/TermToJava.xtend b/asmetal2java_codegen/src/org/asmeta/asm2java/TermToJava.xtend index 1abd730..e575a9e 100644 --- a/asmetal2java_codegen/src/org/asmeta/asm2java/TermToJava.xtend +++ b/asmetal2java_codegen/src/org/asmeta/asm2java/TermToJava.xtend @@ -233,6 +233,11 @@ class TermToJava extends ReflectiveVisitor { ''' «"Arrays.stream("» «new ToString(res).visit((object.getRanges.get(i).domain as PowersetDomain).baseDomain)».values()).anyMatch(c -> «valore»c)) ''') + else if ((object.getRanges.get(i).domain as PowersetDomain).baseDomain instanceof ConcreteDomain) // devo togliere il .value aggiunto in TermToJavaStandardLibrary.xtend (riga 102) + sb.append( + ''' + «""» «new ToString(res).visit((object.getRanges.get(i).domain as PowersetDomain).baseDomain)».elems.stream().anyMatch(c -> c.equals(«app.substring(13,app.length-7)»)) + ''') else sb.append( ''' @@ -371,9 +376,13 @@ class TermToJava extends ReflectiveVisitor { var name = new Util().parseFunction(term.function.name) // Controllo se l'operatore » del tipo: &,|,<=,>=,<,>... - if (ExpressionToJava.hasEvaluateVisitor(name)) { + /*if (ExpressionToJava.hasEvaluateVisitor(name)) { + // if the funcion is an expression + return new ExpressionToJava(res).evaluateFunction(name, term.arguments.terms);*/ + if (ExpressionToJava.hasEvaluateVisitor(name)) { // utilizzo questo if per correggere il problema di avere due .value.value // if the funcion is an expression - return new ExpressionToJava(res).evaluateFunction(name, term.arguments.terms); + var expression = new ExpressionToJava(res).evaluateFunction(name, term.arguments.terms); + return expression.replaceAll(".value.value",".value") } // In questo caso l'operatore rilevato » := else { diff --git a/asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator.xtend b/asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator.xtend new file mode 100644 index 0000000..7d12b6c --- /dev/null +++ b/asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator.xtend @@ -0,0 +1,907 @@ +package org.asmeta.asm2java.main + +import asmeta.structure.Asm +import java.util.List +import asmeta.transitionrules.basictransitionrules.Rule +import org.junit.Assert +import java.util.ArrayList +import org.asmeta.asm2java.SeqRuleCollector +import asmeta.definitions.domains.AbstractTd +import asmeta.definitions.ControlledFunction +import asmeta.definitions.domains.ConcreteDomain +import asmeta.definitions.domains.MapDomain +import asmeta.definitions.domains.SequenceDomain +import asmeta.definitions.domains.EnumTd +import asmeta.definitions.MonitoredFunction +import org.asmeta.asm2java.ToString +import asmeta.definitions.StaticFunction + +class JavaASMGenerator extends AsmToJavaGenerator { + + def compileAndWrite(Asm asm, String writerPath, TranslatorOptions userOptions) { + Assert.assertTrue(writerPath.endsWith(".java")); + compileAndWrite(asm, writerPath, "JAVA", userOptions) + } + + // all the rules that must translate in two versions seq and not seq + // if null, translate all + List seqCalledRules; + + String supp + + String [] finalStateConditions; + + def setFinalStateConditions(String [] finalStateConditions){ + this.finalStateConditions = finalStateConditions; + } + + override compileAsm(Asm asm) { + // collect alla the seq rules if required + if (options.optimizeSeqMacroRule) { + seqCalledRules = new ArrayList + for (r : asm.bodySection.ruleDeclaration) + seqCalledRules.addAll(new SeqRuleCollector(false).visit(r)) + } + + val asmName = asm.name + + var sb = new StringBuffer; + + sb.append( + ''' + + // «asmName»_ASM.java automatically generated from ASM2CODE + + import java.util.Scanner; + + /** + * This class allows you to simulate the behavior of an Abstract State Machine (ASM) + * without asking the user for input values ​​of the monitored functions. + * + *

+ * It has been optimized to be used with evosuite in order to automatically generate test scenarios. + *

+ */ + class «asmName»_ASM { + + private final «asmName» esecuzione; + private int stato; + + /** + * Constructor of the {@code «asmName»_ASM} class. Creates a private instance of the asm + * {@link «asmName»} and sets the initial state of the state machine to 1. + */ + public «asmName»_ASM(){ + this.esecuzione = new «asmName»(); + this.stato = 0; + } + + /** The step function is the only public method of the ASM, + * it receives as parameters the values ​​of the monitored functions to be updated + * and allows to perform a step of the asm by incrementing the state. + */ + public void step('''); + + setMonitoredArgs(asm,sb); + + sb.append('''){ + System.out.println(""); + + printControlled(); + setMonitored( '''); + + for (fd : asm.headerSection.signature.function) { + if (fd instanceof MonitoredFunction) { + if (fd.domain === null) { // [] -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + sb.append(System.lineSeparator) + sb.append("\t\t\t\t\t").append('''«fd.name»,''') + } + else { + var dd = fd.domain + if(dd instanceof EnumTd){ // Enum -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + for (var int i = 0; i < dd.element.size; i++) { + var symbol = new ToString(asm).visit(dd.element.get(i)) + sb.append(System.lineSeparator()) + sb.append("\t\t\t\t\t").append('''«fd.name»_«symbol»,''') + } + } + if(fd.domain instanceof AbstractTd){ // Abstract -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + for (sf : asm.headerSection.signature.function) { + if(sf instanceof StaticFunction){ + if(sf.codomain.equals(fd.domain) && sf.domain===null){ + var symbol = sf.name + sb.append(System.lineSeparator()) + sb.append("\t\t\t\t\t").append('''«fd.name»_«symbol»,''') + } + } + } + } + } + } + } + sb.setLength(sb.length() - 1); + sb.append('''); + this.esecuzione.updateASM(); + + System.out.println(""); + + System.out.println("\n"); + printControlled(); + + /* monitored */ + coverMonitored(); + /* controlled */ + coverControlled();'''); + + sb.append(System.lineSeparator) + if(finalStateConditions !== null && !finalStateConditions.isEmpty){ + sb.append("\t\t\t\t" ).append('''/* final state condition */''') + sb.append(System.lineSeparator) + sb.append("\t\t\t\t" ).append('''if(isFinalState()){ + System.out.println("\n"); + } + else''') + sb.append(System.lineSeparator) + } + sb.append("\t\t\t\t\t\t" ).append('''stato++; + }''') + + setIsFinalState(asm, sb) + sb.append(System.lineSeparator) + + sb.append("\t" ).append('''// Monitored getters'''); + + monitoredGetter(asm, sb); + + sb.append(System.lineSeparator) + sb.append("\t\t").append('''// Controlled getters'''); + sb.append(System.lineSeparator) + + controlledGetter(asm,sb); + + sb.append(System.lineSeparator) + sb.append("\t").append('''// Cover functions'''); + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + sb.append("\t").append(''' + private void coverMonitored(){'''); + + coverFunctions(asm,sb,true) + sb.append(System.lineSeparator) + + sb.append("\t").append(''' + } + + private void coverControlled(){'''); + + coverFunctions(asm,sb,false) + + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + + coverBranches(asm,sb); + + sb.append(''' + + // ASM Methods + + private void printControlled() { + + «printControlled(asm)» + + } + + private void setMonitored( '''); + + setMonitoredArgs(asm,sb); + + sb.append(''') { + + «setMonitored(asm)» + } + }'''); + + return sb.toString(); + + } + + def coverFunctions(Asm asm, StringBuffer sb, boolean monitored) { + + for (fd : asm.headerSection.signature.function) { + if (fd instanceof MonitoredFunction && monitored==true) { + sb.append(System.lineSeparator) + sb.append("\t\t").append('''cover_«fd.name»();''') + } + } + + for (fd : asm.headerSection.signature.function) { + if (fd instanceof ControlledFunction && monitored==false) { + sb.append(System.lineSeparator) + sb.append("\t\t").append('''cover_«fd.name»();''') + } + } + } + + def coverBranches(Asm asm, StringBuffer sb) { + for (fd : asm.headerSection.signature.function){ + if(fd instanceof MonitoredFunction || fd instanceof ControlledFunction){ + if(fd.domain === null){ // [] -> ... + sb.append("\t").append('''private void cover_«fd.name»(){'''); + if(fd.codomain instanceof EnumTd){ // [] -> Enum + sb.append(System.lineSeparator) + sb.append("\t\t").append('''switch(this.get_«fd.name»()){'''); + for(dd : asm.headerSection.signature.domain){ + if(dd.equals(fd.codomain)){ + if(dd instanceof EnumTd){ + for (var int i = 0; i < dd.element.size; i++) { + var symbol = new ToString(asm).visit(dd.element.get(i)) + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''case «symbol» : + System.out.println("Branch «fd.codomain.name» «symbol» covered"); + // Branch «fd.codomain.name» «symbol» covered + break;'''); + } + } + } + } + sb.append(System.lineSeparator) + sb.append("\t\t\t")sb.append('''}'''); + } // [] -> (Integer|String|Boolean|ConcreteDomain|Abstract) + else{ + sb.append(System.lineSeparator) + sb.append("\t\t").append('''this.get_«fd.name»();'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''//1 Branch covered'''); + } + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + else{ // (Abstract|Enum) -> ... + for(dd : asm.headerSection.signature.domain){ + if(dd.equals(fd.domain)){ + sb.append("\t").append('''private void cover_«fd.name»(){'''); + if(dd instanceof EnumTd){ // Enum -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + for (var int i = 0; i < dd.element.size; i++) { + var sd = fd.codomain + var symbol = new ToString(asm).visit(dd.element.get(i)) + sb.append(System.lineSeparator) + sb.append("\t\t").append('''this.get_«fd.name»_«symbol»();'''); + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''// «dd.element.size» Branch covered'''); + } + else if (dd instanceof AbstractTd) { // Abstract -> .. + var i = 0 + for (sf : asm.headerSection.signature.function) { + if(sf instanceof StaticFunction){ + if(sf.codomain.equals(dd) && sf.domain===null){ + var sd = fd.codomain + if(sd instanceof EnumTd){ // Abstract -> Enum + sb.append(System.lineSeparator) + sb.append("\t\t").append('''switch(this.esecuzione.«fd.name».get( + this.esecuzione.«fd.domain.name»_Class.get( + this.esecuzione.«fd.domain.name»_elemsList.indexOf("«sf.name»")))){'''); + for (var int j = 0; j < sd.element.size; j++) { + var symbol = new ToString(asm).visit(sd.element.get(j)) + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''case «symbol» : + System.out.println("Branch «sf.name» «symbol» covered"); + // Branch «sf.name» «symbol» covered + break;'''); + i+=1 + } + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } + else{ // Abstract -> (Integer|String|Boolean|ConcreteDomain|Abstract) + var symbol = sf.name + sb.append(System.lineSeparator) + sb.append("\t\t").append('''this.get_«fd.name»_«symbol»();'''); + i+=1 + } + } + } + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''//«i» Branch covered'''); + } + else { + sb.append(System.lineSeparator) + sb.append("\t\t").append('''this.get_«fd.name»();'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''//1 Branch covered'''); + } + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + } + } + } + } + } + + def monitoredGetter(Asm asm, StringBuffer sb) { + var asmName = asm.name; + for (fd : asm.headerSection.signature.function) { + if (fd instanceof MonitoredFunction) { + if (fd.domain === null) { + if (fd.codomain.name.equals("Boolean") && !(fd.codomain instanceof ConcreteDomain)) { + sb.append(''' + + private boolean get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + if (fd.codomain.name.equals("Integer") && !(fd.codomain instanceof ConcreteDomain)) { + sb.append(''' + + private int get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + if (fd.codomain.name.equals("String") && !(fd.codomain instanceof ConcreteDomain)) { + sb.append(''' + + private String get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + if (fd.codomain instanceof ConcreteDomain) { + sb.append(''' + + private int get_«fd.name»(){ + return this.esecuzione.«fd.name».get().value; + } + '''); + } + if (fd.codomain instanceof EnumTd || + fd.codomain instanceof AbstractTd) { + sb.append(''' + + private «asmName».«fd.codomain.name» get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + } + else{ // getter per le funzioni con Dominio -> Codominio + + for(dd : asm.headerSection.signature.domain){ + if(dd.equals(fd.domain)){ + if(dd instanceof EnumTd){ + for (var int i = 0; i < dd.element.size; i++) { + var symbol = new ToString(asm).visit(dd.element.get(i)) + sb.append(System.lineSeparator) + if(fd.codomain instanceof ConcreteDomain){ // considero subsetOf Integer + sb.append("\t").append('''private int get_«fd.name»_«symbol»(){'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»)).value;'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } else{ + if (fd.codomain.name.equals("Integer")){ + sb.append("\t").append('''private int get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("Boolean")){ + sb.append("\t").append('''private boolean get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("String")){ + sb.append("\t").append('''private String get_«fd.name»_«symbol»(){'''); + } + else{ + sb.append("\t").append('''private «asmName».«fd.codomain.name» get_«fd.name»_«symbol»(){'''); + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»));'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } + sb.append(System.lineSeparator) + } + } + else if(dd instanceof AbstractTd){ + for (sf : asm.headerSection.signature.function) { // controllo le funzioni statiche e prendo quelle che aggiungono al dominio astratto + if(sf instanceof StaticFunction){ + if(sf.codomain.equals(dd) && sf.domain===null){ + var symbol = sf.name + sb.append(System.lineSeparator) + if(fd.codomain instanceof ConcreteDomain){ + sb.append("\t").append('''private int get_«fd.name»_«symbol»(){'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»"))).value;'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } else{ + if (fd.codomain.name.equals("Integer")){ + sb.append("\t").append('''private int get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("Boolean")){ + sb.append("\t").append('''private boolean get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("String")){ + sb.append("\t").append('''private Srting get_«fd.name»_«symbol»(){'''); + } + else{ + sb.append("\t").append('''private «asm.name».«fd.codomain.name» get_«fd.name»_«symbol»(){'''); + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")));'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } + sb.append(System.lineSeparator) + } + } + } + } + } + } + } + } + } + } + + def controlledGetter(Asm asm, StringBuffer sb) { + var asmName = asm.name; + for (fd : asm.headerSection.signature.function) { + if (fd instanceof ControlledFunction) { + if (fd.domain === null) { + if (fd.codomain.name.equals("Boolean") && !(fd.codomain instanceof ConcreteDomain)) { + sb.append(''' + + public boolean get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + if (fd.codomain.name.equals("Integer") && !(fd.codomain instanceof ConcreteDomain)) { + sb.append(''' + + public int get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + if (fd.codomain.name.equals("String") && !(fd.codomain instanceof ConcreteDomain)) { + sb.append(''' + + public String get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + if (fd.codomain instanceof ConcreteDomain) { + sb.append(''' + + public int get_«fd.name»(){ + return this.esecuzione.«fd.name».get().value; + } + '''); + } + if (fd.codomain instanceof EnumTd || + fd.codomain instanceof AbstractTd) { + sb.append(''' + + public «asmName».«fd.codomain.name» get_«fd.name»(){ + return this.esecuzione.«fd.name».get(); + } + '''); + } + } + else{ // getter per le funzioni con Dominio -> Codominio + + for(dd : asm.headerSection.signature.domain){ + if(dd.equals(fd.domain)){ + if(dd instanceof EnumTd){ + for (var int i = 0; i < dd.element.size; i++) { + var symbol = new ToString(asm).visit(dd.element.get(i)) + sb.append(System.lineSeparator) + if(fd.codomain instanceof ConcreteDomain){ // considero subsetOf Integer + sb.append("\t").append('''public int get_«fd.name»_«symbol»(){'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»)).value;'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } else{ + if (fd.codomain.name.equals("Integer")){ + sb.append("\t").append('''public int get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("Boolean")){ + sb.append("\t").append('''public boolean get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("String")){ + sb.append("\t").append('''public String get_«fd.name»_«symbol»(){'''); + } + else{ + sb.append("\t").append('''public «asmName».«fd.codomain.name» get_«fd.name»_«symbol»(){'''); + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»));'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } + sb.append(System.lineSeparator) + } + }// TODO: Ritornare pubblicamente dei valori astratti crea problemi perchè non si possono confrontare + else if(dd instanceof AbstractTd){ + for (sf : asm.headerSection.signature.function) { + if(sf instanceof StaticFunction){ + if(sf.codomain.equals(dd) && sf.domain===null){ + var symbol = sf.name + sb.append(System.lineSeparator) + if(fd.codomain instanceof ConcreteDomain){ + sb.append("\t").append('''public int get_«fd.name»_«symbol»(){'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")).value);'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } else{ + if (fd.codomain.name.equals("Integer")){ + sb.append("\t").append('''public int get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("Boolean")){ + sb.append("\t").append('''public boolean get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("String")){ + sb.append("\t").append('''public Srting get_«fd.name»_«symbol»(){'''); + } + else{ + sb.append("\t").append('''public «asm.name».«fd.codomain.name» get_«fd.name»_«symbol»(){'''); + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")));'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } + sb.append(System.lineSeparator) + } + } + } + } + } + } + } + } + } + } + + def printControlled(Asm asm) { + + var sb = new StringBuffer; + + for (dd : asm.headerSection.signature.domain) { + if (dd instanceof AbstractTd) { + + sb.append(''' + System.out.print("«dd.name»"+ " = {"); + for(int i=0 ; i< esecuzione.«dd.name»_elemsList.size(); i++) + if(i!= esecuzione.«dd.name»_elemsList.size()-1) + System.out.print(esecuzione.«dd.name»_elemsList.get(i) +", "); + else + System.out.print(esecuzione.«dd.name»_elemsList.get(i)); + System.out.println("}"); + ''') + + } + } + + for (fd : asm.headerSection.signature.function) { + + // Studio dei casi controlled con il dominio nullo, quindi funzioni che ricadono nella struttura zeroC + if (fd instanceof ControlledFunction) { + if (fd.domain === null) { + if (fd.codomain instanceof ConcreteDomain) + sb.append(''' + System.out.println("«fd.name» = " + esecuzione.«fd.name».get().value); + ''') + if (fd.codomain.name.equals("Integer") || fd.codomain.name.equals("Boolean") || + fd.codomain.name.equals("String")) + sb.append(''' + System.out.println("«fd.name» = " + esecuzione.«fd.name».get()); + ''') + if (fd.codomain instanceof MapDomain) + sb.append(''' + System.out.println("«fd.name» = " + esecuzione.«fd.name».get()); + ''') + if (fd.codomain instanceof SequenceDomain) + sb.append(''' + System.out.println("«fd.name» = " + esecuzione.«fd.name».get()); + ''') + if (fd.codomain instanceof EnumTd) + sb.append(''' + System.out.println("«fd.name» = " + esecuzione.«fd.name».oldValue.name()); + ''') + } else { + + if (fd.domain instanceof EnumTd && fd.codomain instanceof ConcreteDomain) { + sb.append(''' + for(int i=0; i < esecuzione.«fd.domain.name»_elemsList.size(); i++){ + System.out.println(" «fd.name» => (" + esecuzione.«fd.domain.name»_elemsList.get(i) + + ") = " + esecuzione.«fd.name».oldValues.get(esecuzione.«fd.domain.name»_elemsList.get(i)).value); + } + ''') + } + + if (fd.domain instanceof EnumTd && fd.codomain instanceof EnumTd) { + sb.append(''' + for(int i=0; i < esecuzione.«fd.domain.name»_elemsList.size(); i++){ + System.out.println("«fd.name» => (" + esecuzione.«fd.domain.name»_elemsList.get(i) + + ") = "+ esecuzione.«fd.name».oldValues.get(esecuzione.«fd.domain.name»_elemsList.get(i))); + } + ''') + } + + } + } + + } + + return sb.toString + } + + def setMonitoredArgs(Asm asm, StringBuffer sb) { + val asmName = asm.name + sb.append(''' ''') + for (fd : asm.headerSection.signature.function) { + if (fd instanceof MonitoredFunction) { + if (fd.domain === null) { // [] -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + if (fd.codomain.name.equals("Boolean")) { // [] -> Boolean + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''boolean «fd.name»,''') + } + else if (fd.codomain.name.equals("Integer") || (fd.codomain instanceof ConcreteDomain)) { // [] -> (Integer|ConcreteDomain) + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''int «fd.name»,''') + } + else if (fd.codomain.name.equals("String")) { // [] -> String + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''String «fd.name»,''') + } + else if (fd.codomain instanceof EnumTd) { // [] -> Enum + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''«asmName».«fd.codomain.name» «fd.name»,''') + } + else if (fd.codomain instanceof AbstractTd) { // [] -> Abstract + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''String «fd.name»,''') + } + } + else { // (Enum|Abstract) -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + var dd = fd.domain + if(dd instanceof EnumTd){ // Enum -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + for (var int i = 0; i < dd.element.size; i++) { + var symbol = new ToString(asm).visit(dd.element.get(i)) + if(fd.codomain.name.equals("Integer") || (fd.codomain instanceof ConcreteDomain)){ // Enum -> (Integer|ConcreteDomain) + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''int «fd.name»_«symbol»,''') + } + else if(fd.codomain.name.equals("Boolean")){ // Enum -> Boolean + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''boolean «fd.name»_«symbol»,''') + } + else if(fd.codomain.name.equals("String")){ // Enum -> String + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''String «fd.name»_«symbol»,''') + } + else /*if (fd.codomain instanceof EnumTd || fd.codomain instanceof AbstractTd)*/ { // Enum -> (Enum|Abstract) + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''«asmName».«fd.codomain.name» «fd.name»_«symbol»,''') + } + } + } + else if(fd.domain instanceof AbstractTd){ // Abstract -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + for (sf : asm.headerSection.signature.function) { + if(sf instanceof StaticFunction ){ + if(sf.codomain.equals(fd.domain) && sf.domain===null){ + var symbol = sf.name + if(fd.codomain.name.equals("Integer") || (fd.codomain instanceof ConcreteDomain)){ // Abstract -> (Integer|ConcreteDomain) + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''int «fd.name»_«symbol»,''') + } + else if(fd.codomain.name.equals("Boolean")){ // Abstract -> Boolean + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''boolean «fd.name»_«symbol»,''') + } + else if(fd.codomain.name.equals("String")){ // Abstract -> String + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''String «fd.name»_«symbol»,''') + } + else /*if (fd.codomain instanceof EnumTd || fd.codomain instanceof AbstractTd)*/ { // Abstract -> (Enum|Abstract) + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''«asmName».«fd.codomain.name» «fd.name»_«symbol»,''') + } + } + } + } + } + } + } + } + sb.setLength(sb.length() - 1); + } + + def setMonitored(Asm asm) { + var sb = new StringBuffer; + for (fd : asm.headerSection.signature.function) { + if (fd instanceof MonitoredFunction) { + if (fd.domain === null) { // [] -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + if (fd.codomain instanceof EnumTd) { // [] -> Enum + sb.append(''' + this.esecuzione.«fd.name».set(«fd.name»); + System.out.println("Set «fd.name» = " + «fd.name»);''') + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + else if (fd.codomain instanceof ConcreteDomain) { // [] -> ConcreteDomain + sb.append(''' + this.esecuzione.«fd.name».set( + «asm.name».«fd.codomain.name».valueOf( + this.esecuzione.«fd.codomain.name»_elems.get( + «fd.name» - this.esecuzione.«fd.codomain.name»_elems.get(0)))); + System.out.println("Set «fd.name» = " + «fd.name»);''') + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + else if (fd.codomain instanceof AbstractTd) { // [] -> Abstract + sb.append(''' + this.esecuzione.«fd.name».set( + this.esecuzione.«fd.codomain.name»_Class.get( + this.esecuzione.«fd.codomain.name»_elemsList.indexOf(«fd.name»))); + System.out.println("Set «fd.name» = " + «fd.name»);''') + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + else{ // [] -> (Integer|String|Boolean) + sb.append(''' + this.esecuzione.«fd.name».set(«fd.name»); + System.out.println("Set «fd.name» = " + «fd.name»);''') + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + } else { // (Enum|Abstract) -> (Integer|String|Boolean|ConcreteDomain|Enum|Abstract) + var dd = fd.domain + if(dd instanceof EnumTd){ // Enum -> ... + for (var int i = 0; i < dd.element.size; i++) { + var symbol = new ToString(asm).visit(dd.element.get(i)) + if(fd.codomain instanceof ConcreteDomain){ // Enum -> ConcreteDomain + sb.append(''' + this.esecuzione.«fd.name».set( + «asm.name».«dd.name».«symbol», + «asm.name».«fd.codomain.name».valueOf(this.esecuzione.«fd.codomain.name»_elems.get(«fd.name»_«symbol»))); + System.out.println("Set «fd.name»_«symbol» = " + «fd.name»_«symbol»);''') + } + else{ // Enum -> (Integer|String|Boolean|Enum|Abstract) + sb.append(''' + this.esecuzione.«fd.name».set( + «asm.name».«dd.name».«symbol», «fd.name»_«symbol»);'''); + } + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + } + else if(fd.domain instanceof AbstractTd){ // Abstract -> ... + for (sf : asm.headerSection.signature.function) { + if(sf instanceof StaticFunction){ + if(sf.codomain.equals(fd.domain) && sf.domain===null){ + var symbol = sf.name + if(fd.codomain instanceof ConcreteDomain){ // Abstract -> ConcreteDomain + sb.append(''' + this.esecuzione.«fd.name».set( + this.esecuzione.«fd.domain.name»_Class.get( + this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")), + «asm.name».«fd.codomain.name».valueOf(this.esecuzione.«fd.codomain.name»_elems.get(«fd.name»_«symbol»))); + System.out.println("Set «fd.name»_«symbol» = " + «fd.name»_«symbol»);''') + } + else{ // Abstract -> (Integer|String|Boolean|Enum|Abstract) + sb.append(''' + this.esecuzione.«fd.name».set( + this.esecuzione.«fd.domain.name»_Class.get( + this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")),«fd.name»_«symbol»); + System.out.println("Set «fd.name»_«symbol» = " + «fd.name»_«symbol»);''') + } + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } + } + } + } + } + } + } + + return sb.toString + } + + def setIsFinalState(Asm asm, StringBuffer sb){ + if(finalStateConditions !== null && !finalStateConditions.isEmpty){ + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + sb.append("\t").append('''// final state condition''') + sb.append(System.lineSeparator) + sb.append("\t").append('''public boolean isFinalState(){''') + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return''') + var numberOfConditionsExpected = 0 + var numberOfConditionsActual = 0 + var ss = new StringBuffer; + for(condition : finalStateConditions){ + numberOfConditionsExpected += 1 + val cond_name = condition.replaceAll("^\\s*(\\w+)\\s*.*$", "$1") + var cond_value = condition.replaceAll("^\\s*\\w+\\s*(.*)$", "$1") + + if(cond_name.toLowerCase.equals("stato")){ + ss.append(System.lineSeparator) + ss.append("\t\t\t").append('''this.stato «cond_value» &&''') + numberOfConditionsActual +=1 + } else { + if(!cond_value.matches("\\d+")){ // se la condizione non è numerica + var cond_value_operators = cond_value.replaceAll("^([><=!]+).*", "$1"); + cond_value = '''«asm.name».«cond_value.replaceAll("^([><=!]+)(.*)","$2")»''' ; // aggiungo il prefisso + cond_value = cond_value_operators.concat(cond_value) + } + for(fd : asm.headerSection.signature.function){ + if(fd instanceof ControlledFunction && fd.name.equals(cond_name)){ + ss.append(System.lineSeparator) + ss.append("\t\t\t").append('''this.get_«fd.name»() «cond_value» &&''') + numberOfConditionsActual +=1 + } + } + } + } + if(numberOfConditionsActual == 0){ + sb.append(" true;") + sb.append(System.lineSeparator) + sb.append("\t").append('''// ERROR - NO Conditions found''') + } + else if(numberOfConditionsActual == numberOfConditionsExpected){ + sb.append(ss.toString) + sb.setLength(sb.length() - 3) + sb.append(''';''') + } + else{ + sb.append(ss.toString) + sb.setLength(sb.length() - 3) + sb.append(''';''') + sb.append(System.lineSeparator) + sb.append("\t").append('''// ERROR - «numberOfConditionsExpected-numberOfConditionsActual» Conditions not generated''') + } + sb.append(System.lineSeparator) + sb.append("\t").append('''}''') + sb.append(System.lineSeparator) + } + } + +} diff --git a/asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator2.xtend b/asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator2.xtend index ea0c863..49b97c2 100644 --- a/asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator2.xtend +++ b/asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator2.xtend @@ -14,6 +14,7 @@ import asmeta.definitions.domains.SequenceDomain import asmeta.definitions.domains.EnumTd import asmeta.definitions.MonitoredFunction import org.asmeta.asm2java.ToString +import asmeta.definitions.StaticFunction class JavaASMGenerator2 extends AsmToJavaGenerator { @@ -88,7 +89,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { System.out.println(""); printControlled(); - setMonitored('''); + setMonitored( '''); for (fd : asm.headerSection.signature.function) { if (fd instanceof MonitoredFunction) { @@ -103,7 +104,6 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { } } } - sb.setLength(sb.length() - 1); sb.append('''); this.esecuzione.updateASM(); @@ -178,7 +178,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { } - private void setMonitored('''); + private void setMonitored( '''); setMonitoredArgs(asm,sb); @@ -263,8 +263,8 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { else{ // fd.domain != null for(dd : asm.headerSection.signature.domain){ if(dd.equals(fd.domain)){ + sb.append("\t").append('''private void cover_«fd.name»(){'''); if(dd instanceof EnumTd){ - sb.append("\t").append('''private void cover_«fd.name»(){'''); for (var int i = 0; i < dd.element.size; i++) { var symbol = new ToString(asm).visit(dd.element.get(i)) sb.append(System.lineSeparator) @@ -277,6 +277,31 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { sb.append(System.lineSeparator) sb.append(System.lineSeparator) } + else if (dd instanceof AbstractTd) { + var i = 0 + for (sf : asm.headerSection.signature.function) { // controllo le funzioni statiche e prendo quelle che aggiungono al dominio astratto + if(sf instanceof StaticFunction){ + if(sf.codomain.equals(dd)){ + i+=1 + var symbol = sf.name + sb.append(System.lineSeparator) + sb.append("\t\t").append('''this.get_«fd.name»_«symbol»();'''); + } + } + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''//«i» Branch covered'''); + } + else { + sb.append(System.lineSeparator) + sb.append("\t\t").append('''this.get_«fd.name»();'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''//1 Branch covered'''); + } + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) } } } @@ -313,8 +338,15 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { } '''); } + if (fd.codomain instanceof ConcreteDomain) { + sb.append(''' + + private int get_«fd.name»(){ + return this.esecuzione.«fd.name».get().value; + } + '''); + } if (fd.codomain instanceof EnumTd || - fd.codomain instanceof ConcreteDomain || fd.codomain instanceof AbstractTd) { sb.append(''' @@ -357,8 +389,15 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { } '''); } + if (fd.codomain instanceof ConcreteDomain) { + sb.append(''' + + public int get_«fd.name»(){ + return this.esecuzione.«fd.name».get().value; + } + '''); + } if (fd.codomain instanceof EnumTd || - fd.codomain instanceof ConcreteDomain || fd.codomain instanceof AbstractTd) { sb.append(''' @@ -368,7 +407,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { '''); } } - else{ // TODO: Da sistemare i getter per le funzioni con Dominio -> Codominio + else{ // getter per le funzioni con Dominio -> Codominio for(dd : asm.headerSection.signature.domain){ if(dd.equals(fd.domain)){ @@ -384,9 +423,19 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»)).value;'''); sb.append(System.lineSeparator) sb.append("\t").append('''}'''); - } - else{ - sb.append("\t").append('''public «asmName».«fd.codomain.name» get_«fd.name»_«symbol»(){'''); + } else{ + if (fd.codomain.name.equals("Integer")){ + sb.append("\t").append('''public int get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("Boolean")){ + sb.append("\t").append('''public boolean get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("String")){ + sb.append("\t").append('''public String get_«fd.name»_«symbol»(){'''); + } + else{ + sb.append("\t").append('''public «asmName».«fd.codomain.name» get_«fd.name»_«symbol»(){'''); + } sb.append(System.lineSeparator) sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get('''); sb.append(System.lineSeparator) @@ -397,6 +446,49 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { sb.append(System.lineSeparator) } } + else if(dd instanceof AbstractTd){ + for (sf : asm.headerSection.signature.function) { // controllo le funzioni statiche e prendo quelle che aggiungono al dominio astratto + if(sf instanceof StaticFunction){ + if(sf.codomain.equals(dd)){ + var symbol = sf.name + sb.append(System.lineSeparator) + if(fd.codomain instanceof ConcreteDomain){ + sb.append("\t").append('''public int get_«fd.name»_«symbol»(){'''); + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")).value);'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } else{ + if (fd.codomain.name.equals("Integer")){ + sb.append("\t").append('''public int get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("Boolean")){ + sb.append("\t").append('''public boolean get_«fd.name»_«symbol»(){'''); + } + else if (fd.codomain.name.equals("String")){ + sb.append("\t").append('''public Srting get_«fd.name»_«symbol»(){'''); + } + else{ + sb.append("\t").append('''public «fd.codomain.name» get_«fd.name»_«symbol»(){'''); + } + sb.append(System.lineSeparator) + sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get('''); + sb.append(System.lineSeparator) + sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")));'''); + sb.append(System.lineSeparator) + sb.append("\t").append('''}'''); + } + sb.append(System.lineSeparator) + } + } + } + } } } } @@ -480,6 +572,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { def setMonitoredArgs(Asm asm, StringBuffer sb) { val asmName = asm.name + sb.append(''' ''') for (fd : asm.headerSection.signature.function) { if (fd instanceof MonitoredFunction) { if (fd.domain === null) { @@ -491,6 +584,10 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { sb.append(System.lineSeparator()).append("\t\t") sb.append('''int «fd.name»,''') } + else if (fd.codomain.name.equals("String") && !(fd.codomain instanceof ConcreteDomain)) { + sb.append(System.lineSeparator()).append("\t\t") + sb.append('''String «fd.name»,''') + } else if (fd.codomain instanceof EnumTd) { sb.append(System.lineSeparator()).append("\t\t") sb.append('''«asmName».«fd.codomain.name» «fd.name»,''') @@ -501,7 +598,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { } else if (fd.codomain instanceof AbstractTd) { sb.append(System.lineSeparator()).append("\t\t") - sb.append('''int «fd.name»,''') + sb.append('''String «fd.name»,''') } } else { @@ -528,23 +625,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { if (fd instanceof MonitoredFunction) { // Solo se il dominio » nullo, quindi funzioni che ricadono nella struttura zero if (fd.domain === null) { - // Caso relativo alle variabili booleane non concrete - if (fd.codomain.name.equals("Boolean") && !(fd.codomain instanceof ConcreteDomain)) { - sb.append(''' - this.esecuzione.«fd.name».set(«fd.name»); - System.out.println("Set «fd.name» = " + «fd.name»);''') - sb.append(System.lineSeparator) - sb.append(System.lineSeparator) - } - - if (fd.codomain.name.equals("Integer") && !(fd.codomain instanceof ConcreteDomain)) { - sb.append(''' - this.esecuzione.«fd.name».set(«fd.name»); - System.out.println("Set «fd.name» = " + «fd.name»);''') - sb.append(System.lineSeparator) - sb.append(System.lineSeparator) - } - + if (fd.codomain instanceof EnumTd) { sb.append(''' this.esecuzione.«fd.name».set(«fd.name»); @@ -552,8 +633,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { sb.append(System.lineSeparator) sb.append(System.lineSeparator) } - - if (fd.codomain instanceof ConcreteDomain) { + else if (fd.codomain instanceof ConcreteDomain) { sb.append(''' this.esecuzione.«fd.name».set( «asm.name».«fd.codomain.name».valueOf( @@ -563,14 +643,22 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { sb.append(System.lineSeparator) sb.append(System.lineSeparator) } - - if (fd.codomain instanceof AbstractTd) { + else if (fd.codomain instanceof AbstractTd) { sb.append(''' - this.esecuzione.«fd.name».set(this.esecuzione.«fd.codomain.name»_Class.get(«fd.name»)); + this.esecuzione.«fd.name».set( + this.esecuzione.«fd.codomain.name»_Class.get( + this.esecuzione.«fd.codomain.name»_elemsList.indexOf(«fd.name»))); System.out.println("Set «fd.name» = " + «fd.name»);''') sb.append(System.lineSeparator) sb.append(System.lineSeparator) } + else{ + sb.append(''' + this.esecuzione.«fd.name».set(«fd.name»); + System.out.println("Set «fd.name» = " + «fd.name»);''') + sb.append(System.lineSeparator) + sb.append(System.lineSeparator) + } } else { /* TODO: fix the index i @@ -606,33 +694,60 @@ class JavaASMGenerator2 extends AsmToJavaGenerator { def setIsFinalState(Asm asm, StringBuffer sb){ if(finalStateConditions !== null && !finalStateConditions.isEmpty){ + sb.append(System.lineSeparator) sb.append(System.lineSeparator) sb.append("\t").append('''// final state condition''') sb.append(System.lineSeparator) sb.append("\t").append('''public boolean isFinalState(){''') sb.append(System.lineSeparator) sb.append("\t\t").append('''return''') + var numberOfConditionsExpected = 0 + var numberOfConditionsActual = 0 + var ss = new StringBuffer; for(condition : finalStateConditions){ - + numberOfConditionsExpected += 1 val cond_name = condition.replaceAll("^\\s*(\\w+)\\s*.*$", "$1") - val cond_value = condition.replaceAll("^\\s*\\w+\\s*(.*)$", "$1") - + var cond_value = condition.replaceAll("^\\s*\\w+\\s*(.*)$", "$1") + if(cond_name.toLowerCase.equals("stato")){ - sb.append(System.lineSeparator) - sb.append("\t\t\t").append('''this.stato «cond_value» &&''') - } - else{ - for(fd : asm.headerSection.signature.function) + ss.append(System.lineSeparator) + ss.append("\t\t\t").append('''this.stato «cond_value» &&''') + numberOfConditionsActual +=1 + } else { + if(!cond_value.matches("\\d+")){ // se la condizione non è numerica + var cond_value_operators = cond_value.replaceAll("^([><=!]+).*", "$1"); + cond_value = '''«asm.name».«cond_value.replaceAll("^([><=!]+)(.*)","$2")»''' ; // aggiungo il prefisso + cond_value = cond_value_operators.concat(cond_value) + } + for(fd : asm.headerSection.signature.function){ if(fd instanceof ControlledFunction && fd.name.equals(cond_name)){ - sb.append(System.lineSeparator) - sb.append("\t\t\t").append('''this.get_«fd.name»() «cond_value» &&''') + ss.append(System.lineSeparator) + ss.append("\t\t\t").append('''this.get_«fd.name»() «cond_value» &&''') + numberOfConditionsActual +=1 } } + } + } + if(numberOfConditionsActual == 0){ + sb.append(" true;") + sb.append(System.lineSeparator) + sb.append("\t").append('''// ERROR - NO Conditions found''') + } + else if(numberOfConditionsActual == numberOfConditionsExpected){ + sb.append(ss.toString) + sb.setLength(sb.length() - 3) + sb.append(''';''') + } + else{ + sb.append(ss.toString) + sb.setLength(sb.length() - 3) + sb.append(''';''') + sb.append(System.lineSeparator) + sb.append("\t").append('''// ERROR - «numberOfConditionsExpected-numberOfConditionsActual» Conditions not generated''') } - sb.setLength(sb.length() - 3) - sb.append(''';''') sb.append(System.lineSeparator) sb.append("\t").append('''}''') + sb.append(System.lineSeparator) } } diff --git a/asmetal2java_codegen/src/org/asmeta/asm2java/main/MainClass.java b/asmetal2java_codegen/src/org/asmeta/asm2java/main/MainClass.java index 11d8dfb..0b9e591 100644 --- a/asmetal2java_codegen/src/org/asmeta/asm2java/main/MainClass.java +++ b/asmetal2java_codegen/src/org/asmeta/asm2java/main/MainClass.java @@ -44,7 +44,7 @@ public class MainClass { // the generator for the code static private JavaGenerator jGenerator = new JavaGenerator(); static private JavaExeGenerator jGeneratorExe = new JavaExeGenerator(); - static private JavaASMGenerator2 jGeneratorASM = new JavaASMGenerator2(); + static private JavaASMGenerator jGeneratorASM = new JavaASMGenerator(); // default translator options diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.FunctionToJavaDef.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.FunctionToJavaDef.xtendbin index f8e5358..7920cf9 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.FunctionToJavaDef.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.FunctionToJavaDef.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.RuleToJava.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.RuleToJava.xtendbin index 50d7df6..a95574f 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.RuleToJava.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.RuleToJava.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJava.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJava.xtendbin index 9d2a8de..f56f10d 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJava.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJava.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.java._trace b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.java._trace index bf64046..b021bd2 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.java._trace and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.java._trace differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.xtendbin index 6bdd81d..18ce670 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.TermToJavaStandardLibrary.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/RuleToJava.java b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/RuleToJava.java index d0b3932..972a23c 100644 --- a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/RuleToJava.java +++ b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/RuleToJava.java @@ -284,7 +284,7 @@ public String visit(final UpdateRule object) { _builder_1.append(_visit_2); String _visit_3 = new TermToJava(this.res, false).visit(object.getUpdatingTerm()); _builder_1.append(_visit_3); - _builder_1.append(".value);"); + _builder_1.append(");"); _builder_1.newLineIfNotEmpty(); _builder_1.append("\t\t\t "); String _visit_4 = new TermToJavaInUpdateRule(this.res, false).visit(object.getLocation()); diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/TermToJava.java b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/TermToJava.java index 3544cd1..e0bf2fc 100644 --- a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/TermToJava.java +++ b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/TermToJava.java @@ -376,19 +376,37 @@ public String visit(final ExistTerm object) { _builder_2.newLineIfNotEmpty(); sb.append(_builder_2); } else { - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append("\t"); Domain _domain_4 = object.getRanges().get(i).getDomain(); - String _visit_3 = new ToString(this.res).visit(((PowersetDomain) _domain_4).getBaseDomain()); - _builder_3.append(_visit_3); - _builder_3.append(".elems.stream().anyMatch(c -> c.equals("); - int _length_1 = app.length(); - int _minus_1 = (_length_1 - 1); - String _substring_1 = app.substring(13, _minus_1); - _builder_3.append(_substring_1); - _builder_3.append("))"); - _builder_3.newLineIfNotEmpty(); - sb.append(_builder_3); + Domain _baseDomain_2 = ((PowersetDomain) _domain_4).getBaseDomain(); + if ((_baseDomain_2 instanceof ConcreteDomain)) { + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("\t"); + Domain _domain_5 = object.getRanges().get(i).getDomain(); + String _visit_3 = new ToString(this.res).visit(((PowersetDomain) _domain_5).getBaseDomain()); + _builder_3.append(_visit_3); + _builder_3.append(".elems.stream().anyMatch(c -> c.equals("); + int _length_1 = app.length(); + int _minus_1 = (_length_1 - 7); + String _substring_1 = app.substring(13, _minus_1); + _builder_3.append(_substring_1); + _builder_3.append("))"); + _builder_3.newLineIfNotEmpty(); + sb.append(_builder_3); + } else { + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append("\t"); + Domain _domain_6 = object.getRanges().get(i).getDomain(); + String _visit_4 = new ToString(this.res).visit(((PowersetDomain) _domain_6).getBaseDomain()); + _builder_4.append(_visit_4); + _builder_4.append(".elems.stream().anyMatch(c -> c.equals("); + int _length_2 = app.length(); + int _minus_2 = (_length_2 - 1); + String _substring_2 = app.substring(13, _minus_2); + _builder_4.append(_substring_2); + _builder_4.append("))"); + _builder_4.newLineIfNotEmpty(); + sb.append(_builder_4); + } } } } @@ -622,7 +640,8 @@ public String visit(final FunctionTerm term) { String name = new Util().parseFunction(term.getFunction().getName()); boolean _hasEvaluateVisitor = ExpressionToJava.hasEvaluateVisitor(name); if (_hasEvaluateVisitor) { - return new ExpressionToJava(this.res).evaluateFunction(name, term.getArguments().getTerms()); + String expression = new ExpressionToJava(this.res).evaluateFunction(name, term.getArguments().getTerms()); + return expression.replaceAll(".value.value", ".value"); } else { if (((term.getFunction() instanceof ControlledFunction) && (term.getDomain() instanceof ConcreteDomain))) { functionTerm.append(this.caseFunctionTermSuppCont(term.getFunction(), term)); diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.AsmToJavaGenerator.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.AsmToJavaGenerator.xtendbin index 7a4d6a4..b3c0b0d 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.AsmToJavaGenerator.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.AsmToJavaGenerator.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator.java._trace b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator.java._trace new file mode 100644 index 0000000..6092ee9 Binary files /dev/null and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator.java._trace differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator.xtendbin new file mode 100644 index 0000000..3fbafe8 Binary files /dev/null and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.java._trace b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.java._trace deleted file mode 100644 index 5976f33..0000000 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.java._trace and /dev/null differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.xtendbin index d0ff174..8e30f13 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaExeGenerator.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaExeGenerator.xtendbin index d2195e9..4893821 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaExeGenerator.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaExeGenerator.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaGenerator.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaGenerator.xtendbin index 60b7af7..0941ef8 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaGenerator.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaGenerator.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaWindowGenerator.xtendbin b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaWindowGenerator.xtendbin index 2e43e3c..5aadcb2 100644 Binary files a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaWindowGenerator.xtendbin and b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaWindowGenerator.xtendbin differ diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/JavaASMGenerator.java b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/JavaASMGenerator.java new file mode 100644 index 0000000..33550e2 --- /dev/null +++ b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/JavaASMGenerator.java @@ -0,0 +1,2232 @@ +package org.asmeta.asm2java.main; + +import asmeta.definitions.ControlledFunction; +import asmeta.definitions.Function; +import asmeta.definitions.MonitoredFunction; +import asmeta.definitions.RuleDeclaration; +import asmeta.definitions.StaticFunction; +import asmeta.definitions.domains.AbstractTd; +import asmeta.definitions.domains.ConcreteDomain; +import asmeta.definitions.domains.Domain; +import asmeta.definitions.domains.EnumTd; +import asmeta.definitions.domains.MapDomain; +import asmeta.definitions.domains.SequenceDomain; +import asmeta.structure.Asm; +import asmeta.transitionrules.basictransitionrules.Rule; +import java.util.ArrayList; +import java.util.List; +import org.asmeta.asm2java.SeqRuleCollector; +import org.asmeta.asm2java.ToString; +import org.eclipse.emf.common.util.EList; +import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Conversions; +import org.junit.Assert; + +@SuppressWarnings("all") +public class JavaASMGenerator extends AsmToJavaGenerator { + public void compileAndWrite(final Asm asm, final String writerPath, final TranslatorOptions userOptions) { + Assert.assertTrue(writerPath.endsWith(".java")); + this.compileAndWrite(asm, writerPath, "JAVA", userOptions); + } + + private List seqCalledRules; + + private String supp; + + private String[] finalStateConditions; + + public String[] setFinalStateConditions(final String[] finalStateConditions) { + return this.finalStateConditions = finalStateConditions; + } + + @Override + public String compileAsm(final Asm asm) { + boolean _optimizeSeqMacroRule = this.options.getOptimizeSeqMacroRule(); + if (_optimizeSeqMacroRule) { + ArrayList _arrayList = new ArrayList(); + this.seqCalledRules = _arrayList; + EList _ruleDeclaration = asm.getBodySection().getRuleDeclaration(); + for (final RuleDeclaration r : _ruleDeclaration) { + this.seqCalledRules.addAll(new SeqRuleCollector(false).visit(r)); + } + } + final String asmName = asm.getName(); + StringBuffer sb = new StringBuffer(); + StringConcatenation _builder = new StringConcatenation(); + _builder.newLine(); + _builder.append("// "); + _builder.append(asmName); + _builder.append("_ASM.java automatically generated from ASM2CODE"); + _builder.newLineIfNotEmpty(); + _builder.newLine(); + _builder.append("import java.util.Scanner;"); + _builder.newLine(); + _builder.newLine(); + _builder.append("/**"); + _builder.newLine(); + _builder.append("* This class allows you to simulate the behavior of an Abstract State Machine (ASM)"); + _builder.newLine(); + _builder.append("* without asking the user for input values ​​of the monitored functions."); + _builder.newLine(); + _builder.append("*"); + _builder.newLine(); + _builder.append("*

"); + _builder.newLine(); + _builder.append("* It has been optimized to be used with evosuite in order to automatically generate test scenarios."); + _builder.newLine(); + _builder.append("*

"); + _builder.newLine(); + _builder.append("*/"); + _builder.newLine(); + _builder.append("class "); + _builder.append(asmName); + _builder.append("_ASM {"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("private final "); + _builder.append(asmName, "\t"); + _builder.append(" esecuzione;"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("private int stato;"); + _builder.newLine(); + _builder.append("\t"); + _builder.newLine(); + _builder.append(" "); + _builder.append("/**"); + _builder.newLine(); + _builder.append(" "); + _builder.append("* Constructor of the {@code "); + _builder.append(asmName, " "); + _builder.append("_ASM} class. Creates a private instance of the asm"); + _builder.newLineIfNotEmpty(); + _builder.append(" "); + _builder.append("* {@link "); + _builder.append(asmName, " "); + _builder.append("} and sets the initial state of the state machine to 1."); + _builder.newLineIfNotEmpty(); + _builder.append(" "); + _builder.append("*/"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("public "); + _builder.append(asmName, "\t"); + _builder.append("_ASM(){"); + _builder.newLineIfNotEmpty(); + _builder.append("\t\t"); + _builder.append("this.esecuzione = new "); + _builder.append(asmName, "\t\t"); + _builder.append("();"); + _builder.newLineIfNotEmpty(); + _builder.append("\t\t"); + _builder.append("this.stato = 0;"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("}"); + _builder.newLine(); + _builder.append("\t"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("/** The step function is the only public method of the ASM,"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("* it receives as parameters the values ​​of the monitored functions to be updated "); + _builder.newLine(); + _builder.append("\t"); + _builder.append("* and allows to perform a step of the asm by incrementing the state."); + _builder.newLine(); + _builder.append("\t"); + _builder.append("*/"); + _builder.newLine(); + _builder.append("\t"); + _builder.append("public void step("); + sb.append(_builder); + this.setMonitoredArgs(asm, sb); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("){"); + _builder_1.newLine(); + _builder_1.append("\t\t\t\t"); + _builder_1.append("System.out.println(\"\");"); + _builder_1.newLine(); + _builder_1.append("\t\t\t\t"); + _builder_1.newLine(); + _builder_1.append("\t\t\t\t"); + _builder_1.append("printControlled();"); + _builder_1.newLine(); + _builder_1.append("\t\t\t\t"); + _builder_1.append("setMonitored( "); + sb.append(_builder_1); + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if ((fd instanceof MonitoredFunction)) { + Domain _domain = ((MonitoredFunction)fd).getDomain(); + boolean _tripleEquals = (_domain == null); + if (_tripleEquals) { + sb.append(System.lineSeparator()); + StringBuffer _append = sb.append("\t\t\t\t\t"); + StringConcatenation _builder_2 = new StringConcatenation(); + String _name = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name); + _builder_2.append(","); + _append.append(_builder_2); + } else { + Domain dd = ((MonitoredFunction)fd).getDomain(); + if ((dd instanceof EnumTd)) { + for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { + { + String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t\t\t\t"); + StringConcatenation _builder_3 = new StringConcatenation(); + String _name_1 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_1); + _builder_3.append("_"); + _builder_3.append(symbol); + _builder_3.append(","); + _append_1.append(_builder_3); + } + } + } + Domain _domain_1 = ((MonitoredFunction)fd).getDomain(); + if ((_domain_1 instanceof AbstractTd)) { + EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); + for (final Function sf : _function_1) { + if ((sf instanceof StaticFunction)) { + if ((((StaticFunction)sf).getCodomain().equals(((MonitoredFunction)fd).getDomain()) && (((StaticFunction)sf).getDomain() == null))) { + String symbol = ((StaticFunction)sf).getName(); + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t\t\t\t"); + StringConcatenation _builder_3 = new StringConcatenation(); + String _name_1 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_1); + _builder_3.append("_"); + _builder_3.append(symbol); + _builder_3.append(","); + _append_1.append(_builder_3); + } + } + } + } + } + } + } + int _length = sb.length(); + int _minus = (_length - 1); + sb.setLength(_minus); + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append(");"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("this.esecuzione.updateASM();"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("System.out.println(\"\");"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("System.out.println(\"\\n\");"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("printControlled();"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("/* monitored */"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("coverMonitored();"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("/* controlled */"); + _builder_4.newLine(); + _builder_4.append("\t\t\t\t"); + _builder_4.append("coverControlled();"); + sb.append(_builder_4); + sb.append(System.lineSeparator()); + if (((this.finalStateConditions != null) && (!((List)Conversions.doWrapArray(this.finalStateConditions)).isEmpty()))) { + StringBuffer _append_2 = sb.append("\t\t\t\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("/* final state condition */"); + _append_2.append(_builder_5); + sb.append(System.lineSeparator()); + StringBuffer _append_3 = sb.append("\t\t\t\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("if(isFinalState()){"); + _builder_6.newLine(); + _builder_6.append("\t\t\t\t\t\t"); + _builder_6.append("System.out.println(\"\\n\");"); + _builder_6.newLine(); + _builder_6.append("\t\t\t\t"); + _builder_6.append("}"); + _builder_6.newLine(); + _builder_6.append("\t\t\t\t"); + _builder_6.append("else"); + _append_3.append(_builder_6); + sb.append(System.lineSeparator()); + } + StringBuffer _append_4 = sb.append("\t\t\t\t\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("stato++;"); + _builder_7.newLine(); + _builder_7.append("\t\t\t\t"); + _builder_7.append("}"); + _append_4.append(_builder_7); + this.setIsFinalState(asm, sb); + sb.append(System.lineSeparator()); + StringBuffer _append_5 = sb.append("\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("// Monitored getters"); + _append_5.append(_builder_8); + this.monitoredGetter(asm, sb); + sb.append(System.lineSeparator()); + StringBuffer _append_6 = sb.append("\t\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append("// Controlled getters"); + _append_6.append(_builder_9); + sb.append(System.lineSeparator()); + this.controlledGetter(asm, sb); + sb.append(System.lineSeparator()); + StringBuffer _append_7 = sb.append("\t"); + StringConcatenation _builder_10 = new StringConcatenation(); + _builder_10.append("// Cover functions"); + _append_7.append(_builder_10); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + StringBuffer _append_8 = sb.append("\t"); + StringConcatenation _builder_11 = new StringConcatenation(); + _builder_11.append("private void coverMonitored(){"); + _append_8.append(_builder_11); + this.coverFunctions(asm, sb, true); + sb.append(System.lineSeparator()); + StringBuffer _append_9 = sb.append("\t"); + StringConcatenation _builder_12 = new StringConcatenation(); + _builder_12.append("}"); + _builder_12.newLine(); + _builder_12.newLine(); + _builder_12.append("\t"); + _builder_12.append("private void coverControlled(){"); + _append_9.append(_builder_12); + this.coverFunctions(asm, sb, false); + sb.append(System.lineSeparator()); + StringBuffer _append_10 = sb.append("\t"); + StringConcatenation _builder_13 = new StringConcatenation(); + _builder_13.append("}"); + _append_10.append(_builder_13); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + this.coverBranches(asm, sb); + StringConcatenation _builder_14 = new StringConcatenation(); + _builder_14.newLine(); + _builder_14.append("\t"); + _builder_14.append("// ASM Methods"); + _builder_14.newLine(); + _builder_14.append("\t"); + _builder_14.newLine(); + _builder_14.append("\t"); + _builder_14.append("private void printControlled() {"); + _builder_14.newLine(); + _builder_14.append("\t"); + _builder_14.newLine(); + _builder_14.append("\t\t"); + String _printControlled = this.printControlled(asm); + _builder_14.append(_printControlled, "\t\t"); + _builder_14.newLineIfNotEmpty(); + _builder_14.append("\t"); + _builder_14.newLine(); + _builder_14.append("\t"); + _builder_14.append("}"); + _builder_14.newLine(); + _builder_14.append("\t"); + _builder_14.newLine(); + _builder_14.append("\t"); + _builder_14.append("private void setMonitored( "); + sb.append(_builder_14); + this.setMonitoredArgs(asm, sb); + StringConcatenation _builder_15 = new StringConcatenation(); + _builder_15.append(") {"); + _builder_15.newLine(); + _builder_15.append("\t\t\t\t\t"); + _builder_15.newLine(); + _builder_15.append("\t\t\t\t\t"); + String _setMonitored = this.setMonitored(asm); + _builder_15.append(_setMonitored, "\t\t\t\t\t"); + _builder_15.newLineIfNotEmpty(); + _builder_15.append("\t\t\t\t"); + _builder_15.append("}"); + _builder_15.newLine(); + _builder_15.append("\t\t\t"); + _builder_15.append("}"); + sb.append(_builder_15); + return sb.toString(); + } + + public void coverFunctions(final Asm asm, final StringBuffer sb, final boolean monitored) { + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if (((fd instanceof MonitoredFunction) && (monitored == true))) { + sb.append(System.lineSeparator()); + StringBuffer _append = sb.append("\t\t"); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("cover_"); + String _name = fd.getName(); + _builder.append(_name); + _builder.append("();"); + _append.append(_builder); + } + } + EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd_1 : _function_1) { + if (((fd_1 instanceof ControlledFunction) && (monitored == false))) { + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t"); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("cover_"); + String _name_1 = fd_1.getName(); + _builder_1.append(_name_1); + _builder_1.append("();"); + _append_1.append(_builder_1); + } + } + } + + public void coverBranches(final Asm asm, final StringBuffer sb) { + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if (((fd instanceof MonitoredFunction) || (fd instanceof ControlledFunction))) { + Domain _domain = fd.getDomain(); + boolean _tripleEquals = (_domain == null); + if (_tripleEquals) { + StringBuffer _append = sb.append("\t"); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("private void cover_"); + String _name = fd.getName(); + _builder.append(_name); + _builder.append("(){"); + _append.append(_builder); + Domain _codomain = fd.getCodomain(); + if ((_codomain instanceof EnumTd)) { + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t"); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("switch(this.get_"); + String _name_1 = fd.getName(); + _builder_1.append(_name_1); + _builder_1.append("()){"); + _append_1.append(_builder_1); + EList _domain_1 = asm.getHeaderSection().getSignature().getDomain(); + for (final Domain dd : _domain_1) { + boolean _equals = dd.equals(fd.getCodomain()); + if (_equals) { + if ((dd instanceof EnumTd)) { + for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { + { + String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); + sb.append(System.lineSeparator()); + StringBuffer _append_2 = sb.append("\t\t\t"); + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("case "); + _builder_2.append(symbol); + _builder_2.append(" :"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("\t\t\t\t\t\t\t"); + _builder_2.append("System.out.println(\"Branch "); + String _name_2 = fd.getCodomain().getName(); + _builder_2.append(_name_2, "\t\t\t\t\t\t\t"); + _builder_2.append(" "); + _builder_2.append(symbol, "\t\t\t\t\t\t\t"); + _builder_2.append(" covered\");"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("\t\t\t\t\t\t\t"); + _builder_2.append("// Branch "); + String _name_3 = fd.getCodomain().getName(); + _builder_2.append(_name_3, "\t\t\t\t\t\t\t"); + _builder_2.append(" "); + _builder_2.append(symbol, "\t\t\t\t\t\t\t"); + _builder_2.append(" covered"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("\t\t\t\t\t\t\t"); + _builder_2.append("break;"); + _append_2.append(_builder_2); + } + } + } + } + } + sb.append(System.lineSeparator()); + sb.append("\t\t\t"); + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("}"); + sb.append(_builder_2); + } else { + sb.append(System.lineSeparator()); + StringBuffer _append_2 = sb.append("\t\t"); + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("this.get_"); + String _name_2 = fd.getName(); + _builder_3.append(_name_2); + _builder_3.append("();"); + _append_2.append(_builder_3); + sb.append(System.lineSeparator()); + StringBuffer _append_3 = sb.append("\t\t"); + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append("//1 Branch covered"); + _append_3.append(_builder_4); + } + sb.append(System.lineSeparator()); + StringBuffer _append_4 = sb.append("\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("}"); + _append_4.append(_builder_5); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } else { + EList _domain_2 = asm.getHeaderSection().getSignature().getDomain(); + for (final Domain dd_1 : _domain_2) { + boolean _equals_1 = dd_1.equals(fd.getDomain()); + if (_equals_1) { + StringBuffer _append_5 = sb.append("\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("private void cover_"); + String _name_3 = fd.getName(); + _builder_6.append(_name_3); + _builder_6.append("(){"); + _append_5.append(_builder_6); + if ((dd_1 instanceof EnumTd)) { + for (int i = 0; (i < ((EnumTd)dd_1).getElement().size()); i++) { + { + Domain sd = fd.getCodomain(); + String symbol = new ToString(asm).visit(((EnumTd)dd_1).getElement().get(i)); + sb.append(System.lineSeparator()); + StringBuffer _append_6 = sb.append("\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("this.get_"); + String _name_4 = fd.getName(); + _builder_7.append(_name_4); + _builder_7.append("_"); + _builder_7.append(symbol); + _builder_7.append("();"); + _append_6.append(_builder_7); + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_6 = sb.append("\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("// "); + int _size = ((EnumTd)dd_1).getElement().size(); + _builder_7.append(_size); + _builder_7.append(" Branch covered"); + _append_6.append(_builder_7); + } else { + if ((dd_1 instanceof AbstractTd)) { + int i = 0; + EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); + for (final Function sf : _function_1) { + if ((sf instanceof StaticFunction)) { + if ((((StaticFunction)sf).getCodomain().equals(dd_1) && (((StaticFunction)sf).getDomain() == null))) { + Domain sd = fd.getCodomain(); + if ((sd instanceof EnumTd)) { + sb.append(System.lineSeparator()); + StringBuffer _append_7 = sb.append("\t\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("switch(this.esecuzione."); + String _name_4 = fd.getName(); + _builder_8.append(_name_4); + _builder_8.append(".get("); + _builder_8.newLineIfNotEmpty(); + _builder_8.append("\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_8.append("this.esecuzione."); + String _name_5 = fd.getDomain().getName(); + _builder_8.append(_name_5, "\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_8.append("_Class.get("); + _builder_8.newLineIfNotEmpty(); + _builder_8.append("\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_8.append("this.esecuzione."); + String _name_6 = fd.getDomain().getName(); + _builder_8.append(_name_6, "\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_8.append("_elemsList.indexOf(\""); + String _name_7 = ((StaticFunction)sf).getName(); + _builder_8.append(_name_7, "\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_8.append("\")))){"); + _append_7.append(_builder_8); + for (int j = 0; (j < ((EnumTd)sd).getElement().size()); j++) { + { + String symbol = new ToString(asm).visit(((EnumTd)sd).getElement().get(j)); + sb.append(System.lineSeparator()); + StringBuffer _append_8 = sb.append("\t\t\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append("case "); + _builder_9.append(symbol); + _builder_9.append(" :"); + _builder_9.newLineIfNotEmpty(); + _builder_9.append("\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_9.append("System.out.println(\"Branch "); + String _name_8 = ((StaticFunction)sf).getName(); + _builder_9.append(_name_8, "\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_9.append(" "); + _builder_9.append(symbol, "\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_9.append(" covered\");"); + _builder_9.newLineIfNotEmpty(); + _builder_9.append("\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_9.append("// Branch "); + String _name_9 = ((StaticFunction)sf).getName(); + _builder_9.append(_name_9, "\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_9.append(" "); + _builder_9.append(symbol, "\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_9.append(" covered"); + _builder_9.newLineIfNotEmpty(); + _builder_9.append("\t\t\t\t\t\t\t\t\t\t\t\t"); + _builder_9.append("break;"); + _append_8.append(_builder_9); + int _i = i; + i = (_i + 1); + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_8 = sb.append("\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append("}"); + _append_8.append(_builder_9); + } else { + String symbol = ((StaticFunction)sf).getName(); + sb.append(System.lineSeparator()); + StringBuffer _append_9 = sb.append("\t\t"); + StringConcatenation _builder_10 = new StringConcatenation(); + _builder_10.append("this.get_"); + String _name_8 = fd.getName(); + _builder_10.append(_name_8); + _builder_10.append("_"); + _builder_10.append(symbol); + _builder_10.append("();"); + _append_9.append(_builder_10); + int _i = i; + i = (_i + 1); + } + } + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_10 = sb.append("\t\t"); + StringConcatenation _builder_11 = new StringConcatenation(); + _builder_11.append("//"); + _builder_11.append(i); + _builder_11.append(" Branch covered"); + _append_10.append(_builder_11); + } else { + sb.append(System.lineSeparator()); + StringBuffer _append_11 = sb.append("\t\t"); + StringConcatenation _builder_12 = new StringConcatenation(); + _builder_12.append("this.get_"); + String _name_9 = fd.getName(); + _builder_12.append(_name_9); + _builder_12.append("();"); + _append_11.append(_builder_12); + sb.append(System.lineSeparator()); + StringBuffer _append_12 = sb.append("\t\t"); + StringConcatenation _builder_13 = new StringConcatenation(); + _builder_13.append("//1 Branch covered"); + _append_12.append(_builder_13); + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_13 = sb.append("\t"); + StringConcatenation _builder_14 = new StringConcatenation(); + _builder_14.append("}"); + _append_13.append(_builder_14); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } + } + } + } + } + } + + public void monitoredGetter(final Asm asm, final StringBuffer sb) { + String asmName = asm.getName(); + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if ((fd instanceof MonitoredFunction)) { + Domain _domain = ((MonitoredFunction)fd).getDomain(); + boolean _tripleEquals = (_domain == null); + if (_tripleEquals) { + if ((((MonitoredFunction)fd).getCodomain().getName().equals("Boolean") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { + StringConcatenation _builder = new StringConcatenation(); + _builder.newLine(); + _builder.append("\t\t"); + _builder.append("private boolean get_"); + String _name = ((MonitoredFunction)fd).getName(); + _builder.append(_name, "\t\t"); + _builder.append("(){"); + _builder.newLineIfNotEmpty(); + _builder.append("\t\t\t"); + _builder.append("return this.esecuzione."); + String _name_1 = ((MonitoredFunction)fd).getName(); + _builder.append(_name_1, "\t\t\t"); + _builder.append(".get();"); + _builder.newLineIfNotEmpty(); + _builder.append("\t\t"); + _builder.append("}"); + _builder.newLine(); + sb.append(_builder); + } + if ((((MonitoredFunction)fd).getCodomain().getName().equals("Integer") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.newLine(); + _builder_1.append("\t\t"); + _builder_1.append("private int get_"); + String _name_2 = ((MonitoredFunction)fd).getName(); + _builder_1.append(_name_2, "\t\t"); + _builder_1.append("(){"); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("\t\t\t"); + _builder_1.append("return this.esecuzione."); + String _name_3 = ((MonitoredFunction)fd).getName(); + _builder_1.append(_name_3, "\t\t\t"); + _builder_1.append(".get();"); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("\t\t"); + _builder_1.append("}"); + _builder_1.newLine(); + sb.append(_builder_1); + } + if ((((MonitoredFunction)fd).getCodomain().getName().equals("String") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.newLine(); + _builder_2.append("\t\t"); + _builder_2.append("private String get_"); + String _name_4 = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name_4, "\t\t"); + _builder_2.append("(){"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("\t\t\t"); + _builder_2.append("return this.esecuzione."); + String _name_5 = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name_5, "\t\t\t"); + _builder_2.append(".get();"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("\t\t"); + _builder_2.append("}"); + _builder_2.newLine(); + sb.append(_builder_2); + } + Domain _codomain = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain instanceof ConcreteDomain)) { + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.newLine(); + _builder_3.append("\t\t"); + _builder_3.append("private int get_"); + String _name_6 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_6, "\t\t"); + _builder_3.append("(){"); + _builder_3.newLineIfNotEmpty(); + _builder_3.append("\t\t\t"); + _builder_3.append("return this.esecuzione."); + String _name_7 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_7, "\t\t\t"); + _builder_3.append(".get().value;"); + _builder_3.newLineIfNotEmpty(); + _builder_3.append("\t\t"); + _builder_3.append("}"); + _builder_3.newLine(); + sb.append(_builder_3); + } + if (((((MonitoredFunction)fd).getCodomain() instanceof EnumTd) || + (((MonitoredFunction)fd).getCodomain() instanceof AbstractTd))) { + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.newLine(); + _builder_4.append("\t\t"); + _builder_4.append("private "); + _builder_4.append(asmName, "\t\t"); + _builder_4.append("."); + String _name_8 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_4.append(_name_8, "\t\t"); + _builder_4.append(" get_"); + String _name_9 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_9, "\t\t"); + _builder_4.append("(){"); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("\t\t\t"); + _builder_4.append("return this.esecuzione."); + String _name_10 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_10, "\t\t\t"); + _builder_4.append(".get();"); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("\t\t"); + _builder_4.append("}"); + _builder_4.newLine(); + sb.append(_builder_4); + } + } else { + EList _domain_1 = asm.getHeaderSection().getSignature().getDomain(); + for (final Domain dd : _domain_1) { + boolean _equals = dd.equals(((MonitoredFunction)fd).getDomain()); + if (_equals) { + if ((dd instanceof EnumTd)) { + for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { + { + String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); + sb.append(System.lineSeparator()); + Domain _codomain_1 = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain_1 instanceof ConcreteDomain)) { + StringBuffer _append = sb.append("\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("private int get_"); + String _name_11 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_11); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append("(){"); + _append.append(_builder_5); + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("return this.esecuzione."); + String _name_12 = ((MonitoredFunction)fd).getName(); + _builder_6.append(_name_12); + _builder_6.append(".get("); + _append_1.append(_builder_6); + sb.append(System.lineSeparator()); + StringBuffer _append_2 = sb.append("\t\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("this.esecuzione."); + String _name_13 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_7.append(_name_13); + _builder_7.append("_elemsList.get("); + _builder_7.append(i); + _builder_7.append(")).value;"); + _append_2.append(_builder_7); + sb.append(System.lineSeparator()); + StringBuffer _append_3 = sb.append("\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("}"); + _append_3.append(_builder_8); + } else { + boolean _equals_1 = ((MonitoredFunction)fd).getCodomain().getName().equals("Integer"); + if (_equals_1) { + StringBuffer _append_4 = sb.append("\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append("private int get_"); + String _name_14 = ((MonitoredFunction)fd).getName(); + _builder_9.append(_name_14); + _builder_9.append("_"); + _builder_9.append(symbol); + _builder_9.append("(){"); + _append_4.append(_builder_9); + } else { + boolean _equals_2 = ((MonitoredFunction)fd).getCodomain().getName().equals("Boolean"); + if (_equals_2) { + StringBuffer _append_5 = sb.append("\t"); + StringConcatenation _builder_10 = new StringConcatenation(); + _builder_10.append("private boolean get_"); + String _name_15 = ((MonitoredFunction)fd).getName(); + _builder_10.append(_name_15); + _builder_10.append("_"); + _builder_10.append(symbol); + _builder_10.append("(){"); + _append_5.append(_builder_10); + } else { + boolean _equals_3 = ((MonitoredFunction)fd).getCodomain().getName().equals("String"); + if (_equals_3) { + StringBuffer _append_6 = sb.append("\t"); + StringConcatenation _builder_11 = new StringConcatenation(); + _builder_11.append("private String get_"); + String _name_16 = ((MonitoredFunction)fd).getName(); + _builder_11.append(_name_16); + _builder_11.append("_"); + _builder_11.append(symbol); + _builder_11.append("(){"); + _append_6.append(_builder_11); + } else { + StringBuffer _append_7 = sb.append("\t"); + StringConcatenation _builder_12 = new StringConcatenation(); + _builder_12.append("private "); + _builder_12.append(asmName); + _builder_12.append("."); + String _name_17 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_12.append(_name_17); + _builder_12.append(" get_"); + String _name_18 = ((MonitoredFunction)fd).getName(); + _builder_12.append(_name_18); + _builder_12.append("_"); + _builder_12.append(symbol); + _builder_12.append("(){"); + _append_7.append(_builder_12); + } + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_8 = sb.append("\t\t"); + StringConcatenation _builder_13 = new StringConcatenation(); + _builder_13.append("return this.esecuzione."); + String _name_19 = ((MonitoredFunction)fd).getName(); + _builder_13.append(_name_19); + _builder_13.append(".get("); + _append_8.append(_builder_13); + sb.append(System.lineSeparator()); + StringBuffer _append_9 = sb.append("\t\t\t"); + StringConcatenation _builder_14 = new StringConcatenation(); + _builder_14.append("this.esecuzione."); + String _name_20 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_14.append(_name_20); + _builder_14.append("_elemsList.get("); + _builder_14.append(i); + _builder_14.append("));"); + _append_9.append(_builder_14); + sb.append(System.lineSeparator()); + StringBuffer _append_10 = sb.append("\t"); + StringConcatenation _builder_15 = new StringConcatenation(); + _builder_15.append("}"); + _append_10.append(_builder_15); + } + sb.append(System.lineSeparator()); + } + } + } else { + if ((dd instanceof AbstractTd)) { + EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); + for (final Function sf : _function_1) { + if ((sf instanceof StaticFunction)) { + if ((((StaticFunction)sf).getCodomain().equals(dd) && (((StaticFunction)sf).getDomain() == null))) { + String symbol = ((StaticFunction)sf).getName(); + sb.append(System.lineSeparator()); + Domain _codomain_1 = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain_1 instanceof ConcreteDomain)) { + StringBuffer _append = sb.append("\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("private int get_"); + String _name_11 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_11); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append("(){"); + _append.append(_builder_5); + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("return this.esecuzione."); + String _name_12 = ((MonitoredFunction)fd).getName(); + _builder_6.append(_name_12); + _builder_6.append(".get("); + _append_1.append(_builder_6); + sb.append(System.lineSeparator()); + StringBuffer _append_2 = sb.append("\t\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("this.esecuzione."); + String _name_13 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_7.append(_name_13); + _builder_7.append("_Class.get("); + _append_2.append(_builder_7); + sb.append(System.lineSeparator()); + StringBuffer _append_3 = sb.append("\t\t\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("this.esecuzione."); + String _name_14 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_8.append(_name_14); + _builder_8.append("_elemsList.indexOf(\""); + _builder_8.append(symbol); + _builder_8.append("\"))).value;"); + _append_3.append(_builder_8); + sb.append(System.lineSeparator()); + StringBuffer _append_4 = sb.append("\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append("}"); + _append_4.append(_builder_9); + } else { + boolean _equals_1 = ((MonitoredFunction)fd).getCodomain().getName().equals("Integer"); + if (_equals_1) { + StringBuffer _append_5 = sb.append("\t"); + StringConcatenation _builder_10 = new StringConcatenation(); + _builder_10.append("private int get_"); + String _name_15 = ((MonitoredFunction)fd).getName(); + _builder_10.append(_name_15); + _builder_10.append("_"); + _builder_10.append(symbol); + _builder_10.append("(){"); + _append_5.append(_builder_10); + } else { + boolean _equals_2 = ((MonitoredFunction)fd).getCodomain().getName().equals("Boolean"); + if (_equals_2) { + StringBuffer _append_6 = sb.append("\t"); + StringConcatenation _builder_11 = new StringConcatenation(); + _builder_11.append("private boolean get_"); + String _name_16 = ((MonitoredFunction)fd).getName(); + _builder_11.append(_name_16); + _builder_11.append("_"); + _builder_11.append(symbol); + _builder_11.append("(){"); + _append_6.append(_builder_11); + } else { + boolean _equals_3 = ((MonitoredFunction)fd).getCodomain().getName().equals("String"); + if (_equals_3) { + StringBuffer _append_7 = sb.append("\t"); + StringConcatenation _builder_12 = new StringConcatenation(); + _builder_12.append("private Srting get_"); + String _name_17 = ((MonitoredFunction)fd).getName(); + _builder_12.append(_name_17); + _builder_12.append("_"); + _builder_12.append(symbol); + _builder_12.append("(){"); + _append_7.append(_builder_12); + } else { + StringBuffer _append_8 = sb.append("\t"); + StringConcatenation _builder_13 = new StringConcatenation(); + _builder_13.append("private "); + String _name_18 = asm.getName(); + _builder_13.append(_name_18); + _builder_13.append("."); + String _name_19 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_13.append(_name_19); + _builder_13.append(" get_"); + String _name_20 = ((MonitoredFunction)fd).getName(); + _builder_13.append(_name_20); + _builder_13.append("_"); + _builder_13.append(symbol); + _builder_13.append("(){"); + _append_8.append(_builder_13); + } + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_9 = sb.append("\t\t"); + StringConcatenation _builder_14 = new StringConcatenation(); + _builder_14.append("return this.esecuzione."); + String _name_21 = ((MonitoredFunction)fd).getName(); + _builder_14.append(_name_21); + _builder_14.append(".get("); + _append_9.append(_builder_14); + sb.append(System.lineSeparator()); + StringBuffer _append_10 = sb.append("\t\t\t"); + StringConcatenation _builder_15 = new StringConcatenation(); + _builder_15.append("this.esecuzione."); + String _name_22 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_15.append(_name_22); + _builder_15.append("_Class.get("); + _append_10.append(_builder_15); + sb.append(System.lineSeparator()); + StringBuffer _append_11 = sb.append("\t\t\t"); + StringConcatenation _builder_16 = new StringConcatenation(); + _builder_16.append("this.esecuzione."); + String _name_23 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_16.append(_name_23); + _builder_16.append("_elemsList.indexOf(\""); + _builder_16.append(symbol); + _builder_16.append("\")));"); + _append_11.append(_builder_16); + sb.append(System.lineSeparator()); + StringBuffer _append_12 = sb.append("\t"); + StringConcatenation _builder_17 = new StringConcatenation(); + _builder_17.append("}"); + _append_12.append(_builder_17); + } + sb.append(System.lineSeparator()); + } + } + } + } + } + } + } + } + } + } + } + + public void controlledGetter(final Asm asm, final StringBuffer sb) { + String asmName = asm.getName(); + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if ((fd instanceof ControlledFunction)) { + Domain _domain = ((ControlledFunction)fd).getDomain(); + boolean _tripleEquals = (_domain == null); + if (_tripleEquals) { + if ((((ControlledFunction)fd).getCodomain().getName().equals("Boolean") && (!(((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain)))) { + StringConcatenation _builder = new StringConcatenation(); + _builder.newLine(); + _builder.append("\t\t"); + _builder.append("public boolean get_"); + String _name = ((ControlledFunction)fd).getName(); + _builder.append(_name, "\t\t"); + _builder.append("(){"); + _builder.newLineIfNotEmpty(); + _builder.append("\t\t\t"); + _builder.append("return this.esecuzione."); + String _name_1 = ((ControlledFunction)fd).getName(); + _builder.append(_name_1, "\t\t\t"); + _builder.append(".get();"); + _builder.newLineIfNotEmpty(); + _builder.append("\t\t"); + _builder.append("}"); + _builder.newLine(); + sb.append(_builder); + } + if ((((ControlledFunction)fd).getCodomain().getName().equals("Integer") && (!(((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain)))) { + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.newLine(); + _builder_1.append("\t\t"); + _builder_1.append("public int get_"); + String _name_2 = ((ControlledFunction)fd).getName(); + _builder_1.append(_name_2, "\t\t"); + _builder_1.append("(){"); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("\t\t\t"); + _builder_1.append("return this.esecuzione."); + String _name_3 = ((ControlledFunction)fd).getName(); + _builder_1.append(_name_3, "\t\t\t"); + _builder_1.append(".get();"); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("\t\t"); + _builder_1.append("}"); + _builder_1.newLine(); + sb.append(_builder_1); + } + if ((((ControlledFunction)fd).getCodomain().getName().equals("String") && (!(((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain)))) { + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.newLine(); + _builder_2.append("\t\t"); + _builder_2.append("public String get_"); + String _name_4 = ((ControlledFunction)fd).getName(); + _builder_2.append(_name_4, "\t\t"); + _builder_2.append("(){"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("\t\t\t"); + _builder_2.append("return this.esecuzione."); + String _name_5 = ((ControlledFunction)fd).getName(); + _builder_2.append(_name_5, "\t\t\t"); + _builder_2.append(".get();"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("\t\t"); + _builder_2.append("}"); + _builder_2.newLine(); + sb.append(_builder_2); + } + Domain _codomain = ((ControlledFunction)fd).getCodomain(); + if ((_codomain instanceof ConcreteDomain)) { + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.newLine(); + _builder_3.append("\t\t"); + _builder_3.append("public int get_"); + String _name_6 = ((ControlledFunction)fd).getName(); + _builder_3.append(_name_6, "\t\t"); + _builder_3.append("(){"); + _builder_3.newLineIfNotEmpty(); + _builder_3.append("\t\t\t"); + _builder_3.append("return this.esecuzione."); + String _name_7 = ((ControlledFunction)fd).getName(); + _builder_3.append(_name_7, "\t\t\t"); + _builder_3.append(".get().value;"); + _builder_3.newLineIfNotEmpty(); + _builder_3.append("\t\t"); + _builder_3.append("}"); + _builder_3.newLine(); + sb.append(_builder_3); + } + if (((((ControlledFunction)fd).getCodomain() instanceof EnumTd) || + (((ControlledFunction)fd).getCodomain() instanceof AbstractTd))) { + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.newLine(); + _builder_4.append("\t\t"); + _builder_4.append("public "); + _builder_4.append(asmName, "\t\t"); + _builder_4.append("."); + String _name_8 = ((ControlledFunction)fd).getCodomain().getName(); + _builder_4.append(_name_8, "\t\t"); + _builder_4.append(" get_"); + String _name_9 = ((ControlledFunction)fd).getName(); + _builder_4.append(_name_9, "\t\t"); + _builder_4.append("(){"); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("\t\t\t"); + _builder_4.append("return this.esecuzione."); + String _name_10 = ((ControlledFunction)fd).getName(); + _builder_4.append(_name_10, "\t\t\t"); + _builder_4.append(".get();"); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("\t\t"); + _builder_4.append("}"); + _builder_4.newLine(); + sb.append(_builder_4); + } + } else { + EList _domain_1 = asm.getHeaderSection().getSignature().getDomain(); + for (final Domain dd : _domain_1) { + boolean _equals = dd.equals(((ControlledFunction)fd).getDomain()); + if (_equals) { + if ((dd instanceof EnumTd)) { + for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { + { + String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); + sb.append(System.lineSeparator()); + Domain _codomain_1 = ((ControlledFunction)fd).getCodomain(); + if ((_codomain_1 instanceof ConcreteDomain)) { + StringBuffer _append = sb.append("\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("public int get_"); + String _name_11 = ((ControlledFunction)fd).getName(); + _builder_5.append(_name_11); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append("(){"); + _append.append(_builder_5); + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("return this.esecuzione."); + String _name_12 = ((ControlledFunction)fd).getName(); + _builder_6.append(_name_12); + _builder_6.append(".oldValues.get("); + _append_1.append(_builder_6); + sb.append(System.lineSeparator()); + StringBuffer _append_2 = sb.append("\t\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("this.esecuzione."); + String _name_13 = ((ControlledFunction)fd).getDomain().getName(); + _builder_7.append(_name_13); + _builder_7.append("_elemsList.get("); + _builder_7.append(i); + _builder_7.append(")).value;"); + _append_2.append(_builder_7); + sb.append(System.lineSeparator()); + StringBuffer _append_3 = sb.append("\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("}"); + _append_3.append(_builder_8); + } else { + boolean _equals_1 = ((ControlledFunction)fd).getCodomain().getName().equals("Integer"); + if (_equals_1) { + StringBuffer _append_4 = sb.append("\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append("public int get_"); + String _name_14 = ((ControlledFunction)fd).getName(); + _builder_9.append(_name_14); + _builder_9.append("_"); + _builder_9.append(symbol); + _builder_9.append("(){"); + _append_4.append(_builder_9); + } else { + boolean _equals_2 = ((ControlledFunction)fd).getCodomain().getName().equals("Boolean"); + if (_equals_2) { + StringBuffer _append_5 = sb.append("\t"); + StringConcatenation _builder_10 = new StringConcatenation(); + _builder_10.append("public boolean get_"); + String _name_15 = ((ControlledFunction)fd).getName(); + _builder_10.append(_name_15); + _builder_10.append("_"); + _builder_10.append(symbol); + _builder_10.append("(){"); + _append_5.append(_builder_10); + } else { + boolean _equals_3 = ((ControlledFunction)fd).getCodomain().getName().equals("String"); + if (_equals_3) { + StringBuffer _append_6 = sb.append("\t"); + StringConcatenation _builder_11 = new StringConcatenation(); + _builder_11.append("public String get_"); + String _name_16 = ((ControlledFunction)fd).getName(); + _builder_11.append(_name_16); + _builder_11.append("_"); + _builder_11.append(symbol); + _builder_11.append("(){"); + _append_6.append(_builder_11); + } else { + StringBuffer _append_7 = sb.append("\t"); + StringConcatenation _builder_12 = new StringConcatenation(); + _builder_12.append("public "); + _builder_12.append(asmName); + _builder_12.append("."); + String _name_17 = ((ControlledFunction)fd).getCodomain().getName(); + _builder_12.append(_name_17); + _builder_12.append(" get_"); + String _name_18 = ((ControlledFunction)fd).getName(); + _builder_12.append(_name_18); + _builder_12.append("_"); + _builder_12.append(symbol); + _builder_12.append("(){"); + _append_7.append(_builder_12); + } + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_8 = sb.append("\t\t"); + StringConcatenation _builder_13 = new StringConcatenation(); + _builder_13.append("return this.esecuzione."); + String _name_19 = ((ControlledFunction)fd).getName(); + _builder_13.append(_name_19); + _builder_13.append(".oldValues.get("); + _append_8.append(_builder_13); + sb.append(System.lineSeparator()); + StringBuffer _append_9 = sb.append("\t\t\t"); + StringConcatenation _builder_14 = new StringConcatenation(); + _builder_14.append("this.esecuzione."); + String _name_20 = ((ControlledFunction)fd).getDomain().getName(); + _builder_14.append(_name_20); + _builder_14.append("_elemsList.get("); + _builder_14.append(i); + _builder_14.append("));"); + _append_9.append(_builder_14); + sb.append(System.lineSeparator()); + StringBuffer _append_10 = sb.append("\t"); + StringConcatenation _builder_15 = new StringConcatenation(); + _builder_15.append("}"); + _append_10.append(_builder_15); + } + sb.append(System.lineSeparator()); + } + } + } else { + if ((dd instanceof AbstractTd)) { + EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); + for (final Function sf : _function_1) { + if ((sf instanceof StaticFunction)) { + if ((((StaticFunction)sf).getCodomain().equals(dd) && (((StaticFunction)sf).getDomain() == null))) { + String symbol = ((StaticFunction)sf).getName(); + sb.append(System.lineSeparator()); + Domain _codomain_1 = ((ControlledFunction)fd).getCodomain(); + if ((_codomain_1 instanceof ConcreteDomain)) { + StringBuffer _append = sb.append("\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("public int get_"); + String _name_11 = ((ControlledFunction)fd).getName(); + _builder_5.append(_name_11); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append("(){"); + _append.append(_builder_5); + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("return this.esecuzione."); + String _name_12 = ((ControlledFunction)fd).getName(); + _builder_6.append(_name_12); + _builder_6.append(".oldValues.get("); + _append_1.append(_builder_6); + sb.append(System.lineSeparator()); + StringBuffer _append_2 = sb.append("\t\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("this.esecuzione."); + String _name_13 = ((ControlledFunction)fd).getDomain().getName(); + _builder_7.append(_name_13); + _builder_7.append("_Class.get("); + _append_2.append(_builder_7); + sb.append(System.lineSeparator()); + StringBuffer _append_3 = sb.append("\t\t\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("this.esecuzione."); + String _name_14 = ((ControlledFunction)fd).getDomain().getName(); + _builder_8.append(_name_14); + _builder_8.append("_elemsList.indexOf(\""); + _builder_8.append(symbol); + _builder_8.append("\")).value);"); + _append_3.append(_builder_8); + sb.append(System.lineSeparator()); + StringBuffer _append_4 = sb.append("\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append("}"); + _append_4.append(_builder_9); + } else { + boolean _equals_1 = ((ControlledFunction)fd).getCodomain().getName().equals("Integer"); + if (_equals_1) { + StringBuffer _append_5 = sb.append("\t"); + StringConcatenation _builder_10 = new StringConcatenation(); + _builder_10.append("public int get_"); + String _name_15 = ((ControlledFunction)fd).getName(); + _builder_10.append(_name_15); + _builder_10.append("_"); + _builder_10.append(symbol); + _builder_10.append("(){"); + _append_5.append(_builder_10); + } else { + boolean _equals_2 = ((ControlledFunction)fd).getCodomain().getName().equals("Boolean"); + if (_equals_2) { + StringBuffer _append_6 = sb.append("\t"); + StringConcatenation _builder_11 = new StringConcatenation(); + _builder_11.append("public boolean get_"); + String _name_16 = ((ControlledFunction)fd).getName(); + _builder_11.append(_name_16); + _builder_11.append("_"); + _builder_11.append(symbol); + _builder_11.append("(){"); + _append_6.append(_builder_11); + } else { + boolean _equals_3 = ((ControlledFunction)fd).getCodomain().getName().equals("String"); + if (_equals_3) { + StringBuffer _append_7 = sb.append("\t"); + StringConcatenation _builder_12 = new StringConcatenation(); + _builder_12.append("public Srting get_"); + String _name_17 = ((ControlledFunction)fd).getName(); + _builder_12.append(_name_17); + _builder_12.append("_"); + _builder_12.append(symbol); + _builder_12.append("(){"); + _append_7.append(_builder_12); + } else { + StringBuffer _append_8 = sb.append("\t"); + StringConcatenation _builder_13 = new StringConcatenation(); + _builder_13.append("public "); + String _name_18 = asm.getName(); + _builder_13.append(_name_18); + _builder_13.append("."); + String _name_19 = ((ControlledFunction)fd).getCodomain().getName(); + _builder_13.append(_name_19); + _builder_13.append(" get_"); + String _name_20 = ((ControlledFunction)fd).getName(); + _builder_13.append(_name_20); + _builder_13.append("_"); + _builder_13.append(symbol); + _builder_13.append("(){"); + _append_8.append(_builder_13); + } + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_9 = sb.append("\t\t"); + StringConcatenation _builder_14 = new StringConcatenation(); + _builder_14.append("return this.esecuzione."); + String _name_21 = ((ControlledFunction)fd).getName(); + _builder_14.append(_name_21); + _builder_14.append(".oldValues.get("); + _append_9.append(_builder_14); + sb.append(System.lineSeparator()); + StringBuffer _append_10 = sb.append("\t\t\t"); + StringConcatenation _builder_15 = new StringConcatenation(); + _builder_15.append("this.esecuzione."); + String _name_22 = ((ControlledFunction)fd).getDomain().getName(); + _builder_15.append(_name_22); + _builder_15.append("_Class.get("); + _append_10.append(_builder_15); + sb.append(System.lineSeparator()); + StringBuffer _append_11 = sb.append("\t\t\t"); + StringConcatenation _builder_16 = new StringConcatenation(); + _builder_16.append("this.esecuzione."); + String _name_23 = ((ControlledFunction)fd).getDomain().getName(); + _builder_16.append(_name_23); + _builder_16.append("_elemsList.indexOf(\""); + _builder_16.append(symbol); + _builder_16.append("\")));"); + _append_11.append(_builder_16); + sb.append(System.lineSeparator()); + StringBuffer _append_12 = sb.append("\t"); + StringConcatenation _builder_17 = new StringConcatenation(); + _builder_17.append("}"); + _append_12.append(_builder_17); + } + sb.append(System.lineSeparator()); + } + } + } + } + } + } + } + } + } + } + } + + public String printControlled(final Asm asm) { + StringBuffer sb = new StringBuffer(); + EList _domain = asm.getHeaderSection().getSignature().getDomain(); + for (final Domain dd : _domain) { + if ((dd instanceof AbstractTd)) { + StringConcatenation _builder = new StringConcatenation(); + _builder.append("System.out.print(\""); + String _name = ((AbstractTd)dd).getName(); + _builder.append(_name); + _builder.append("\"+ \" = {\");"); + _builder.newLineIfNotEmpty(); + _builder.append("for(int i=0 ; i< esecuzione."); + String _name_1 = ((AbstractTd)dd).getName(); + _builder.append(_name_1); + _builder.append("_elemsList.size(); i++)"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("if(i!= esecuzione."); + String _name_2 = ((AbstractTd)dd).getName(); + _builder.append(_name_2, "\t"); + _builder.append("_elemsList.size()-1)"); + _builder.newLineIfNotEmpty(); + _builder.append("\t\t"); + _builder.append("System.out.print(esecuzione."); + String _name_3 = ((AbstractTd)dd).getName(); + _builder.append(_name_3, "\t\t"); + _builder.append("_elemsList.get(i) +\", \");"); + _builder.newLineIfNotEmpty(); + _builder.append("\t"); + _builder.append("else"); + _builder.newLine(); + _builder.append("\t\t"); + _builder.append("System.out.print(esecuzione."); + String _name_4 = ((AbstractTd)dd).getName(); + _builder.append(_name_4, "\t\t"); + _builder.append("_elemsList.get(i));\t"); + _builder.newLineIfNotEmpty(); + _builder.append("System.out.println(\"}\");"); + _builder.newLine(); + sb.append(_builder); + } + } + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if ((fd instanceof ControlledFunction)) { + Domain _domain_1 = ((ControlledFunction)fd).getDomain(); + boolean _tripleEquals = (_domain_1 == null); + if (_tripleEquals) { + Domain _codomain = ((ControlledFunction)fd).getCodomain(); + if ((_codomain instanceof ConcreteDomain)) { + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("System.out.println(\""); + String _name_5 = ((ControlledFunction)fd).getName(); + _builder_1.append(_name_5); + _builder_1.append(" = \" + esecuzione."); + String _name_6 = ((ControlledFunction)fd).getName(); + _builder_1.append(_name_6); + _builder_1.append(".get().value);"); + _builder_1.newLineIfNotEmpty(); + sb.append(_builder_1); + } + if (((((ControlledFunction)fd).getCodomain().getName().equals("Integer") || ((ControlledFunction)fd).getCodomain().getName().equals("Boolean")) || + ((ControlledFunction)fd).getCodomain().getName().equals("String"))) { + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("System.out.println(\""); + String _name_7 = ((ControlledFunction)fd).getName(); + _builder_2.append(_name_7); + _builder_2.append(" = \" + esecuzione."); + String _name_8 = ((ControlledFunction)fd).getName(); + _builder_2.append(_name_8); + _builder_2.append(".get());"); + _builder_2.newLineIfNotEmpty(); + sb.append(_builder_2); + } + Domain _codomain_1 = ((ControlledFunction)fd).getCodomain(); + if ((_codomain_1 instanceof MapDomain)) { + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("System.out.println(\""); + String _name_9 = ((ControlledFunction)fd).getName(); + _builder_3.append(_name_9); + _builder_3.append(" = \" + esecuzione."); + String _name_10 = ((ControlledFunction)fd).getName(); + _builder_3.append(_name_10); + _builder_3.append(".get());"); + _builder_3.newLineIfNotEmpty(); + sb.append(_builder_3); + } + Domain _codomain_2 = ((ControlledFunction)fd).getCodomain(); + if ((_codomain_2 instanceof SequenceDomain)) { + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append("System.out.println(\""); + String _name_11 = ((ControlledFunction)fd).getName(); + _builder_4.append(_name_11); + _builder_4.append(" = \" + esecuzione."); + String _name_12 = ((ControlledFunction)fd).getName(); + _builder_4.append(_name_12); + _builder_4.append(".get());"); + _builder_4.newLineIfNotEmpty(); + sb.append(_builder_4); + } + Domain _codomain_3 = ((ControlledFunction)fd).getCodomain(); + if ((_codomain_3 instanceof EnumTd)) { + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("System.out.println(\""); + String _name_13 = ((ControlledFunction)fd).getName(); + _builder_5.append(_name_13); + _builder_5.append(" = \" + esecuzione."); + String _name_14 = ((ControlledFunction)fd).getName(); + _builder_5.append(_name_14); + _builder_5.append(".oldValue.name());"); + _builder_5.newLineIfNotEmpty(); + sb.append(_builder_5); + } + } else { + if (((((ControlledFunction)fd).getDomain() instanceof EnumTd) && (((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain))) { + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("for(int i=0; i < esecuzione."); + String _name_15 = ((ControlledFunction)fd).getDomain().getName(); + _builder_6.append(_name_15); + _builder_6.append("_elemsList.size(); i++){"); + _builder_6.newLineIfNotEmpty(); + _builder_6.append("\t"); + _builder_6.append("System.out.println(\" "); + String _name_16 = ((ControlledFunction)fd).getName(); + _builder_6.append(_name_16, "\t"); + _builder_6.append(" => (\" + esecuzione."); + String _name_17 = ((ControlledFunction)fd).getDomain().getName(); + _builder_6.append(_name_17, "\t"); + _builder_6.append("_elemsList.get(i) + "); + _builder_6.newLineIfNotEmpty(); + _builder_6.append("\t"); + _builder_6.append("\") = \" + esecuzione."); + String _name_18 = ((ControlledFunction)fd).getName(); + _builder_6.append(_name_18, "\t"); + _builder_6.append(".oldValues.get(esecuzione."); + String _name_19 = ((ControlledFunction)fd).getDomain().getName(); + _builder_6.append(_name_19, "\t"); + _builder_6.append("_elemsList.get(i)).value);"); + _builder_6.newLineIfNotEmpty(); + _builder_6.append("}"); + _builder_6.newLine(); + sb.append(_builder_6); + } + if (((((ControlledFunction)fd).getDomain() instanceof EnumTd) && (((ControlledFunction)fd).getCodomain() instanceof EnumTd))) { + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("for(int i=0; i < esecuzione."); + String _name_20 = ((ControlledFunction)fd).getDomain().getName(); + _builder_7.append(_name_20); + _builder_7.append("_elemsList.size(); i++){"); + _builder_7.newLineIfNotEmpty(); + _builder_7.append("\t"); + _builder_7.append("System.out.println(\""); + String _name_21 = ((ControlledFunction)fd).getName(); + _builder_7.append(_name_21, "\t"); + _builder_7.append(" => (\" + esecuzione."); + String _name_22 = ((ControlledFunction)fd).getDomain().getName(); + _builder_7.append(_name_22, "\t"); + _builder_7.append("_elemsList.get(i) + "); + _builder_7.newLineIfNotEmpty(); + _builder_7.append("\t"); + _builder_7.append("\") = \"+ esecuzione."); + String _name_23 = ((ControlledFunction)fd).getName(); + _builder_7.append(_name_23, "\t"); + _builder_7.append(".oldValues.get(esecuzione."); + String _name_24 = ((ControlledFunction)fd).getDomain().getName(); + _builder_7.append(_name_24, "\t"); + _builder_7.append("_elemsList.get(i)));"); + _builder_7.newLineIfNotEmpty(); + _builder_7.append("}"); + _builder_7.newLine(); + sb.append(_builder_7); + } + } + } + } + return sb.toString(); + } + + public void setMonitoredArgs(final Asm asm, final StringBuffer sb) { + final String asmName = asm.getName(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append(" "); + sb.append(_builder); + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if ((fd instanceof MonitoredFunction)) { + Domain _domain = ((MonitoredFunction)fd).getDomain(); + boolean _tripleEquals = (_domain == null); + if (_tripleEquals) { + boolean _equals = ((MonitoredFunction)fd).getCodomain().getName().equals("Boolean"); + if (_equals) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("boolean "); + String _name = ((MonitoredFunction)fd).getName(); + _builder_1.append(_name); + _builder_1.append(","); + sb.append(_builder_1); + } else { + if ((((MonitoredFunction)fd).getCodomain().getName().equals("Integer") || (((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain))) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("int "); + String _name_1 = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name_1); + _builder_2.append(","); + sb.append(_builder_2); + } else { + boolean _equals_1 = ((MonitoredFunction)fd).getCodomain().getName().equals("String"); + if (_equals_1) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("String "); + String _name_2 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_2); + _builder_3.append(","); + sb.append(_builder_3); + } else { + Domain _codomain = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain instanceof EnumTd)) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append(asmName); + _builder_4.append("."); + String _name_3 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_4.append(_name_3); + _builder_4.append(" "); + String _name_4 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_4); + _builder_4.append(","); + sb.append(_builder_4); + } else { + Domain _codomain_1 = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain_1 instanceof AbstractTd)) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("String "); + String _name_5 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_5); + _builder_5.append(","); + sb.append(_builder_5); + } + } + } + } + } + } else { + Domain dd = ((MonitoredFunction)fd).getDomain(); + if ((dd instanceof EnumTd)) { + for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { + { + String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); + if ((((MonitoredFunction)fd).getCodomain().getName().equals("Integer") || (((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain))) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("int "); + String _name_6 = ((MonitoredFunction)fd).getName(); + _builder_6.append(_name_6); + _builder_6.append("_"); + _builder_6.append(symbol); + _builder_6.append(","); + sb.append(_builder_6); + } else { + boolean _equals_2 = ((MonitoredFunction)fd).getCodomain().getName().equals("Boolean"); + if (_equals_2) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("boolean "); + String _name_7 = ((MonitoredFunction)fd).getName(); + _builder_7.append(_name_7); + _builder_7.append("_"); + _builder_7.append(symbol); + _builder_7.append(","); + sb.append(_builder_7); + } else { + boolean _equals_3 = ((MonitoredFunction)fd).getCodomain().getName().equals("String"); + if (_equals_3) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("String "); + String _name_8 = ((MonitoredFunction)fd).getName(); + _builder_8.append(_name_8); + _builder_8.append("_"); + _builder_8.append(symbol); + _builder_8.append(","); + sb.append(_builder_8); + } else { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append(asmName); + _builder_9.append("."); + String _name_9 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_9.append(_name_9); + _builder_9.append(" "); + String _name_10 = ((MonitoredFunction)fd).getName(); + _builder_9.append(_name_10); + _builder_9.append("_"); + _builder_9.append(symbol); + _builder_9.append(","); + sb.append(_builder_9); + } + } + } + } + } + } else { + Domain _domain_1 = ((MonitoredFunction)fd).getDomain(); + if ((_domain_1 instanceof AbstractTd)) { + EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); + for (final Function sf : _function_1) { + if ((sf instanceof StaticFunction)) { + if ((((StaticFunction)sf).getCodomain().equals(((MonitoredFunction)fd).getDomain()) && (((StaticFunction)sf).getDomain() == null))) { + String symbol = ((StaticFunction)sf).getName(); + if ((((MonitoredFunction)fd).getCodomain().getName().equals("Integer") || (((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain))) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("int "); + String _name_6 = ((MonitoredFunction)fd).getName(); + _builder_6.append(_name_6); + _builder_6.append("_"); + _builder_6.append(symbol); + _builder_6.append(","); + sb.append(_builder_6); + } else { + boolean _equals_2 = ((MonitoredFunction)fd).getCodomain().getName().equals("Boolean"); + if (_equals_2) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("boolean "); + String _name_7 = ((MonitoredFunction)fd).getName(); + _builder_7.append(_name_7); + _builder_7.append("_"); + _builder_7.append(symbol); + _builder_7.append(","); + sb.append(_builder_7); + } else { + boolean _equals_3 = ((MonitoredFunction)fd).getCodomain().getName().equals("String"); + if (_equals_3) { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_8 = new StringConcatenation(); + _builder_8.append("String "); + String _name_8 = ((MonitoredFunction)fd).getName(); + _builder_8.append(_name_8); + _builder_8.append("_"); + _builder_8.append(symbol); + _builder_8.append(","); + sb.append(_builder_8); + } else { + sb.append(System.lineSeparator()).append("\t\t"); + StringConcatenation _builder_9 = new StringConcatenation(); + _builder_9.append(asmName); + _builder_9.append("."); + String _name_9 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_9.append(_name_9); + _builder_9.append(" "); + String _name_10 = ((MonitoredFunction)fd).getName(); + _builder_9.append(_name_10); + _builder_9.append("_"); + _builder_9.append(symbol); + _builder_9.append(","); + sb.append(_builder_9); + } + } + } + } + } + } + } + } + } + } + } + int _length = sb.length(); + int _minus = (_length - 1); + sb.setLength(_minus); + } + + public String setMonitored(final Asm asm) { + StringBuffer sb = new StringBuffer(); + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if ((fd instanceof MonitoredFunction)) { + Domain _domain = ((MonitoredFunction)fd).getDomain(); + boolean _tripleEquals = (_domain == null); + if (_tripleEquals) { + Domain _codomain = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain instanceof EnumTd)) { + StringConcatenation _builder = new StringConcatenation(); + _builder.append("this.esecuzione."); + String _name = ((MonitoredFunction)fd).getName(); + _builder.append(_name); + _builder.append(".set("); + String _name_1 = ((MonitoredFunction)fd).getName(); + _builder.append(_name_1); + _builder.append(");"); + _builder.newLineIfNotEmpty(); + _builder.append("System.out.println(\"Set "); + String _name_2 = ((MonitoredFunction)fd).getName(); + _builder.append(_name_2); + _builder.append(" = \" + "); + String _name_3 = ((MonitoredFunction)fd).getName(); + _builder.append(_name_3); + _builder.append(");"); + sb.append(_builder); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } else { + Domain _codomain_1 = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain_1 instanceof ConcreteDomain)) { + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("this.esecuzione."); + String _name_4 = ((MonitoredFunction)fd).getName(); + _builder_1.append(_name_4); + _builder_1.append(".set("); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("\t"); + String _name_5 = asm.getName(); + _builder_1.append(_name_5, "\t"); + _builder_1.append("."); + String _name_6 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_1.append(_name_6, "\t"); + _builder_1.append(".valueOf("); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("\t"); + _builder_1.append("this.esecuzione."); + String _name_7 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_1.append(_name_7, "\t"); + _builder_1.append("_elems.get("); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("\t"); + String _name_8 = ((MonitoredFunction)fd).getName(); + _builder_1.append(_name_8, "\t"); + _builder_1.append(" - this.esecuzione."); + String _name_9 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_1.append(_name_9, "\t"); + _builder_1.append("_elems.get(0))));"); + _builder_1.newLineIfNotEmpty(); + _builder_1.append("System.out.println(\"Set "); + String _name_10 = ((MonitoredFunction)fd).getName(); + _builder_1.append(_name_10); + _builder_1.append(" = \" + "); + String _name_11 = ((MonitoredFunction)fd).getName(); + _builder_1.append(_name_11); + _builder_1.append(");"); + sb.append(_builder_1); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } else { + Domain _codomain_2 = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain_2 instanceof AbstractTd)) { + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("this.esecuzione."); + String _name_12 = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name_12); + _builder_2.append(".set("); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("this.esecuzione."); + String _name_13 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_2.append(_name_13); + _builder_2.append("_Class.get("); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("this.esecuzione."); + String _name_14 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_2.append(_name_14); + _builder_2.append("_elemsList.indexOf("); + String _name_15 = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name_15); + _builder_2.append(")));"); + _builder_2.newLineIfNotEmpty(); + _builder_2.append("System.out.println(\"Set "); + String _name_16 = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name_16); + _builder_2.append(" = \" + "); + String _name_17 = ((MonitoredFunction)fd).getName(); + _builder_2.append(_name_17); + _builder_2.append(");"); + sb.append(_builder_2); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } else { + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("this.esecuzione."); + String _name_18 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_18); + _builder_3.append(".set("); + String _name_19 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_19); + _builder_3.append(");"); + _builder_3.newLineIfNotEmpty(); + _builder_3.append("System.out.println(\"Set "); + String _name_20 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_20); + _builder_3.append(" = \" + "); + String _name_21 = ((MonitoredFunction)fd).getName(); + _builder_3.append(_name_21); + _builder_3.append(");"); + sb.append(_builder_3); + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } + } + } + } else { + Domain dd = ((MonitoredFunction)fd).getDomain(); + if ((dd instanceof EnumTd)) { + for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { + { + String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); + Domain _codomain_3 = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain_3 instanceof ConcreteDomain)) { + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append("this.esecuzione."); + String _name_22 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_22); + _builder_4.append(".set("); + _builder_4.newLineIfNotEmpty(); + String _name_23 = asm.getName(); + _builder_4.append(_name_23); + _builder_4.append("."); + String _name_24 = ((EnumTd)dd).getName(); + _builder_4.append(_name_24); + _builder_4.append("."); + _builder_4.append(symbol); + _builder_4.append(","); + _builder_4.newLineIfNotEmpty(); + String _name_25 = asm.getName(); + _builder_4.append(_name_25); + _builder_4.append("."); + String _name_26 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_4.append(_name_26); + _builder_4.append(".valueOf(this.esecuzione."); + String _name_27 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_4.append(_name_27); + _builder_4.append("_elems.get("); + String _name_28 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_28); + _builder_4.append("_"); + _builder_4.append(symbol); + _builder_4.append(")));"); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("System.out.println(\"Set "); + String _name_29 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_29); + _builder_4.append("_"); + _builder_4.append(symbol); + _builder_4.append(" = \" + "); + String _name_30 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_30); + _builder_4.append("_"); + _builder_4.append(symbol); + _builder_4.append(");"); + sb.append(_builder_4); + } else { + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("this.esecuzione."); + String _name_31 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_31); + _builder_5.append(".set("); + _builder_5.newLineIfNotEmpty(); + String _name_32 = asm.getName(); + _builder_5.append(_name_32); + _builder_5.append("."); + String _name_33 = ((EnumTd)dd).getName(); + _builder_5.append(_name_33); + _builder_5.append("."); + _builder_5.append(symbol); + _builder_5.append(", "); + String _name_34 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_34); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append(");"); + sb.append(_builder_5); + } + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } + } + } else { + Domain _domain_1 = ((MonitoredFunction)fd).getDomain(); + if ((_domain_1 instanceof AbstractTd)) { + EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); + for (final Function sf : _function_1) { + if ((sf instanceof StaticFunction)) { + if ((((StaticFunction)sf).getCodomain().equals(((MonitoredFunction)fd).getDomain()) && (((StaticFunction)sf).getDomain() == null))) { + String symbol = ((StaticFunction)sf).getName(); + Domain _codomain_3 = ((MonitoredFunction)fd).getCodomain(); + if ((_codomain_3 instanceof ConcreteDomain)) { + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append("this.esecuzione."); + String _name_22 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_22); + _builder_4.append(".set("); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("this.esecuzione."); + String _name_23 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_4.append(_name_23); + _builder_4.append("_Class.get("); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("this.esecuzione."); + String _name_24 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_4.append(_name_24); + _builder_4.append("_elemsList.indexOf(\""); + _builder_4.append(symbol); + _builder_4.append("\")),"); + _builder_4.newLineIfNotEmpty(); + String _name_25 = asm.getName(); + _builder_4.append(_name_25); + _builder_4.append("."); + String _name_26 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_4.append(_name_26); + _builder_4.append(".valueOf(this.esecuzione."); + String _name_27 = ((MonitoredFunction)fd).getCodomain().getName(); + _builder_4.append(_name_27); + _builder_4.append("_elems.get("); + String _name_28 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_28); + _builder_4.append("_"); + _builder_4.append(symbol); + _builder_4.append(")));"); + _builder_4.newLineIfNotEmpty(); + _builder_4.append("System.out.println(\"Set "); + String _name_29 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_29); + _builder_4.append("_"); + _builder_4.append(symbol); + _builder_4.append(" = \" + "); + String _name_30 = ((MonitoredFunction)fd).getName(); + _builder_4.append(_name_30); + _builder_4.append("_"); + _builder_4.append(symbol); + _builder_4.append(");"); + sb.append(_builder_4); + } else { + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("this.esecuzione."); + String _name_31 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_31); + _builder_5.append(".set("); + _builder_5.newLineIfNotEmpty(); + _builder_5.append("this.esecuzione."); + String _name_32 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_5.append(_name_32); + _builder_5.append("_Class.get("); + _builder_5.newLineIfNotEmpty(); + _builder_5.append("this.esecuzione."); + String _name_33 = ((MonitoredFunction)fd).getDomain().getName(); + _builder_5.append(_name_33); + _builder_5.append("_elemsList.indexOf(\""); + _builder_5.append(symbol); + _builder_5.append("\")),"); + String _name_34 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_34); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append(");"); + _builder_5.newLineIfNotEmpty(); + _builder_5.append("System.out.println(\"Set "); + String _name_35 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_35); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append(" = \" + "); + String _name_36 = ((MonitoredFunction)fd).getName(); + _builder_5.append(_name_36); + _builder_5.append("_"); + _builder_5.append(symbol); + _builder_5.append(");"); + sb.append(_builder_5); + } + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + } + } + } + } + } + } + } + } + return sb.toString(); + } + + public StringBuffer setIsFinalState(final Asm asm, final StringBuffer sb) { + StringBuffer _xifexpression = null; + if (((this.finalStateConditions != null) && (!((List)Conversions.doWrapArray(this.finalStateConditions)).isEmpty()))) { + StringBuffer _xblockexpression = null; + { + sb.append(System.lineSeparator()); + sb.append(System.lineSeparator()); + StringBuffer _append = sb.append("\t"); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("// final state condition"); + _append.append(_builder); + sb.append(System.lineSeparator()); + StringBuffer _append_1 = sb.append("\t"); + StringConcatenation _builder_1 = new StringConcatenation(); + _builder_1.append("public boolean isFinalState(){"); + _append_1.append(_builder_1); + sb.append(System.lineSeparator()); + StringBuffer _append_2 = sb.append("\t\t"); + StringConcatenation _builder_2 = new StringConcatenation(); + _builder_2.append("return"); + _append_2.append(_builder_2); + int numberOfConditionsExpected = 0; + int numberOfConditionsActual = 0; + StringBuffer ss = new StringBuffer(); + for (final String condition : this.finalStateConditions) { + { + int _numberOfConditionsExpected = numberOfConditionsExpected; + numberOfConditionsExpected = (_numberOfConditionsExpected + 1); + final String cond_name = condition.replaceAll("^\\s*(\\w+)\\s*.*$", "$1"); + String cond_value = condition.replaceAll("^\\s*\\w+\\s*(.*)$", "$1"); + boolean _equals = cond_name.toLowerCase().equals("stato"); + if (_equals) { + ss.append(System.lineSeparator()); + StringBuffer _append_3 = ss.append("\t\t\t"); + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("this.stato "); + _builder_3.append(cond_value); + _builder_3.append(" &&"); + _append_3.append(_builder_3); + int _numberOfConditionsActual = numberOfConditionsActual; + numberOfConditionsActual = (_numberOfConditionsActual + 1); + } else { + boolean _matches = cond_value.matches("\\d+"); + boolean _not = (!_matches); + if (_not) { + String cond_value_operators = cond_value.replaceAll("^([><=!]+).*", "$1"); + StringConcatenation _builder_4 = new StringConcatenation(); + String _name = asm.getName(); + _builder_4.append(_name); + _builder_4.append("."); + String _replaceAll = cond_value.replaceAll("^([><=!]+)(.*)", "$2"); + _builder_4.append(_replaceAll); + cond_value = _builder_4.toString(); + cond_value = cond_value_operators.concat(cond_value); + } + EList _function = asm.getHeaderSection().getSignature().getFunction(); + for (final Function fd : _function) { + if (((fd instanceof ControlledFunction) && fd.getName().equals(cond_name))) { + ss.append(System.lineSeparator()); + StringBuffer _append_4 = ss.append("\t\t\t"); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append("this.get_"); + String _name_1 = fd.getName(); + _builder_5.append(_name_1); + _builder_5.append("() "); + _builder_5.append(cond_value); + _builder_5.append(" &&"); + _append_4.append(_builder_5); + int _numberOfConditionsActual_1 = numberOfConditionsActual; + numberOfConditionsActual = (_numberOfConditionsActual_1 + 1); + } + } + } + } + } + if ((numberOfConditionsActual == 0)) { + sb.append(" true;"); + sb.append(System.lineSeparator()); + StringBuffer _append_3 = sb.append("\t"); + StringConcatenation _builder_3 = new StringConcatenation(); + _builder_3.append("// ERROR - NO Conditions found"); + _append_3.append(_builder_3); + } else { + if ((numberOfConditionsActual == numberOfConditionsExpected)) { + sb.append(ss.toString()); + int _length = sb.length(); + int _minus = (_length - 3); + sb.setLength(_minus); + StringConcatenation _builder_4 = new StringConcatenation(); + _builder_4.append(";"); + sb.append(_builder_4); + } else { + sb.append(ss.toString()); + int _length_1 = sb.length(); + int _minus_1 = (_length_1 - 3); + sb.setLength(_minus_1); + StringConcatenation _builder_5 = new StringConcatenation(); + _builder_5.append(";"); + sb.append(_builder_5); + sb.append(System.lineSeparator()); + StringBuffer _append_4 = sb.append("\t"); + StringConcatenation _builder_6 = new StringConcatenation(); + _builder_6.append("// ERROR - "); + _builder_6.append((numberOfConditionsExpected - numberOfConditionsActual)); + _builder_6.append(" Conditions not generated"); + _append_4.append(_builder_6); + } + } + sb.append(System.lineSeparator()); + StringBuffer _append_5 = sb.append("\t"); + StringConcatenation _builder_7 = new StringConcatenation(); + _builder_7.append("}"); + _append_5.append(_builder_7); + _xblockexpression = sb.append(System.lineSeparator()); + } + _xifexpression = _xblockexpression; + } + return _xifexpression; + } +} diff --git a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/JavaASMGenerator2.java b/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/JavaASMGenerator2.java deleted file mode 100644 index e29f58e..0000000 --- a/asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/JavaASMGenerator2.java +++ /dev/null @@ -1,1254 +0,0 @@ -package org.asmeta.asm2java.main; - -import asmeta.definitions.ControlledFunction; -import asmeta.definitions.Function; -import asmeta.definitions.MonitoredFunction; -import asmeta.definitions.RuleDeclaration; -import asmeta.definitions.domains.AbstractTd; -import asmeta.definitions.domains.ConcreteDomain; -import asmeta.definitions.domains.Domain; -import asmeta.definitions.domains.EnumTd; -import asmeta.definitions.domains.MapDomain; -import asmeta.definitions.domains.SequenceDomain; -import asmeta.structure.Asm; -import asmeta.transitionrules.basictransitionrules.Rule; -import java.util.ArrayList; -import java.util.List; -import org.asmeta.asm2java.SeqRuleCollector; -import org.asmeta.asm2java.ToString; -import org.eclipse.emf.common.util.EList; -import org.eclipse.xtend2.lib.StringConcatenation; -import org.eclipse.xtext.xbase.lib.Conversions; -import org.junit.Assert; - -@SuppressWarnings("all") -public class JavaASMGenerator2 extends AsmToJavaGenerator { - public void compileAndWrite(final Asm asm, final String writerPath, final TranslatorOptions userOptions) { - Assert.assertTrue(writerPath.endsWith(".java")); - this.compileAndWrite(asm, writerPath, "JAVA", userOptions); - } - - private List seqCalledRules; - - private String supp; - - private String[] finalStateConditions; - - public String[] setFinalStateConditions(final String[] finalStateConditions) { - return this.finalStateConditions = finalStateConditions; - } - - @Override - public String compileAsm(final Asm asm) { - boolean _optimizeSeqMacroRule = this.options.getOptimizeSeqMacroRule(); - if (_optimizeSeqMacroRule) { - ArrayList _arrayList = new ArrayList(); - this.seqCalledRules = _arrayList; - EList _ruleDeclaration = asm.getBodySection().getRuleDeclaration(); - for (final RuleDeclaration r : _ruleDeclaration) { - this.seqCalledRules.addAll(new SeqRuleCollector(false).visit(r)); - } - } - final String asmName = asm.getName(); - StringBuffer sb = new StringBuffer(); - StringConcatenation _builder = new StringConcatenation(); - _builder.newLine(); - _builder.append("// "); - _builder.append(asmName); - _builder.append("_ASM.java automatically generated from ASM2CODE"); - _builder.newLineIfNotEmpty(); - _builder.newLine(); - _builder.append("import java.util.Scanner;"); - _builder.newLine(); - _builder.newLine(); - _builder.append("/**"); - _builder.newLine(); - _builder.append("* This class allows you to simulate the behavior of an Abstract State Machine (ASM)"); - _builder.newLine(); - _builder.append("* without asking the user for input values ​​of the monitored functions."); - _builder.newLine(); - _builder.append("*"); - _builder.newLine(); - _builder.append("*

"); - _builder.newLine(); - _builder.append("* It has been optimized to be used with evosuite in order to automatically generate test scenarios."); - _builder.newLine(); - _builder.append("*

"); - _builder.newLine(); - _builder.append("*/"); - _builder.newLine(); - _builder.append("class "); - _builder.append(asmName); - _builder.append("_ASM {"); - _builder.newLineIfNotEmpty(); - _builder.append("\t"); - _builder.newLine(); - _builder.append("\t"); - _builder.append("private final "); - _builder.append(asmName, "\t"); - _builder.append(" esecuzione;"); - _builder.newLineIfNotEmpty(); - _builder.append("\t"); - _builder.append("private int stato;"); - _builder.newLine(); - _builder.append("\t"); - _builder.newLine(); - _builder.append(" "); - _builder.append("/**"); - _builder.newLine(); - _builder.append(" "); - _builder.append("* Constructor of the {@code "); - _builder.append(asmName, " "); - _builder.append("_ASM} class. Creates a private instance of the asm"); - _builder.newLineIfNotEmpty(); - _builder.append(" "); - _builder.append("* {@link "); - _builder.append(asmName, " "); - _builder.append("} and sets the initial state of the state machine to 1."); - _builder.newLineIfNotEmpty(); - _builder.append(" "); - _builder.append("*/"); - _builder.newLine(); - _builder.append("\t"); - _builder.append("public "); - _builder.append(asmName, "\t"); - _builder.append("_ASM(){"); - _builder.newLineIfNotEmpty(); - _builder.append("\t\t"); - _builder.append("this.esecuzione = new "); - _builder.append(asmName, "\t\t"); - _builder.append("();"); - _builder.newLineIfNotEmpty(); - _builder.append("\t\t"); - _builder.append("this.stato = 0;"); - _builder.newLine(); - _builder.append("\t"); - _builder.append("}"); - _builder.newLine(); - _builder.append("\t"); - _builder.newLine(); - _builder.append("\t"); - _builder.append("/** The step function is the only public method of the ASM,"); - _builder.newLine(); - _builder.append("\t"); - _builder.append("* it receives as parameters the values ​​of the monitored functions to be updated "); - _builder.newLine(); - _builder.append("\t"); - _builder.append("* and allows to perform a step of the asm by incrementing the state."); - _builder.newLine(); - _builder.append("\t"); - _builder.append("*/"); - _builder.newLine(); - _builder.append("\t"); - _builder.append("public void step("); - sb.append(_builder); - this.setMonitoredArgs(asm, sb); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("){"); - _builder_1.newLine(); - _builder_1.append("\t\t\t\t"); - _builder_1.append("System.out.println(\"\");"); - _builder_1.newLine(); - _builder_1.append("\t\t\t\t"); - _builder_1.newLine(); - _builder_1.append("\t\t\t\t"); - _builder_1.append("printControlled();"); - _builder_1.newLine(); - _builder_1.append("\t\t\t\t"); - _builder_1.append("setMonitored("); - sb.append(_builder_1); - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if ((fd instanceof MonitoredFunction)) { - Domain _domain = ((MonitoredFunction)fd).getDomain(); - boolean _tripleEquals = (_domain == null); - if (_tripleEquals) { - sb.append(System.lineSeparator()); - StringBuffer _append = sb.append("\t\t\t\t\t"); - StringConcatenation _builder_2 = new StringConcatenation(); - String _name = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name); - _builder_2.append(","); - _append.append(_builder_2); - } else { - } - } - } - int _length = sb.length(); - int _minus = (_length - 1); - sb.setLength(_minus); - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append(");"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("this.esecuzione.updateASM();"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("System.out.println(\"\");"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("System.out.println(\"\\n\");"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("printControlled();"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("/* monitored */"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("coverMonitored();"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("/* controlled */"); - _builder_3.newLine(); - _builder_3.append("\t\t\t\t"); - _builder_3.append("coverControlled();"); - sb.append(_builder_3); - sb.append(System.lineSeparator()); - if (((this.finalStateConditions != null) && (!((List)Conversions.doWrapArray(this.finalStateConditions)).isEmpty()))) { - StringBuffer _append_1 = sb.append("\t\t\t\t"); - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("/* final state condition */"); - _append_1.append(_builder_4); - sb.append(System.lineSeparator()); - StringBuffer _append_2 = sb.append("\t\t\t\t"); - StringConcatenation _builder_5 = new StringConcatenation(); - _builder_5.append("if(isFinalState()){"); - _builder_5.newLine(); - _builder_5.append("\t\t\t\t\t\t"); - _builder_5.append("System.out.println(\"\\n\");"); - _builder_5.newLine(); - _builder_5.append("\t\t\t\t"); - _builder_5.append("}"); - _builder_5.newLine(); - _builder_5.append("\t\t\t\t"); - _builder_5.append("else"); - _append_2.append(_builder_5); - sb.append(System.lineSeparator()); - } - StringBuffer _append_3 = sb.append("\t\t\t\t\t\t"); - StringConcatenation _builder_6 = new StringConcatenation(); - _builder_6.append("stato++;"); - _builder_6.newLine(); - _builder_6.append("\t\t\t\t"); - _builder_6.append("}"); - _append_3.append(_builder_6); - this.setIsFinalState(asm, sb); - sb.append(System.lineSeparator()); - StringBuffer _append_4 = sb.append("\t"); - StringConcatenation _builder_7 = new StringConcatenation(); - _builder_7.append("// Monitored getters"); - _append_4.append(_builder_7); - this.monitoredGetter(asm, sb); - sb.append(System.lineSeparator()); - StringBuffer _append_5 = sb.append("\t\t"); - StringConcatenation _builder_8 = new StringConcatenation(); - _builder_8.append("// Controlled getters"); - _append_5.append(_builder_8); - sb.append(System.lineSeparator()); - this.controlledGetter(asm, sb); - sb.append(System.lineSeparator()); - StringBuffer _append_6 = sb.append("\t"); - StringConcatenation _builder_9 = new StringConcatenation(); - _builder_9.append("// Cover functions"); - _append_6.append(_builder_9); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - StringBuffer _append_7 = sb.append("\t"); - StringConcatenation _builder_10 = new StringConcatenation(); - _builder_10.append("private void coverMonitored(){"); - _append_7.append(_builder_10); - this.coverFunctions(asm, sb, true); - sb.append(System.lineSeparator()); - StringBuffer _append_8 = sb.append("\t"); - StringConcatenation _builder_11 = new StringConcatenation(); - _builder_11.append("}"); - _builder_11.newLine(); - _builder_11.newLine(); - _builder_11.append("\t"); - _builder_11.append("private void coverControlled(){"); - _append_8.append(_builder_11); - this.coverFunctions(asm, sb, false); - sb.append(System.lineSeparator()); - StringBuffer _append_9 = sb.append("\t"); - StringConcatenation _builder_12 = new StringConcatenation(); - _builder_12.append("}"); - _append_9.append(_builder_12); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - this.coverBranches(asm, sb); - StringConcatenation _builder_13 = new StringConcatenation(); - _builder_13.newLine(); - _builder_13.append("\t"); - _builder_13.append("// ASM Methods"); - _builder_13.newLine(); - _builder_13.append("\t"); - _builder_13.newLine(); - _builder_13.append("\t"); - _builder_13.append("private void printControlled() {"); - _builder_13.newLine(); - _builder_13.append("\t"); - _builder_13.newLine(); - _builder_13.append("\t\t"); - String _printControlled = this.printControlled(asm); - _builder_13.append(_printControlled, "\t\t"); - _builder_13.newLineIfNotEmpty(); - _builder_13.append("\t"); - _builder_13.newLine(); - _builder_13.append("\t"); - _builder_13.append("}"); - _builder_13.newLine(); - _builder_13.append("\t"); - _builder_13.newLine(); - _builder_13.append("\t"); - _builder_13.append("private void setMonitored("); - sb.append(_builder_13); - this.setMonitoredArgs(asm, sb); - StringConcatenation _builder_14 = new StringConcatenation(); - _builder_14.append(") {"); - _builder_14.newLine(); - _builder_14.append("\t\t\t\t\t"); - _builder_14.newLine(); - _builder_14.append("\t\t\t\t\t"); - String _setMonitored = this.setMonitored(asm); - _builder_14.append(_setMonitored, "\t\t\t\t\t"); - _builder_14.newLineIfNotEmpty(); - _builder_14.append("\t\t\t\t"); - _builder_14.append("}"); - _builder_14.newLine(); - _builder_14.append("\t\t\t"); - _builder_14.append("}"); - sb.append(_builder_14); - return sb.toString(); - } - - public void coverFunctions(final Asm asm, final StringBuffer sb, final boolean monitored) { - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if (((fd instanceof MonitoredFunction) && (monitored == true))) { - sb.append(System.lineSeparator()); - StringBuffer _append = sb.append("\t\t"); - StringConcatenation _builder = new StringConcatenation(); - _builder.append("cover_"); - String _name = fd.getName(); - _builder.append(_name); - _builder.append("();"); - _append.append(_builder); - } - } - EList _function_1 = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd_1 : _function_1) { - if (((fd_1 instanceof ControlledFunction) && (monitored == false))) { - sb.append(System.lineSeparator()); - StringBuffer _append_1 = sb.append("\t\t"); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("cover_"); - String _name_1 = fd_1.getName(); - _builder_1.append(_name_1); - _builder_1.append("();"); - _append_1.append(_builder_1); - } - } - } - - public void coverBranches(final Asm asm, final StringBuffer sb) { - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if (((fd instanceof MonitoredFunction) || (fd instanceof ControlledFunction))) { - Domain _domain = fd.getDomain(); - boolean _tripleEquals = (_domain == null); - if (_tripleEquals) { - StringBuffer _append = sb.append("\t"); - StringConcatenation _builder = new StringConcatenation(); - _builder.append("private void cover_"); - String _name = fd.getName(); - _builder.append(_name); - _builder.append("(){"); - _append.append(_builder); - Domain _codomain = fd.getCodomain(); - if ((_codomain instanceof EnumTd)) { - sb.append(System.lineSeparator()); - StringBuffer _append_1 = sb.append("\t\t"); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("switch(this.get_"); - String _name_1 = fd.getName(); - _builder_1.append(_name_1); - _builder_1.append("()){"); - _append_1.append(_builder_1); - EList _domain_1 = asm.getHeaderSection().getSignature().getDomain(); - for (final Domain dd : _domain_1) { - boolean _equals = dd.equals(fd.getCodomain()); - if (_equals) { - if ((dd instanceof EnumTd)) { - for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { - { - String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); - sb.append(System.lineSeparator()); - StringBuffer _append_2 = sb.append("\t\t\t"); - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.append("case "); - _builder_2.append(symbol); - _builder_2.append(" :"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("\t\t\t\t\t\t\t"); - _builder_2.append("System.out.println(\"Branch "); - String _name_2 = fd.getCodomain().getName(); - _builder_2.append(_name_2, "\t\t\t\t\t\t\t"); - _builder_2.append(" "); - _builder_2.append(symbol, "\t\t\t\t\t\t\t"); - _builder_2.append(" covered\");"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("\t\t\t\t\t\t\t"); - _builder_2.append("// Branch "); - String _name_3 = fd.getCodomain().getName(); - _builder_2.append(_name_3, "\t\t\t\t\t\t\t"); - _builder_2.append(" "); - _builder_2.append(symbol, "\t\t\t\t\t\t\t"); - _builder_2.append(" covered"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("\t\t\t\t\t\t\t"); - _builder_2.append("break;"); - _append_2.append(_builder_2); - } - } - } - } - } - sb.append(System.lineSeparator()); - sb.append("\t\t\t"); - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.append("}"); - sb.append(_builder_2); - } else { - sb.append(System.lineSeparator()); - StringBuffer _append_2 = sb.append("\t\t"); - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append("this.get_"); - String _name_2 = fd.getName(); - _builder_3.append(_name_2); - _builder_3.append("();"); - _append_2.append(_builder_3); - sb.append(System.lineSeparator()); - StringBuffer _append_3 = sb.append("\t\t"); - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("//1 Branch covered"); - _append_3.append(_builder_4); - } - sb.append(System.lineSeparator()); - StringBuffer _append_4 = sb.append("\t"); - StringConcatenation _builder_5 = new StringConcatenation(); - _builder_5.append("}"); - _append_4.append(_builder_5); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - } else { - EList _domain_2 = asm.getHeaderSection().getSignature().getDomain(); - for (final Domain dd_1 : _domain_2) { - boolean _equals_1 = dd_1.equals(fd.getDomain()); - if (_equals_1) { - if ((dd_1 instanceof EnumTd)) { - StringBuffer _append_5 = sb.append("\t"); - StringConcatenation _builder_6 = new StringConcatenation(); - _builder_6.append("private void cover_"); - String _name_3 = fd.getName(); - _builder_6.append(_name_3); - _builder_6.append("(){"); - _append_5.append(_builder_6); - for (int i = 0; (i < ((EnumTd)dd_1).getElement().size()); i++) { - { - String symbol = new ToString(asm).visit(((EnumTd)dd_1).getElement().get(i)); - sb.append(System.lineSeparator()); - StringBuffer _append_6 = sb.append("\t\t"); - StringConcatenation _builder_7 = new StringConcatenation(); - _builder_7.append("this.get_"); - String _name_4 = fd.getName(); - _builder_7.append(_name_4); - _builder_7.append("_"); - _builder_7.append(symbol); - _builder_7.append("();"); - _append_6.append(_builder_7); - } - } - sb.append(System.lineSeparator()); - StringBuffer _append_6 = sb.append("\t\t"); - StringConcatenation _builder_7 = new StringConcatenation(); - _builder_7.append("// "); - int _size = ((EnumTd)dd_1).getElement().size(); - _builder_7.append(_size); - _builder_7.append(" Branch covered"); - _append_6.append(_builder_7); - sb.append(System.lineSeparator()); - StringBuffer _append_7 = sb.append("\t"); - StringConcatenation _builder_8 = new StringConcatenation(); - _builder_8.append("}"); - _append_7.append(_builder_8); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - } - } - } - } - } - } - } - - public void monitoredGetter(final Asm asm, final StringBuffer sb) { - String asmName = asm.getName(); - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if ((fd instanceof MonitoredFunction)) { - Domain _domain = ((MonitoredFunction)fd).getDomain(); - boolean _tripleEquals = (_domain == null); - if (_tripleEquals) { - if ((((MonitoredFunction)fd).getCodomain().getName().equals("Boolean") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder = new StringConcatenation(); - _builder.newLine(); - _builder.append("\t\t"); - _builder.append("private boolean get_"); - String _name = ((MonitoredFunction)fd).getName(); - _builder.append(_name, "\t\t"); - _builder.append("(){"); - _builder.newLineIfNotEmpty(); - _builder.append("\t\t\t"); - _builder.append("return this.esecuzione."); - String _name_1 = ((MonitoredFunction)fd).getName(); - _builder.append(_name_1, "\t\t\t"); - _builder.append(".get();"); - _builder.newLineIfNotEmpty(); - _builder.append("\t\t"); - _builder.append("}"); - _builder.newLine(); - sb.append(_builder); - } - if ((((MonitoredFunction)fd).getCodomain().getName().equals("Integer") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.newLine(); - _builder_1.append("\t\t"); - _builder_1.append("private int get_"); - String _name_2 = ((MonitoredFunction)fd).getName(); - _builder_1.append(_name_2, "\t\t"); - _builder_1.append("(){"); - _builder_1.newLineIfNotEmpty(); - _builder_1.append("\t\t\t"); - _builder_1.append("return this.esecuzione."); - String _name_3 = ((MonitoredFunction)fd).getName(); - _builder_1.append(_name_3, "\t\t\t"); - _builder_1.append(".get();"); - _builder_1.newLineIfNotEmpty(); - _builder_1.append("\t\t"); - _builder_1.append("}"); - _builder_1.newLine(); - sb.append(_builder_1); - } - if ((((MonitoredFunction)fd).getCodomain().getName().equals("String") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.newLine(); - _builder_2.append("\t\t"); - _builder_2.append("private String get_"); - String _name_4 = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name_4, "\t\t"); - _builder_2.append("(){"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("\t\t\t"); - _builder_2.append("return this.esecuzione."); - String _name_5 = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name_5, "\t\t\t"); - _builder_2.append(".get();"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("\t\t"); - _builder_2.append("}"); - _builder_2.newLine(); - sb.append(_builder_2); - } - if ((((((MonitoredFunction)fd).getCodomain() instanceof EnumTd) || - (((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)) || - (((MonitoredFunction)fd).getCodomain() instanceof AbstractTd))) { - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.newLine(); - _builder_3.append("\t\t"); - _builder_3.append("private "); - _builder_3.append(asmName, "\t\t"); - _builder_3.append("."); - String _name_6 = ((MonitoredFunction)fd).getCodomain().getName(); - _builder_3.append(_name_6, "\t\t"); - _builder_3.append(" get_"); - String _name_7 = ((MonitoredFunction)fd).getName(); - _builder_3.append(_name_7, "\t\t"); - _builder_3.append("(){"); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("\t\t\t"); - _builder_3.append("return this.esecuzione."); - String _name_8 = ((MonitoredFunction)fd).getName(); - _builder_3.append(_name_8, "\t\t\t"); - _builder_3.append(".get();"); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("\t\t"); - _builder_3.append("}"); - _builder_3.newLine(); - sb.append(_builder_3); - } - } - } - } - } - - public void controlledGetter(final Asm asm, final StringBuffer sb) { - String asmName = asm.getName(); - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if ((fd instanceof ControlledFunction)) { - Domain _domain = ((ControlledFunction)fd).getDomain(); - boolean _tripleEquals = (_domain == null); - if (_tripleEquals) { - if ((((ControlledFunction)fd).getCodomain().getName().equals("Boolean") && (!(((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder = new StringConcatenation(); - _builder.newLine(); - _builder.append("\t\t"); - _builder.append("public boolean get_"); - String _name = ((ControlledFunction)fd).getName(); - _builder.append(_name, "\t\t"); - _builder.append("(){"); - _builder.newLineIfNotEmpty(); - _builder.append("\t\t\t"); - _builder.append("return this.esecuzione."); - String _name_1 = ((ControlledFunction)fd).getName(); - _builder.append(_name_1, "\t\t\t"); - _builder.append(".get();"); - _builder.newLineIfNotEmpty(); - _builder.append("\t\t"); - _builder.append("}"); - _builder.newLine(); - sb.append(_builder); - } - if ((((ControlledFunction)fd).getCodomain().getName().equals("Integer") && (!(((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.newLine(); - _builder_1.append("\t\t"); - _builder_1.append("public int get_"); - String _name_2 = ((ControlledFunction)fd).getName(); - _builder_1.append(_name_2, "\t\t"); - _builder_1.append("(){"); - _builder_1.newLineIfNotEmpty(); - _builder_1.append("\t\t\t"); - _builder_1.append("return this.esecuzione."); - String _name_3 = ((ControlledFunction)fd).getName(); - _builder_1.append(_name_3, "\t\t\t"); - _builder_1.append(".get();"); - _builder_1.newLineIfNotEmpty(); - _builder_1.append("\t\t"); - _builder_1.append("}"); - _builder_1.newLine(); - sb.append(_builder_1); - } - if ((((ControlledFunction)fd).getCodomain().getName().equals("String") && (!(((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.newLine(); - _builder_2.append("\t\t"); - _builder_2.append("public String get_"); - String _name_4 = ((ControlledFunction)fd).getName(); - _builder_2.append(_name_4, "\t\t"); - _builder_2.append("(){"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("\t\t\t"); - _builder_2.append("return this.esecuzione."); - String _name_5 = ((ControlledFunction)fd).getName(); - _builder_2.append(_name_5, "\t\t\t"); - _builder_2.append(".get();"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("\t\t"); - _builder_2.append("}"); - _builder_2.newLine(); - sb.append(_builder_2); - } - if ((((((ControlledFunction)fd).getCodomain() instanceof EnumTd) || - (((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain)) || - (((ControlledFunction)fd).getCodomain() instanceof AbstractTd))) { - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.newLine(); - _builder_3.append("\t\t"); - _builder_3.append("public "); - _builder_3.append(asmName, "\t\t"); - _builder_3.append("."); - String _name_6 = ((ControlledFunction)fd).getCodomain().getName(); - _builder_3.append(_name_6, "\t\t"); - _builder_3.append(" get_"); - String _name_7 = ((ControlledFunction)fd).getName(); - _builder_3.append(_name_7, "\t\t"); - _builder_3.append("(){"); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("\t\t\t"); - _builder_3.append("return this.esecuzione."); - String _name_8 = ((ControlledFunction)fd).getName(); - _builder_3.append(_name_8, "\t\t\t"); - _builder_3.append(".get();"); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("\t\t"); - _builder_3.append("}"); - _builder_3.newLine(); - sb.append(_builder_3); - } - } else { - EList _domain_1 = asm.getHeaderSection().getSignature().getDomain(); - for (final Domain dd : _domain_1) { - boolean _equals = dd.equals(((ControlledFunction)fd).getDomain()); - if (_equals) { - if ((dd instanceof EnumTd)) { - for (int i = 0; (i < ((EnumTd)dd).getElement().size()); i++) { - { - String symbol = new ToString(asm).visit(((EnumTd)dd).getElement().get(i)); - sb.append(System.lineSeparator()); - Domain _codomain = ((ControlledFunction)fd).getCodomain(); - if ((_codomain instanceof ConcreteDomain)) { - StringBuffer _append = sb.append("\t"); - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("public int get_"); - String _name_9 = ((ControlledFunction)fd).getName(); - _builder_4.append(_name_9); - _builder_4.append("_"); - _builder_4.append(symbol); - _builder_4.append("(){"); - _append.append(_builder_4); - sb.append(System.lineSeparator()); - StringBuffer _append_1 = sb.append("\t\t"); - StringConcatenation _builder_5 = new StringConcatenation(); - _builder_5.append("return this.esecuzione."); - String _name_10 = ((ControlledFunction)fd).getName(); - _builder_5.append(_name_10); - _builder_5.append(".oldValues.get("); - _append_1.append(_builder_5); - sb.append(System.lineSeparator()); - StringBuffer _append_2 = sb.append("\t\t\t"); - StringConcatenation _builder_6 = new StringConcatenation(); - _builder_6.append("this.esecuzione."); - String _name_11 = ((ControlledFunction)fd).getDomain().getName(); - _builder_6.append(_name_11); - _builder_6.append("_elemsList.get("); - _builder_6.append(i); - _builder_6.append(")).value;"); - _append_2.append(_builder_6); - sb.append(System.lineSeparator()); - StringBuffer _append_3 = sb.append("\t"); - StringConcatenation _builder_7 = new StringConcatenation(); - _builder_7.append("}"); - _append_3.append(_builder_7); - } else { - StringBuffer _append_4 = sb.append("\t"); - StringConcatenation _builder_8 = new StringConcatenation(); - _builder_8.append("public "); - _builder_8.append(asmName); - _builder_8.append("."); - String _name_12 = ((ControlledFunction)fd).getCodomain().getName(); - _builder_8.append(_name_12); - _builder_8.append(" get_"); - String _name_13 = ((ControlledFunction)fd).getName(); - _builder_8.append(_name_13); - _builder_8.append("_"); - _builder_8.append(symbol); - _builder_8.append("(){"); - _append_4.append(_builder_8); - sb.append(System.lineSeparator()); - StringBuffer _append_5 = sb.append("\t\t"); - StringConcatenation _builder_9 = new StringConcatenation(); - _builder_9.append("return this.esecuzione."); - String _name_14 = ((ControlledFunction)fd).getName(); - _builder_9.append(_name_14); - _builder_9.append(".oldValues.get("); - _append_5.append(_builder_9); - sb.append(System.lineSeparator()); - StringBuffer _append_6 = sb.append("\t\t\t"); - StringConcatenation _builder_10 = new StringConcatenation(); - _builder_10.append("this.esecuzione."); - String _name_15 = ((ControlledFunction)fd).getDomain().getName(); - _builder_10.append(_name_15); - _builder_10.append("_elemsList.get("); - _builder_10.append(i); - _builder_10.append("));"); - _append_6.append(_builder_10); - sb.append(System.lineSeparator()); - StringBuffer _append_7 = sb.append("\t"); - StringConcatenation _builder_11 = new StringConcatenation(); - _builder_11.append("}"); - _append_7.append(_builder_11); - } - sb.append(System.lineSeparator()); - } - } - } - } - } - } - } - } - } - - public String printControlled(final Asm asm) { - StringBuffer sb = new StringBuffer(); - EList _domain = asm.getHeaderSection().getSignature().getDomain(); - for (final Domain dd : _domain) { - if ((dd instanceof AbstractTd)) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("System.out.print(\""); - String _name = ((AbstractTd)dd).getName(); - _builder.append(_name); - _builder.append("\"+ \" = {\");"); - _builder.newLineIfNotEmpty(); - _builder.append("for(int i=0 ; i< esecuzione."); - String _name_1 = ((AbstractTd)dd).getName(); - _builder.append(_name_1); - _builder.append("_elemsList.size(); i++)"); - _builder.newLineIfNotEmpty(); - _builder.append("\t"); - _builder.append("if(i!= esecuzione."); - String _name_2 = ((AbstractTd)dd).getName(); - _builder.append(_name_2, "\t"); - _builder.append("_elemsList.size()-1)"); - _builder.newLineIfNotEmpty(); - _builder.append("\t\t"); - _builder.append("System.out.print(esecuzione."); - String _name_3 = ((AbstractTd)dd).getName(); - _builder.append(_name_3, "\t\t"); - _builder.append("_elemsList.get(i) +\", \");"); - _builder.newLineIfNotEmpty(); - _builder.append("\t"); - _builder.append("else"); - _builder.newLine(); - _builder.append("\t\t"); - _builder.append("System.out.print(esecuzione."); - String _name_4 = ((AbstractTd)dd).getName(); - _builder.append(_name_4, "\t\t"); - _builder.append("_elemsList.get(i));\t"); - _builder.newLineIfNotEmpty(); - _builder.append("System.out.println(\"}\");"); - _builder.newLine(); - sb.append(_builder); - } - } - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if ((fd instanceof ControlledFunction)) { - Domain _domain_1 = ((ControlledFunction)fd).getDomain(); - boolean _tripleEquals = (_domain_1 == null); - if (_tripleEquals) { - Domain _codomain = ((ControlledFunction)fd).getCodomain(); - if ((_codomain instanceof ConcreteDomain)) { - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("System.out.println(\""); - String _name_5 = ((ControlledFunction)fd).getName(); - _builder_1.append(_name_5); - _builder_1.append(" = \" + esecuzione."); - String _name_6 = ((ControlledFunction)fd).getName(); - _builder_1.append(_name_6); - _builder_1.append(".get().value);"); - _builder_1.newLineIfNotEmpty(); - sb.append(_builder_1); - } - if (((((ControlledFunction)fd).getCodomain().getName().equals("Integer") || ((ControlledFunction)fd).getCodomain().getName().equals("Boolean")) || - ((ControlledFunction)fd).getCodomain().getName().equals("String"))) { - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.append("System.out.println(\""); - String _name_7 = ((ControlledFunction)fd).getName(); - _builder_2.append(_name_7); - _builder_2.append(" = \" + esecuzione."); - String _name_8 = ((ControlledFunction)fd).getName(); - _builder_2.append(_name_8); - _builder_2.append(".get());"); - _builder_2.newLineIfNotEmpty(); - sb.append(_builder_2); - } - Domain _codomain_1 = ((ControlledFunction)fd).getCodomain(); - if ((_codomain_1 instanceof MapDomain)) { - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append("System.out.println(\""); - String _name_9 = ((ControlledFunction)fd).getName(); - _builder_3.append(_name_9); - _builder_3.append(" = \" + esecuzione."); - String _name_10 = ((ControlledFunction)fd).getName(); - _builder_3.append(_name_10); - _builder_3.append(".get());"); - _builder_3.newLineIfNotEmpty(); - sb.append(_builder_3); - } - Domain _codomain_2 = ((ControlledFunction)fd).getCodomain(); - if ((_codomain_2 instanceof SequenceDomain)) { - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("System.out.println(\""); - String _name_11 = ((ControlledFunction)fd).getName(); - _builder_4.append(_name_11); - _builder_4.append(" = \" + esecuzione."); - String _name_12 = ((ControlledFunction)fd).getName(); - _builder_4.append(_name_12); - _builder_4.append(".get());"); - _builder_4.newLineIfNotEmpty(); - sb.append(_builder_4); - } - Domain _codomain_3 = ((ControlledFunction)fd).getCodomain(); - if ((_codomain_3 instanceof EnumTd)) { - StringConcatenation _builder_5 = new StringConcatenation(); - _builder_5.append("System.out.println(\""); - String _name_13 = ((ControlledFunction)fd).getName(); - _builder_5.append(_name_13); - _builder_5.append(" = \" + esecuzione."); - String _name_14 = ((ControlledFunction)fd).getName(); - _builder_5.append(_name_14); - _builder_5.append(".oldValue.name());"); - _builder_5.newLineIfNotEmpty(); - sb.append(_builder_5); - } - } else { - if (((((ControlledFunction)fd).getDomain() instanceof EnumTd) && (((ControlledFunction)fd).getCodomain() instanceof ConcreteDomain))) { - StringConcatenation _builder_6 = new StringConcatenation(); - _builder_6.append("for(int i=0; i < esecuzione."); - String _name_15 = ((ControlledFunction)fd).getDomain().getName(); - _builder_6.append(_name_15); - _builder_6.append("_elemsList.size(); i++){"); - _builder_6.newLineIfNotEmpty(); - _builder_6.append("\t"); - _builder_6.append("System.out.println(\" "); - String _name_16 = ((ControlledFunction)fd).getName(); - _builder_6.append(_name_16, "\t"); - _builder_6.append(" => (\" + esecuzione."); - String _name_17 = ((ControlledFunction)fd).getDomain().getName(); - _builder_6.append(_name_17, "\t"); - _builder_6.append("_elemsList.get(i) + "); - _builder_6.newLineIfNotEmpty(); - _builder_6.append("\t"); - _builder_6.append("\") = \" + esecuzione."); - String _name_18 = ((ControlledFunction)fd).getName(); - _builder_6.append(_name_18, "\t"); - _builder_6.append(".oldValues.get(esecuzione."); - String _name_19 = ((ControlledFunction)fd).getDomain().getName(); - _builder_6.append(_name_19, "\t"); - _builder_6.append("_elemsList.get(i)).value);"); - _builder_6.newLineIfNotEmpty(); - _builder_6.append("}"); - _builder_6.newLine(); - sb.append(_builder_6); - } - if (((((ControlledFunction)fd).getDomain() instanceof EnumTd) && (((ControlledFunction)fd).getCodomain() instanceof EnumTd))) { - StringConcatenation _builder_7 = new StringConcatenation(); - _builder_7.append("for(int i=0; i < esecuzione."); - String _name_20 = ((ControlledFunction)fd).getDomain().getName(); - _builder_7.append(_name_20); - _builder_7.append("_elemsList.size(); i++){"); - _builder_7.newLineIfNotEmpty(); - _builder_7.append("\t"); - _builder_7.append("System.out.println(\""); - String _name_21 = ((ControlledFunction)fd).getName(); - _builder_7.append(_name_21, "\t"); - _builder_7.append(" => (\" + esecuzione."); - String _name_22 = ((ControlledFunction)fd).getDomain().getName(); - _builder_7.append(_name_22, "\t"); - _builder_7.append("_elemsList.get(i) + "); - _builder_7.newLineIfNotEmpty(); - _builder_7.append("\t"); - _builder_7.append("\") = \"+ esecuzione."); - String _name_23 = ((ControlledFunction)fd).getName(); - _builder_7.append(_name_23, "\t"); - _builder_7.append(".oldValues.get(esecuzione."); - String _name_24 = ((ControlledFunction)fd).getDomain().getName(); - _builder_7.append(_name_24, "\t"); - _builder_7.append("_elemsList.get(i)));"); - _builder_7.newLineIfNotEmpty(); - _builder_7.append("}"); - _builder_7.newLine(); - sb.append(_builder_7); - } - } - } - } - return sb.toString(); - } - - public void setMonitoredArgs(final Asm asm, final StringBuffer sb) { - final String asmName = asm.getName(); - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if ((fd instanceof MonitoredFunction)) { - Domain _domain = ((MonitoredFunction)fd).getDomain(); - boolean _tripleEquals = (_domain == null); - if (_tripleEquals) { - if ((((MonitoredFunction)fd).getCodomain().getName().equals("Boolean") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - sb.append(System.lineSeparator()).append("\t\t"); - StringConcatenation _builder = new StringConcatenation(); - _builder.append("boolean "); - String _name = ((MonitoredFunction)fd).getName(); - _builder.append(_name); - _builder.append(","); - sb.append(_builder); - } else { - if ((((MonitoredFunction)fd).getCodomain().getName().equals("Integer") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - sb.append(System.lineSeparator()).append("\t\t"); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("int "); - String _name_1 = ((MonitoredFunction)fd).getName(); - _builder_1.append(_name_1); - _builder_1.append(","); - sb.append(_builder_1); - } else { - Domain _codomain = ((MonitoredFunction)fd).getCodomain(); - if ((_codomain instanceof EnumTd)) { - sb.append(System.lineSeparator()).append("\t\t"); - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.append(asmName); - _builder_2.append("."); - String _name_2 = ((MonitoredFunction)fd).getCodomain().getName(); - _builder_2.append(_name_2); - _builder_2.append(" "); - String _name_3 = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name_3); - _builder_2.append(","); - sb.append(_builder_2); - } else { - Domain _codomain_1 = ((MonitoredFunction)fd).getCodomain(); - if ((_codomain_1 instanceof ConcreteDomain)) { - sb.append(System.lineSeparator()).append("\t\t"); - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append("int "); - String _name_4 = ((MonitoredFunction)fd).getName(); - _builder_3.append(_name_4); - _builder_3.append(","); - sb.append(_builder_3); - } else { - Domain _codomain_2 = ((MonitoredFunction)fd).getCodomain(); - if ((_codomain_2 instanceof AbstractTd)) { - sb.append(System.lineSeparator()).append("\t\t"); - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("int "); - String _name_5 = ((MonitoredFunction)fd).getName(); - _builder_4.append(_name_5); - _builder_4.append(","); - sb.append(_builder_4); - } - } - } - } - } - } else { - } - } - } - int _length = sb.length(); - int _minus = (_length - 1); - sb.setLength(_minus); - } - - public String setMonitored(final Asm asm) { - StringBuffer sb = new StringBuffer(); - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if ((fd instanceof MonitoredFunction)) { - Domain _domain = ((MonitoredFunction)fd).getDomain(); - boolean _tripleEquals = (_domain == null); - if (_tripleEquals) { - if ((((MonitoredFunction)fd).getCodomain().getName().equals("Boolean") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder = new StringConcatenation(); - _builder.append("this.esecuzione."); - String _name = ((MonitoredFunction)fd).getName(); - _builder.append(_name); - _builder.append(".set("); - String _name_1 = ((MonitoredFunction)fd).getName(); - _builder.append(_name_1); - _builder.append(");"); - _builder.newLineIfNotEmpty(); - _builder.append("System.out.println(\"Set "); - String _name_2 = ((MonitoredFunction)fd).getName(); - _builder.append(_name_2); - _builder.append(" = \" + "); - String _name_3 = ((MonitoredFunction)fd).getName(); - _builder.append(_name_3); - _builder.append(");"); - sb.append(_builder); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - } - if ((((MonitoredFunction)fd).getCodomain().getName().equals("Integer") && (!(((MonitoredFunction)fd).getCodomain() instanceof ConcreteDomain)))) { - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("this.esecuzione."); - String _name_4 = ((MonitoredFunction)fd).getName(); - _builder_1.append(_name_4); - _builder_1.append(".set("); - String _name_5 = ((MonitoredFunction)fd).getName(); - _builder_1.append(_name_5); - _builder_1.append(");"); - _builder_1.newLineIfNotEmpty(); - _builder_1.append("System.out.println(\"Set "); - String _name_6 = ((MonitoredFunction)fd).getName(); - _builder_1.append(_name_6); - _builder_1.append(" = \" + "); - String _name_7 = ((MonitoredFunction)fd).getName(); - _builder_1.append(_name_7); - _builder_1.append(");"); - sb.append(_builder_1); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - } - Domain _codomain = ((MonitoredFunction)fd).getCodomain(); - if ((_codomain instanceof EnumTd)) { - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.append("this.esecuzione."); - String _name_8 = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name_8); - _builder_2.append(".set("); - String _name_9 = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name_9); - _builder_2.append(");"); - _builder_2.newLineIfNotEmpty(); - _builder_2.append("System.out.println(\"Set "); - String _name_10 = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name_10); - _builder_2.append(" = \" + "); - String _name_11 = ((MonitoredFunction)fd).getName(); - _builder_2.append(_name_11); - _builder_2.append(");"); - sb.append(_builder_2); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - } - Domain _codomain_1 = ((MonitoredFunction)fd).getCodomain(); - if ((_codomain_1 instanceof ConcreteDomain)) { - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append("this.esecuzione."); - String _name_12 = ((MonitoredFunction)fd).getName(); - _builder_3.append(_name_12); - _builder_3.append(".set("); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("\t"); - String _name_13 = asm.getName(); - _builder_3.append(_name_13, "\t"); - _builder_3.append("."); - String _name_14 = ((MonitoredFunction)fd).getCodomain().getName(); - _builder_3.append(_name_14, "\t"); - _builder_3.append(".valueOf("); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("\t"); - _builder_3.append("this.esecuzione."); - String _name_15 = ((MonitoredFunction)fd).getCodomain().getName(); - _builder_3.append(_name_15, "\t"); - _builder_3.append("_elems.get("); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("\t"); - String _name_16 = ((MonitoredFunction)fd).getName(); - _builder_3.append(_name_16, "\t"); - _builder_3.append(" - this.esecuzione."); - String _name_17 = ((MonitoredFunction)fd).getCodomain().getName(); - _builder_3.append(_name_17, "\t"); - _builder_3.append("_elems.get(0))));"); - _builder_3.newLineIfNotEmpty(); - _builder_3.append("System.out.println(\"Set "); - String _name_18 = ((MonitoredFunction)fd).getName(); - _builder_3.append(_name_18); - _builder_3.append(" = \" + "); - String _name_19 = ((MonitoredFunction)fd).getName(); - _builder_3.append(_name_19); - _builder_3.append(");"); - sb.append(_builder_3); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - } - Domain _codomain_2 = ((MonitoredFunction)fd).getCodomain(); - if ((_codomain_2 instanceof AbstractTd)) { - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("this.esecuzione."); - String _name_20 = ((MonitoredFunction)fd).getName(); - _builder_4.append(_name_20); - _builder_4.append(".set(this.esecuzione."); - String _name_21 = ((MonitoredFunction)fd).getCodomain().getName(); - _builder_4.append(_name_21); - _builder_4.append("_Class.get("); - String _name_22 = ((MonitoredFunction)fd).getName(); - _builder_4.append(_name_22); - _builder_4.append("));"); - _builder_4.newLineIfNotEmpty(); - _builder_4.append("System.out.println(\"Set "); - String _name_23 = ((MonitoredFunction)fd).getName(); - _builder_4.append(_name_23); - _builder_4.append(" = \" + "); - String _name_24 = ((MonitoredFunction)fd).getName(); - _builder_4.append(_name_24); - _builder_4.append(");"); - sb.append(_builder_4); - sb.append(System.lineSeparator()); - sb.append(System.lineSeparator()); - } - } else { - } - } - } - return sb.toString(); - } - - public StringBuffer setIsFinalState(final Asm asm, final StringBuffer sb) { - StringBuffer _xifexpression = null; - if (((this.finalStateConditions != null) && (!((List)Conversions.doWrapArray(this.finalStateConditions)).isEmpty()))) { - StringBuffer _xblockexpression = null; - { - sb.append(System.lineSeparator()); - StringBuffer _append = sb.append("\t"); - StringConcatenation _builder = new StringConcatenation(); - _builder.append("// final state condition"); - _append.append(_builder); - sb.append(System.lineSeparator()); - StringBuffer _append_1 = sb.append("\t"); - StringConcatenation _builder_1 = new StringConcatenation(); - _builder_1.append("public boolean isFinalState(){"); - _append_1.append(_builder_1); - sb.append(System.lineSeparator()); - StringBuffer _append_2 = sb.append("\t\t"); - StringConcatenation _builder_2 = new StringConcatenation(); - _builder_2.append("return"); - _append_2.append(_builder_2); - for (final String condition : this.finalStateConditions) { - { - final String cond_name = condition.replaceAll("^\\s*(\\w+)\\s*.*$", "$1"); - final String cond_value = condition.replaceAll("^\\s*\\w+\\s*(.*)$", "$1"); - boolean _equals = cond_name.toLowerCase().equals("stato"); - if (_equals) { - sb.append(System.lineSeparator()); - StringBuffer _append_3 = sb.append("\t\t\t"); - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append("this.stato "); - _builder_3.append(cond_value); - _builder_3.append(" &&"); - _append_3.append(_builder_3); - } else { - EList _function = asm.getHeaderSection().getSignature().getFunction(); - for (final Function fd : _function) { - if (((fd instanceof ControlledFunction) && fd.getName().equals(cond_name))) { - sb.append(System.lineSeparator()); - StringBuffer _append_4 = sb.append("\t\t\t"); - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("this.get_"); - String _name = fd.getName(); - _builder_4.append(_name); - _builder_4.append("() "); - _builder_4.append(cond_value); - _builder_4.append(" &&"); - _append_4.append(_builder_4); - } - } - } - } - } - int _length = sb.length(); - int _minus = (_length - 3); - sb.setLength(_minus); - StringConcatenation _builder_3 = new StringConcatenation(); - _builder_3.append(";"); - sb.append(_builder_3); - sb.append(System.lineSeparator()); - StringBuffer _append_3 = sb.append("\t"); - StringConcatenation _builder_4 = new StringConcatenation(); - _builder_4.append("}"); - _xblockexpression = _append_3.append(_builder_4); - } - _xifexpression = _xblockexpression; - } - return _xifexpression; - } -}