diff options
Diffstat (limited to 'verigraph/service/src/tests/j-verigraph-generator/test_generator.py')
| -rw-r--r-- | verigraph/service/src/tests/j-verigraph-generator/test_generator.py | 160 |
1 files changed, 160 insertions, 0 deletions
diff --git a/verigraph/service/src/tests/j-verigraph-generator/test_generator.py b/verigraph/service/src/tests/j-verigraph-generator/test_generator.py new file mode 100644 index 0000000..f4629bb --- /dev/null +++ b/verigraph/service/src/tests/j-verigraph-generator/test_generator.py @@ -0,0 +1,160 @@ +#!/usr/bin/python + +############################################################################## +# Copyright (c) 2017 Politecnico di Torino and others. +# +# All rights reserved. This program and the accompanying materials +# are made available under the terms of the Apache License, Version 2.0 +# which accompanies this distribution, and is available at +# http://www.apache.org/licenses/LICENSE-2.0 +############################################################################## + +from pprint import pprint +from code_generator import CodeGeneratorBackend +import sys, getopt +import contextlib +import os +from utility import * +import logging + +def main(argv): + if len(argv) < 8: + print 'test_generator.py -i <inputfile> -o <outputfile> -s <source> -d <destination>' + sys.exit(2) + #initialize command line arguments values + inputfile = '' + outputfile = '' + source = '' + destination = '' + #parse command line arguments and exit if there is an error + try: + opts, args = getopt.getopt(argv,"hi:o:s:d:",["ifile=","ofile=","source=","destination="]) + except getopt.GetoptError: + print 'test_generator.py -i <inputfile> -o <outputfile> -s <source> -d <destination>' + sys.exit(2) + for opt, arg in opts: + if opt == '-h': + print 'test_generator.py -i <inputfile> -o <outputfile> -s <source> -d <destination>' + sys.exit() + elif opt in ("-i", "--ifile"): + inputfile = arg + elif opt in ("-o", "--ofile"): + outputfile = arg + elif opt in ("-s", "--source"): + source = arg + elif opt in ("-d", "--destination"): + destination = arg + #set logging + logging.basicConfig(stream=sys.stderr, level=logging.INFO) + #capitalize ouput filename + dirname = os.path.dirname(outputfile) + basename = os.path.basename(outputfile) + basename = os.path.splitext(basename)[0] + basename = basename[0].upper() + basename[1:] + + #print arguments + logging.debug('Input file is', inputfile) + logging.debug('Output file is', dirname + "/" + basename) + logging.debug('Source node is', source) + logging.debug('Destination node is', destination) + + #begin file generation + with smart_open(dirname + "/" + basename + ".java") as f: + c = CodeGeneratorBackend() + c.begin(tab=" ") + c.writeln("package tests;") + c.writeln("import java.util.Calendar;") + c.writeln("import java.util.Date;") + c.writeln("import java.util.HashMap;") + + c.writeln("import com.microsoft.z3.Context;") + c.writeln("import com.microsoft.z3.FuncDecl;") + c.writeln("import com.microsoft.z3.Model;") + c.writeln("import com.microsoft.z3.Status;") + c.writeln("import com.microsoft.z3.Z3Exception;") + c.writeln("import mcnet.components.IsolationResult;") + + + inputfile = os.path.basename(inputfile) + c.writeln("import tests.scenarios." + os.path.splitext(inputfile)[0] + ";") + c.writeln("public class " + basename + "{") + + c.indent() + c.writeln("Context ctx;") + + c.write("public void resetZ3() throws Z3Exception{\n\ + HashMap<String, String> cfg = new HashMap<String, String>();\n\ + cfg.put(\"model\", \"true\");\n\ + ctx = new Context(cfg);\n\ + \r\t}\n") + + c.write("public void printVector (Object[] array){\n\ + int i=0;\n\ + System.out.println( \"*** Printing vector ***\");\n\ + for (Object a : array){\n\ + i+=1;\n\ + System.out.println( \"#\"+i);\n\ + System.out.println(a);\n\ + System.out.println( \"*** \"+ i+ \" elements printed! ***\");\n\ + }\n\ + \r\t}\n") + + c.write("public void printModel (Model model) throws Z3Exception{\n\ + for (FuncDecl d : model.getFuncDecls()){\n\ + System.out.println(d.getName() +\" = \"+ d.toString());\n\ + System.out.println(\"\");\n\ + }\n\ + \r\t}\n") + + c.writeln("public int run() throws Z3Exception{") + c.indent() + + c.writeln(basename + " p = new " + basename + "();") + + #adding time estimation + #c.writeln("int k = 0;") + #c.writeln("long t = 0;") + + #c.writeln("for(;k<1;k++){") + #c.indent() + + c.writeln("p.resetZ3();") + + c.write(os.path.splitext(inputfile)[0] + " model = new " + os.path.splitext(inputfile)[0] + "(p.ctx);\n") + + #c.writeln("Calendar cal = Calendar.getInstance();") + #c.writeln("Date start_time = cal.getTime();") + + c.write("IsolationResult ret =model.check.checkIsolationProperty(model.") + c.append(source + ", model." + destination + ");\n") + #c.writeln("Calendar cal2 = Calendar.getInstance();") + #c.writeln("t = t+(cal2.getTime().getTime() - start_time.getTime());") + + c.writeln("if (ret.result == Status.UNSATISFIABLE){\n\ + System.out.println(\"UNSAT\");\n\ + return -1;\n\ + }else if (ret.result == Status.SATISFIABLE){\n\ + System.out.println(\"SAT\");\n\ + return 0;\n\ + }else{\n\ + System.out.println(\"UNKNOWN\");\n\ + return -2;\n\ + \r\t\t}") + + #c.dedent() + #c.writeln("}") + + #c.writeln("") + #c.writeln("System.out.printf(\"Mean execution time " + source + " -> " + destination + ": %.16f\", ((float) t/(float)1000)/k);") + + c.dedent() + c.writeln("}") + + c.dedent() + c.writeln("}") + + print >>f, c.end() + logging.debug("File " + os.path.abspath(dirname + "/" + basename + ".java") + " has been successfully generated!!") + +if __name__ == "__main__": + main(sys.argv[1:]) |