Skip to content

Commit 442e03b

Browse files
isaacmaffeisisaacmaffeis
committed
added getter for domain -> codomain functions
1 parent 37de172 commit 442e03b

File tree

5 files changed

+587
-236
lines changed

5 files changed

+587
-236
lines changed

‎asmetal2java_codegen/examples/ATM3.asm

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -230,4 +230,4 @@ default init s0:
230230
case card2 : 1652
231231
case card3 : 548
232232
endswitch
233-
function accessible($c in NumCard) = true
233+
function accessible($c in NumCard) = true

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

Lines changed: 129 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ import asmeta.definitions.domains.SequenceDomain
1414
import asmeta.definitions.domains.EnumTd
1515
import asmeta.definitions.MonitoredFunction
1616
import org.asmeta.asm2java.ToString
17+
import asmeta.definitions.StaticFunction
1718

1819
class JavaASMGenerator2 extends AsmToJavaGenerator {
1920

@@ -276,6 +277,21 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
276277
sb.append(System.lineSeparator)
277278
sb.append(System.lineSeparator)
278279
}
280+
else if (dd instanceof AbstractTd) {
281+
var i = 0
282+
for (sf : asm.headerSection.signature.function) { // controllo le funzioni statiche e prendo quelle che aggiungono al dominio astratto
283+
if(sf instanceof StaticFunction){
284+
if(sf.codomain.equals(dd)){
285+
i+=1
286+
var symbol = sf.name
287+
sb.append(System.lineSeparator)
288+
sb.append("\t\t").append('''this.get_«fd.name»_«symbol»();''');
289+
}
290+
}
291+
}
292+
sb.append(System.lineSeparator)
293+
sb.append("\t\t").append('''//«i» Branch covered''');
294+
}
279295
else {
280296
sb.append(System.lineSeparator)
281297
sb.append("\t\t").append('''this.get_«fd.name»();''');
@@ -407,9 +423,19 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
407423
sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.get(«i»)).value;''');
408424
sb.append(System.lineSeparator)
409425
sb.append("\t").append('''}''');
410-
}
411-
else{
412-
sb.append("\t").append('''public «asmName».«fd.codomain.name» get_«fd.name»_«symbol»(){''');
426+
} else{
427+
if (fd.codomain.name.equals("Integer")){
428+
sb.append("\t").append('''public int get_«fd.name»_«symbol»(){''');
429+
}
430+
else if (fd.codomain.name.equals("Boolean")){
431+
sb.append("\t").append('''public boolean get_«fd.name»_«symbol»(){''');
432+
}
433+
else if (fd.codomain.name.equals("String")){
434+
sb.append("\t").append('''public String get_«fd.name»_«symbol»(){''');
435+
}
436+
else{
437+
sb.append("\t").append('''public «asmName».«fd.codomain.name» get_«fd.name»_«symbol»(){''');
438+
}
413439
sb.append(System.lineSeparator)
414440
sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get(''');
415441
sb.append(System.lineSeparator)
@@ -420,6 +446,49 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
420446
sb.append(System.lineSeparator)
421447
}
422448
}
449+
else if(dd instanceof AbstractTd){
450+
for (sf : asm.headerSection.signature.function) { // controllo le funzioni statiche e prendo quelle che aggiungono al dominio astratto
451+
if(sf instanceof StaticFunction){
452+
if(sf.codomain.equals(dd)){
453+
var symbol = sf.name
454+
sb.append(System.lineSeparator)
455+
if(fd.codomain instanceof ConcreteDomain){
456+
sb.append("\t").append('''public int get_«fd.name»_«symbol»(){''');
457+
sb.append(System.lineSeparator)
458+
sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get(''');
459+
sb.append(System.lineSeparator)
460+
sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get(''');
461+
sb.append(System.lineSeparator)
462+
sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")).value);''');
463+
sb.append(System.lineSeparator)
464+
sb.append("\t").append('''}''');
465+
} else{
466+
if (fd.codomain.name.equals("Integer")){
467+
sb.append("\t").append('''public int get_«fd.name»_«symbol»(){''');
468+
}
469+
else if (fd.codomain.name.equals("Boolean")){
470+
sb.append("\t").append('''public boolean get_«fd.name»_«symbol»(){''');
471+
}
472+
else if (fd.codomain.name.equals("String")){
473+
sb.append("\t").append('''public Srting get_«fd.name»_«symbol»(){''');
474+
}
475+
else{
476+
sb.append("\t").append('''public «fd.codomain.name» get_«fd.name»_«symbol»(){''');
477+
}
478+
sb.append(System.lineSeparator)
479+
sb.append("\t\t").append('''return this.esecuzione.«fd.name».oldValues.get(''');
480+
sb.append(System.lineSeparator)
481+
sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_Class.get(''');
482+
sb.append(System.lineSeparator)
483+
sb.append("\t\t\t").append('''this.esecuzione.«fd.domain.name»_elemsList.indexOf("«symbol»")));''');
484+
sb.append(System.lineSeparator)
485+
sb.append("\t").append('''}''');
486+
}
487+
sb.append(System.lineSeparator)
488+
}
489+
}
490+
}
491+
}
423492
}
424493
}
425494
}
@@ -515,6 +584,10 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
515584
sb.append(System.lineSeparator()).append("\t\t")
516585
sb.append('''int «fd.name»,''')
517586
}
587+
else if (fd.codomain.name.equals("String") && !(fd.codomain instanceof ConcreteDomain)) {
588+
sb.append(System.lineSeparator()).append("\t\t")
589+
sb.append('''String «fd.name»,''')
590+
}
518591
else if (fd.codomain instanceof EnumTd) {
519592
sb.append(System.lineSeparator()).append("\t\t")
520593
sb.append('''«asmName».«fd.codomain.name» «fd.name»,''')
@@ -525,7 +598,7 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
525598
}
526599
else if (fd.codomain instanceof AbstractTd) {
527600
sb.append(System.lineSeparator()).append("\t\t")
528-
sb.append('''int «fd.name»,''')
601+
sb.append('''String «fd.name»,''')
529602
}
530603
}
531604
else {
@@ -552,32 +625,15 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
552625
if (fd instanceof MonitoredFunction) {
553626
// Solo se il dominio » nullo, quindi funzioni che ricadono nella struttura zero<Valore>
554627
if (fd.domain === null) {
555-
// Caso relativo alle variabili booleane non concrete
556-
if (fd.codomain.name.equals("Boolean") && !(fd.codomain instanceof ConcreteDomain)) {
557-
sb.append('''
558-
this.esecuzione.«fd.name».set(«fd.name»);
559-
System.out.println("Set «fd.name» = " + «fd.name»);''')
560-
sb.append(System.lineSeparator)
561-
sb.append(System.lineSeparator)
562-
}
563-
564-
if (fd.codomain.name.equals("Integer") && !(fd.codomain instanceof ConcreteDomain)) {
565-
sb.append('''
566-
this.esecuzione.«fd.name».set(«fd.name»);
567-
System.out.println("Set «fd.name» = " + «fd.name»);''')
568-
sb.append(System.lineSeparator)
569-
sb.append(System.lineSeparator)
570-
}
571-
628+
572629
if (fd.codomain instanceof EnumTd) {
573630
sb.append('''
574631
this.esecuzione.«fd.name».set(«fd.name»);
575632
System.out.println("Set «fd.name» = " + «fd.name»);''')
576633
sb.append(System.lineSeparator)
577634
sb.append(System.lineSeparator)
578635
}
579-
580-
if (fd.codomain instanceof ConcreteDomain) {
636+
else if (fd.codomain instanceof ConcreteDomain) {
581637
sb.append('''
582638
this.esecuzione.«fd.name».set(
583639
«asm.name».«fd.codomain.name».valueOf(
@@ -587,14 +643,22 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
587643
sb.append(System.lineSeparator)
588644
sb.append(System.lineSeparator)
589645
}
590-
591-
if (fd.codomain instanceof AbstractTd) {
646+
else if (fd.codomain instanceof AbstractTd) {
592647
sb.append('''
593-
this.esecuzione.«fd.name».set(this.esecuzione.«fd.codomain.name»_Class.get(«fd.name»));
648+
this.esecuzione.«fd.name».set(
649+
this.esecuzione.«fd.codomain.name»_Class.get(
650+
this.esecuzione.«fd.codomain.name»_elemsList.indexOf(«fd.name»)));
594651
System.out.println("Set «fd.name» = " + «fd.name»);''')
595652
sb.append(System.lineSeparator)
596653
sb.append(System.lineSeparator)
597654
}
655+
else{
656+
sb.append('''
657+
this.esecuzione.«fd.name».set(«fd.name»);
658+
System.out.println("Set «fd.name» = " + «fd.name»);''')
659+
sb.append(System.lineSeparator)
660+
sb.append(System.lineSeparator)
661+
}
598662

599663
} else {
600664
/* TODO: fix the index i
@@ -630,33 +694,60 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
630694

631695
def setIsFinalState(Asm asm, StringBuffer sb){
632696
if(finalStateConditions !== null && !finalStateConditions.isEmpty){
697+
sb.append(System.lineSeparator)
633698
sb.append(System.lineSeparator)
634699
sb.append("\t").append('''// final state condition''')
635700
sb.append(System.lineSeparator)
636701
sb.append("\t").append('''public boolean isFinalState(){''')
637702
sb.append(System.lineSeparator)
638703
sb.append("\t\t").append('''return''')
704+
var numberOfConditionsExpected = 0
705+
var numberOfConditionsActual = 0
706+
var ss = new StringBuffer;
639707
for(condition : finalStateConditions){
640-
708+
numberOfConditionsExpected += 1
641709
val cond_name = condition.replaceAll("^\\s*(\\w+)\\s*.*$", "$1")
642-
val cond_value = condition.replaceAll("^\\s*\\w+\\s*(.*)$", "$1")
643-
710+
var cond_value = condition.replaceAll("^\\s*\\w+\\s*(.*)$", "$1")
711+
644712
if(cond_name.toLowerCase.equals("stato")){
645-
sb.append(System.lineSeparator)
646-
sb.append("\t\t\t").append('''this.stato «cond_value» &&''')
647-
}
648-
else{
649-
for(fd : asm.headerSection.signature.function)
713+
ss.append(System.lineSeparator)
714+
ss.append("\t\t\t").append('''this.stato «cond_value» &&''')
715+
numberOfConditionsActual +=1
716+
} else {
717+
if(!cond_value.matches("\\d+")){ // se la condizione non è numerica
718+
var cond_value_operators = cond_value.replaceAll("^([><=!]+).*", "$1");
719+
cond_value = '''«asm.name».«cond_value.replaceAll("^([><=!]+)(.*)","$2")»''' ; // aggiungo il prefisso
720+
cond_value = cond_value_operators.concat(cond_value)
721+
}
722+
for(fd : asm.headerSection.signature.function){
650723
if(fd instanceof ControlledFunction && fd.name.equals(cond_name)){
651-
sb.append(System.lineSeparator)
652-
sb.append("\t\t\t").append('''this.get_«fd.name»() «cond_value» &&''')
724+
ss.append(System.lineSeparator)
725+
ss.append("\t\t\t").append('''this.get_«fd.name»() «cond_value» &&''')
726+
numberOfConditionsActual +=1
653727
}
654728
}
729+
}
730+
}
731+
if(numberOfConditionsActual == 0){
732+
sb.append(" true;")
733+
sb.append(System.lineSeparator)
734+
sb.append("\t").append('''// ERROR - NO Conditions found''')
735+
}
736+
else if(numberOfConditionsActual == numberOfConditionsExpected){
737+
sb.append(ss.toString)
738+
sb.setLength(sb.length() - 3)
739+
sb.append(''';''')
740+
}
741+
else{
742+
sb.append(ss.toString)
743+
sb.setLength(sb.length() - 3)
744+
sb.append(''';''')
745+
sb.append(System.lineSeparator)
746+
sb.append("\t").append('''// ERROR - «numberOfConditionsExpected-numberOfConditionsActual» Conditions not generated''')
655747
}
656-
sb.setLength(sb.length() - 3)
657-
sb.append(''';''')
658748
sb.append(System.lineSeparator)
659749
sb.append("\t").append('''}''')
750+
sb.append(System.lineSeparator)
660751
}
661752
}
662753

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

19.2 KB
Binary file not shown.

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

1.89 KB
Binary file not shown.

0 commit comments

Comments
 (0)