Skip to content

Commit 2cf5fda

Browse files
isaacmaffeisisaacmaffeis
authored
Merge pull request #17 from isaacmaffeis/isaac
fixed elemsList issue and added support for Domain -> Codomain functions fixed condition logic bug
2 parents 92bbb7b + f036cde commit 2cf5fda

11 files changed

+441
-124
lines changed

‎asmetal2java_codegen/src/org/asmeta/asm2java/DomainToJavaSigDef.xtend

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,10 @@ class DomainToJavaSigDef extends ReflectiveVisitor<String> {
145145
sb.append('''«new ToString(res).visit(object.element.get(i))»}
146146
''')
147147
}
148-
148+
149+
sb.append(System.lineSeparator)
150+
sb.append('''
151+
List<«object.name»> «object.name»_elemsList = new ArrayList<>();''')
149152
return sb.toString
150153
}
151154

‎asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaASMGenerator2.xtend

Lines changed: 100 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ import asmeta.definitions.domains.MapDomain
1313
import asmeta.definitions.domains.SequenceDomain
1414
import asmeta.definitions.domains.EnumTd
1515
import asmeta.definitions.MonitoredFunction
16+
import org.asmeta.asm2java.ToString
1617

1718
class JavaASMGenerator2 extends AsmToJavaGenerator {
1819

@@ -118,8 +119,8 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
118119
coverControlled();''');
119120

120121
sb.append(System.lineSeparator)
121-
if(finalStateConditions !== null || !finalStateConditions.isEmpty){
122-
sb.append("\t\t\t\t" ).append('''/*final state condition */''')
122+
if(finalStateConditions !== null && !finalStateConditions.isEmpty){
123+
sb.append("\t\t\t\t" ).append('''/* final state condition */''')
123124
sb.append(System.lineSeparator)
124125
sb.append("\t\t\t\t" ).append('''if(isFinalState()){
125126
System.out.println("\n<Stato finale>");
@@ -141,7 +142,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
141142
sb.append("\t\t").append('''// Controlled getters''');
142143
sb.append(System.lineSeparator)
143144

144-
controllerGetter(asm,sb);
145+
controlledGetter(asm,sb);
145146

146147
sb.append(System.lineSeparator)
147148
sb.append("\t").append('''// Cover functions''');
@@ -211,34 +212,74 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
211212
def coverBranches(Asm asm, StringBuffer sb) {
212213
for (fd : asm.headerSection.signature.function){
213214
if(fd instanceof MonitoredFunction || fd instanceof ControlledFunction){
214-
sb.append("\t").append('''private void cover_«fd.name»(){''');
215-
if(fd.codomain instanceof EnumTd){
216-
sb.append(System.lineSeparator)
217-
sb.append("\t\t").append('''switch(this.get_«fd.name»()){''');
218-
var codomainContents = fd.codomain.eContents;
219-
for(enumerativeLog: codomainContents){
220-
val startIndex = enumerativeLog.toString().indexOf("symbol: ") + "symbol: ".length
221-
val endIndex = enumerativeLog.toString().indexOf(")", startIndex)
222-
val symbol = enumerativeLog.toString().substring(startIndex, endIndex)
215+
if(fd.domain === null){
216+
sb.append("\t").append('''private void cover_«fd.name»(){''');
217+
if(fd.codomain instanceof EnumTd){
218+
sb.append(System.lineSeparator)
219+
sb.append("\t\t").append('''switch(this.get_«fd.name»()){''');
220+
/* metodo più rapido ma meno consistente
221+
var codomainContents = fd.codomain.eContents;
222+
for(enumerativeLog: codomainContents){
223+
val startIndex = enumerativeLog.toString().indexOf("symbol: ") + "symbol: ".length
224+
val endIndex = enumerativeLog.toString().indexOf(")", startIndex)
225+
val symbol = enumerativeLog.toString().substring(startIndex, endIndex)
226+
sb.append(System.lineSeparator)
227+
sb.append("\t\t\t").append('''case «symbol» :
228+
System.out.println("Branch «fd.codomain.name» «symbol» covered");
229+
// Branch «fd.codomain.name» «symbol» covered
230+
break;''');
231+
}
232+
*/
233+
/*Metodo normale */
234+
for(dd : asm.headerSection.signature.domain){
235+
if(dd.equals(fd.codomain)){
236+
if(dd instanceof EnumTd){
237+
for (var int i = 0; i < dd.element.size; i++) {
238+
var symbol = new ToString(asm).visit(dd.element.get(i))
239+
sb.append(System.lineSeparator)
240+
sb.append("\t\t\t").append('''case «symbol» :
241+
System.out.println("Branch «fd.codomain.name» «symbol» covered");
242+
// Branch «fd.codomain.name» «symbol» covered
243+
break;''');
244+
}
245+
}
246+
}
247+
}
248+
/* */
249+
sb.append(System.lineSeparator)
250+
sb.append("\t\t\t")sb.append('''}''');
251+
}
252+
else{
253+
sb.append(System.lineSeparator)
254+
sb.append("\t\t").append('''this.get_«fd.name»();''');
223255
sb.append(System.lineSeparator)
224-
sb.append("\t\t\t").append('''case «symbol» :
225-
System.out.println("Branch «fd.codomain.name» «symbol» covered");
226-
// Branch «fd.codomain.name» «symbol» covered
227-
break;''');
256+
sb.append("\t\t").append('''//1 Branch covered''');
228257
}
229258
sb.append(System.lineSeparator)
230-
sb.append("\t\t\t")sb.append('''}''');
231-
}
232-
else{
259+
sb.append("\t").append('''}''');
233260
sb.append(System.lineSeparator)
234-
sb.append("\t\t").append('''this.get_«fd.name»();''');
235261
sb.append(System.lineSeparator)
236-
sb.append("\t\t").append('''//1 Branch covered''');
237262
}
238-
sb.append(System.lineSeparator)
239-
sb.append("\t").append('''}''');
240-
sb.append(System.lineSeparator)
241-
sb.append(System.lineSeparator)
263+
else{ // fd.domain != null
264+
for(dd : asm.headerSection.signature.domain){
265+
if(dd.equals(fd.domain)){
266+
if(dd instanceof EnumTd){
267+
sb.append("\t").append('''private void cover_«fd.name»(){''');
268+
for (var int i = 0; i < dd.element.size; i++) {
269+
var symbol = new ToString(asm).visit(dd.element.get(i))
270+
sb.append(System.lineSeparator)
271+
sb.append("\t\t").append('''this.get_«fd.name»_«symbol»();''');
272+
}
273+
sb.append(System.lineSeparator)
274+
sb.append("\t\t").append('''// «dd.element.size» Branch covered''');
275+
sb.append(System.lineSeparator)
276+
sb.append("\t").append('''}''');
277+
sb.append(System.lineSeparator)
278+
sb.append(System.lineSeparator)
279+
}
280+
}
281+
}
282+
}
242283
}
243284
}
244285
}
@@ -287,7 +328,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
287328
}
288329
}
289330

290-
def controllerGetter(Asm asm, StringBuffer sb) {
331+
def controlledGetter(Asm asm, StringBuffer sb) {
291332
var asmName = asm.name;
292333
for (fd : asm.headerSection.signature.function) {
293334
if (fd instanceof ControlledFunction) {
@@ -327,6 +368,38 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
327368
''');
328369
}
329370
}
371+
else{ // TODO: Da sistemare i getter per le funzioni con Dominio -> Codominio
372+
373+
for(dd : asm.headerSection.signature.domain){
374+
if(dd.equals(fd.domain)){
375+
if(dd instanceof EnumTd){
376+
for (var int i = 0; i < dd.element.size; i++) {
377+
var symbol = new ToString(asm).visit(dd.element.get(i))
378+
sb.append(System.lineSeparator)
379+
if(fd.codomain instanceof ConcreteDomain){ // considero subsetOf Integer
380+
sb.append("\t").append('''public int get_«fd.name»_«symbol»(){''');
381+
sb.append(System.lineSeparator)
382+
sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get(''');
383+
sb.append(System.lineSeparator)
384+
sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»)).value;''');
385+
sb.append(System.lineSeparator)
386+
sb.append("\t").append('''}''');
387+
}
388+
else{
389+
sb.append("\t").append('''public «asmName».«fd.codomain.name» get_«fd.name»_«symbol»(){''');
390+
sb.append(System.lineSeparator)
391+
sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get(''');
392+
sb.append(System.lineSeparator)
393+
sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»));''');
394+
sb.append(System.lineSeparator)
395+
sb.append("\t").append('''}''');
396+
}
397+
sb.append(System.lineSeparator)
398+
}
399+
}
400+
}
401+
}
402+
}
330403
}
331404
}
332405
}
@@ -532,7 +605,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
532605
}
533606

534607
def setIsFinalState(Asm asm, StringBuffer sb){
535-
if(finalStateConditions !== null || !finalStateConditions.isEmpty){
608+
if(finalStateConditions !== null && !finalStateConditions.isEmpty){
536609
sb.append(System.lineSeparator)
537610
sb.append("\t").append('''// final state condition''')
538611
sb.append(System.lineSeparator)

‎asmetal2java_codegen/src/org/asmeta/asm2java/main/JavaGenerator.xtend

Lines changed: 36 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ import org.asmeta.asm2java.RuleToJava
1717
import org.asmeta.asm2java.SeqRuleCollector
1818
import org.asmeta.asm2java.Util
1919
import org.junit.Assert
20+
import asmeta.definitions.domains.EnumTd
21+
import org.asmeta.asm2java.ToString
2022

2123
/**Generates .cpp ASM file */
2224
class JavaGenerator extends AsmToJavaGenerator {
@@ -47,6 +49,7 @@ class JavaGenerator extends AsmToJavaGenerator {
4749
functionSignature(asm)
4850
// TODO fix include list
4951
return '''
52+
5053
// «asmName».java automatically generated from ASM2CODE
5154
5255
import java.util.ArrayList;
@@ -173,9 +176,10 @@ class JavaGenerator extends AsmToJavaGenerator {
173176

174177
«asmName»(){
175178

176-
//Definizione iniziale dei domini statici
179+
//Definizione iniziale dei domini statici
177180

178181
«initialStaticDomainDefinition(asm)»
182+
«initialStaticEnumDomainDefinition(asm)»
179183

180184
//Definizione iniziale dei domini dinamici
181185

@@ -329,6 +333,37 @@ class JavaGenerator extends AsmToJavaGenerator {
329333
else
330334
return ""
331335
}
336+
337+
// Metodo per inizializzare gli array _elemsList associati ai domini enumerativi
338+
def initialStaticEnumDomainDefinition(Asm asm) {
339+
340+
var StringBuffer initial = new StringBuffer
341+
342+
if (asm.bodySection !== null && asm.bodySection.domainDefinition !== null) {
343+
for (dd : asm.headerSection.signature.domain) {
344+
if(dd instanceof EnumTd){
345+
initial.append(
346+
dd.name + "_elemsList = Collections.unmodifiableList(Arrays.asList(")
347+
348+
for (var int i = 0; i < dd.element.size; i++) {
349+
350+
if (i != dd.element.size - 1)
351+
initial.append('''«dd.name».«new ToString(asm).visit(dd.element.get(i))», ''')
352+
else
353+
initial.append('''«dd.name».«new ToString(asm).visit(dd.element.get(i))»)''')
354+
}
355+
356+
initial.append(");\n")
357+
}
358+
}
359+
}
360+
361+
if (initial.toString.length != 0)
362+
return initial.toString + "\n"
363+
else
364+
return ""
365+
}
366+
332367

333368
// Metodo per settare i valori dei domini definiti Dynamic nel signature
334369
// Da controllarne l'uso: Dynamic domains must be initialized, not defined!

‎asmetal2java_codegen/src/org/asmeta/asm2java/main/MainClass.java

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -43,13 +43,13 @@ public class MainClass {
4343

4444
// the generator for the code
4545
static private JavaGenerator jGenerator = new JavaGenerator();
46-
//static private JavaExeGenerator jGeneratorExe = new JavaExeGenerator();
46+
static private JavaExeGenerator jGeneratorExe = new JavaExeGenerator();
4747
static private JavaASMGenerator2 jGeneratorASM = new JavaASMGenerator2();
4848

4949

5050
// default translator options
5151
private static TranslatorOptions translatorOptions =
52-
new TranslatorOptions(false, true, true);
52+
new TranslatorOptions(false, false, false);
5353

5454
/**
5555
* Generates Java code from an ASM specification.
@@ -87,24 +87,24 @@ public static CompileResult generate(
8787
//File javaFile = new File(SRC_GEN + File.separator + name + ".java");
8888
File javaFile = new File(dir.getPath() + File.separator + name + ".java");
8989
File javaFileCompilazione = new File(dirCompilazione + File.separator + name + ".java");
90-
//File javaFileExe = new File(dirEsecuzione + File.separator + name + "_Exe.java");
91-
//File javaFileExeN = new File(dirEsecuzione + File.separator + name + ".java");
90+
File javaFileExe = new File(dirEsecuzione + File.separator + name + "_Exe.java");
91+
File javaFileExeN = new File(dirEsecuzione + File.separator + name + ".java");
9292
File javaFileASM = new File(dirEsecuzione + File.separator + name + "_ASM.java");
9393
File javaFileASMN = new File(dirEsecuzione + File.separator + name + ".java");
9494

9595
File javaFileT = new File(dirTraduzione + File.separator + name + ".java");
96-
//File javaFileExeT = new File(dirTraduzione + File.separator + name + "_Exe.java");
96+
File javaFileExeT = new File(dirTraduzione + File.separator + name + "_Exe.java");
9797
File javaFileASMT = new File(dirTraduzione + File.separator + name + "_ASM.java");
9898

9999
deleteExisting(javaFile);
100100
deleteExisting(javaFileCompilazione);
101-
//deleteExisting(javaFileExe);
102-
//deleteExisting(javaFileExeN);
101+
deleteExisting(javaFileExe);
102+
deleteExisting(javaFileExeN);
103103
deleteExisting(javaFileASM);
104104
deleteExisting(javaFileASMN);
105105
deleteExisting(javaFileASMT);
106106
deleteExisting(javaFileT);
107-
//deleteExisting(javaFileExeT);
107+
deleteExisting(javaFileExeT);
108108

109109
System.out.println("\n\n===" + name + " ===================");
110110

@@ -117,9 +117,9 @@ public static CompileResult generate(
117117
userOptions);
118118

119119
// EXE Class
120-
//jGeneratorExe.compileAndWrite(model.getMain(), javaFileExe.getCanonicalPath(), userOptions);
121-
//jGenerator.compileAndWrite(model.getMain(), javaFileExeN.getCanonicalPath(), userOptions);
122-
//jGeneratorExe.compileAndWrite(model.getMain(), javaFileExeT.getCanonicalPath(), userOptions);
120+
jGeneratorExe.compileAndWrite(model.getMain(), javaFileExe.getCanonicalPath(), userOptions);
121+
jGenerator.compileAndWrite(model.getMain(), javaFileExeN.getCanonicalPath(), userOptions);
122+
jGeneratorExe.compileAndWrite(model.getMain(), javaFileExeT.getCanonicalPath(), userOptions);
123123

124124
// ASM Class
125125
jGeneratorASM.setFinalStateConditions(finalStateConditions);
@@ -134,15 +134,15 @@ public static CompileResult generate(
134134

135135
System.out.println("Generated java file: " + javaFile.getCanonicalPath());
136136
System.out.println("Generated java file: " + javaFileCompilazione.getCanonicalPath());
137-
//System.out.println("Generated java file: " + javaFileExeN.getCanonicalPath());
137+
System.out.println("Generated java file: " + javaFileExeN.getCanonicalPath());
138138
System.out.println("Generated ASM java file: " + javaFileASMN.getCanonicalPath());
139139

140-
//System.out.println("Generated java file for the execution: " + javaFileExe.getCanonicalPath());
140+
System.out.println("Generated java file for the execution: " + javaFileExe.getCanonicalPath());
141141

142142
System.out.println("All java files Generated in: " + javaFileT.getCanonicalPath());
143143

144144
exportFile(javaFile, outputFolder);
145-
//exportFile(javaFileExe, outputFolder);
145+
exportFile(javaFileExe, outputFolder);
146146
exportFile(javaFileASM, outputFolder);
147147

148148

‎asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/.DomainToJavaSigDef.xtendbin

192 Bytes
Binary file not shown.

‎asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/DomainToJavaSigDef.java

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -234,6 +234,16 @@ public String visit(final EnumTd object) {
234234
sb.append(_builder_2);
235235
}
236236
}
237+
sb.append(System.lineSeparator());
238+
StringConcatenation _builder_1 = new StringConcatenation();
239+
_builder_1.append("List<");
240+
String _name_1 = object.getName();
241+
_builder_1.append(_name_1);
242+
_builder_1.append("> ");
243+
String _name_2 = object.getName();
244+
_builder_1.append(_name_2);
245+
_builder_1.append("_elemsList = new ArrayList<>();");
246+
sb.append(_builder_1);
237247
return sb.toString();
238248
}
239249

‎asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.java._trace

12.2 KB
Binary file not shown.

‎asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaASMGenerator2.xtendbin

1.14 KB
Binary file not shown.

‎asmetal2java_codegen/xtend-gen/org/asmeta/asm2java/main/.JavaGenerator.xtendbin

670 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)