Merge pull request #10 from isaacmaffeis/isaac

updated ASM generator: added final state condition and fixed bugs

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

@@ -27,6 +27,12 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
 
 	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) {
@@ -109,13 +115,25 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
 				/* monitored */
 				coverMonitored();
 				/* controlled */
-				coverControlled();
+				coverControlled();''');
 
-				stato++;
-		}
-			
-		// Monitored getters
-			''');
+			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<Stato finale>");
+				}
+				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);
 
@@ -464,8 +482,10 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
 
 					if (fd.codomain instanceof ConcreteDomain) {
 						sb.append('''
-						this.esecuzione.«fd.name»_supporto.value = «fd.name»;
-						this.esecuzione.«fd.name».set(this.esecuzione.«fd.name»_supporto);
+						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)
@@ -511,4 +531,36 @@ class JavaASMGenerator2 extends AsmToJavaGenerator {
 		return sb.toString
 	}
 
+	def setIsFinalState(Asm asm, StringBuffer sb){
+		if(finalStateConditions !== null || !finalStateConditions.isEmpty){
+			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''')
+			for(condition : finalStateConditions){
+
+				val cond_name = condition.replaceAll("^\\s*(\\w+)\\s*.*$", "$1")
+				val 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)
+						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» &&''')
+						}
+					}
+			}
+			sb.setLength(sb.length() - 3)
+			sb.append(''';''')
+			sb.append(System.lineSeparator)
+			sb.append("\t").append('''}''')
+		}
+	}
+
 }

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

@@ -7,8 +7,10 @@
 import java.io.OutputStream;
 import java.nio.file.Files;
 import java.nio.file.NoSuchFileException;
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashSet;
+import java.util.List;
 import java.util.Properties;
 import java.util.Set;
 
@@ -61,7 +63,8 @@ public class MainClass {
 	public static CompileResult generate(
       String asmspec,
 			TranslatorOptions userOptions,
-			String outputFolder)
+			String outputFolder,
+			String[] finalStateConditions)
 			throws Exception {
 		//
 		// PARSE THE SPECIFICATION
@@ -80,7 +83,6 @@ public static CompileResult generate(
 		String dirEsecuzione = asmFile.getParentFile().getPath() + "/esecuzione";
 		String dirTraduzione = asmFile.getParentFile().getPath() + "/Traduzione";
 
-
 		// AC
 		//File javaFile = new File(SRC_GEN + File.separator + name + ".java");
     File javaFile = new File(dir.getPath() + File.separator + name + ".java");
@@ -94,7 +96,6 @@ public static CompileResult generate(
 		//File javaFileExeT = new File(dirTraduzione + File.separator + name + "_Exe.java");
 		File javaFileASMT = new File(dirTraduzione + File.separator + name + "_ASM.java");
 
-
 		deleteExisting(javaFile);
 		deleteExisting(javaFileCompilazione);
 		//deleteExisting(javaFileExe);
@@ -109,19 +110,23 @@ public static CompileResult generate(
 
 		// write java
 		try {
+			// Java Class
 		  jGenerator.compileAndWrite(model.getMain(), javaFile.getCanonicalPath(), userOptions);
 		  jGenerator.compileAndWrite(model.getMain(),
 					javaFileCompilazione.getCanonicalPath(),
 					userOptions);
+
+			// EXE Class
 			//jGeneratorExe.compileAndWrite(model.getMain(), javaFileExe.getCanonicalPath(), userOptions);
 			//jGenerator.compileAndWrite(model.getMain(), javaFileExeN.getCanonicalPath(), userOptions);
 		  //jGeneratorExe.compileAndWrite(model.getMain(), javaFileExeT.getCanonicalPath(), userOptions);
 
+			// ASM Class
+			jGeneratorASM.setFinalStateConditions(finalStateConditions);
 			jGeneratorASM.compileAndWrite(model.getMain(), javaFileASM.getCanonicalPath(), userOptions);
 			jGenerator.compileAndWrite(model.getMain(), javaFileASMN.getCanonicalPath(), userOptions);
 			jGeneratorASM.compileAndWrite(model.getMain(), javaFileASMT.getCanonicalPath(), userOptions);
 
-
 		} catch (Exception e) {
 			e.printStackTrace();
 			return new CompileResult(false, e.getMessage());
@@ -216,6 +221,19 @@ public static Options getCommandLineOptions() {
 				.hasArg(true)
 				.desc("The output folder (optional, defaults to `./output/`)")
 				.build();
+
+		// final state condition (Only for ASM scenario generator)
+		Option finalState = Option.builder("finalState")
+				.argName("finalState")
+				.type(String.class)
+				.hasArg(true)
+				.desc("Final state condition:\n"
+						+ "(for ASM scenario generation only)\n"
+						+ "Allows you to specify the final state condition,\n"
+						+ " in order to help automatic scenario generation.\n"
+						+ "Add the conditions separated by ':'\n"
+						+ "example: state>=5:total>=50")
+				.build();
 
 		// property
 		Option property = Option.builder("D")
@@ -235,6 +253,7 @@ public static Options getCommandLineOptions() {
 		options.addOption(help);
 		options.addOption(input);
 		options.addOption(output);
+		options.addOption(finalState);
 		options.addOption(property);
 
 		return options;
@@ -310,9 +329,18 @@ private void execute (CommandLine line, Options options) {
 		} else {
 			outputFolder = line.getOptionValue("output");
 		}
+
+		String[] finalStateConditions = null;
+		if(line.hasOption("finalState")){
+			finalStateConditions = line.getOptionValue("finalState").split(":");
+		}
 
 		try {
-			CompileResult compileResult = generate(asmspec, translatorOptions, outputFolder);
+			CompileResult compileResult = generate(
+					asmspec,
+					translatorOptions,
+					outputFolder,
+					finalStateConditions);
 			if(compileResult.getSuccess()){
 				logger.info("Generation succeed : " + compileResult.toString());
 			}