From 606f6965f3ccec837aa216cbb3f56fdcf943a59b Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 11 Oct 2019 15:51:49 -0400 Subject: VAMPIRE: complete testing setup --- .../dslreasoner/vampire/icse/GeneralTest.xtend | 59 ------ .../dslreasoner/vampire/icse/YakinduTest.xtend | 214 +++++++++++++-------- 2 files changed, 132 insertions(+), 141 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src') diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend index 5225fb89..26ed10e3 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.xtend @@ -26,65 +26,6 @@ import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl import org.eclipse.viatra.query.runtime.api.IQueryGroup class GeneralTest { - val static USER_AGENT = "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36" - - def static void main(String[] args) { - val form = makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300) - -// val x =sendPost("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\ntester -// -//\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n -// -//------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___Paradox---4.0\"\r\n\r\nParadox---4.0\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___Paradox---4.0\"\r\n\r\nparadox --no-progress --time %d --tstp --model %s\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--") - val x = sendPost(form) - print(x.toString) - } - - def static makeForm(String formula, String solver, String cmd, int time) { - return header + addSpec(formula) + addOptions + addSolver(solver, cmd.replace("%d", time.toString)) + addEnd - } - - def static sendPost(String formData ) throws Exception { - - val OkHttpClient client = new OkHttpClient() - - val MediaType mediaType = MediaType.parse( - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA") - val RequestBody body = RequestBody.create(mediaType, formData) - val Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body). - addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", - "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", - "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"). - addHeader("Accept", - "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3"). - addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", - "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", - "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", - "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build() - - val Response response = client.newCall(request).execute() -// TimeUnit.SECONDS.sleep(5) -// return newArrayList( response.body.string.split("\n")) -return response.body.string - - // case 1: - } - def static getHeader() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n" - } - def static addSpec(String spec) { - return spec.replace("\n", "\r\n") - } - def static addOptions() { - return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n" - } - def static addSolver(String ID, String cmd) { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID + "\"\r\n\r\n" + ID + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___" + ID + "\"\r\n\r\n" + cmd + "\r\n" - } - def static addEnd() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--" - } def static Map getTypeMap(Map classMap, EcoreMetamodelDescriptor metamodel, Ecore2Logic e2l, Ecore2Logic_Trace trace) { diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index c35b200e..9121367b 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend @@ -1,6 +1,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement @@ -11,6 +12,8 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration @@ -32,10 +35,11 @@ class YakinduTest { // Workspace setup val Date date = new Date(System.currentTimeMillis) - val SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); + val SimpleDateFormat format = new SimpleDateFormat("dd-HHmm"); val formattedDate = format.format(date) val inputs = new FileSystemWorkspace('''initialModels/''', "") + val dataWorkspace = new FileSystemWorkspace('''output/YakinduTest/''', "") val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "") workspace.initAndClear @@ -55,89 +59,120 @@ class YakinduTest { // val queries = null println("DSL loaded") - var SZ_TOP = 10 - var SZ_BOT = 126 - var INC = 1 + var SZ_TOP = 30 + var SZ_BOT = 5 + var INC = 5 var REPS = 1 - - val RANGE = 3 - val EXACT = 10 + val RUNTIME = 20 + + val EXACT = -1 if (EXACT != -1) { SZ_TOP = EXACT SZ_BOT = EXACT INC = 1 - REPS = 1 + REPS = 10 } + val BACKENDSOLVERS = newArrayList( +// BackendSolver::CVC4 +// , +// BackendSolver::DARWINFM +// , +// BackendSolver::EDARWIN +// , +// BackendSolver::GEOIII +// , + BackendSolver::IPROVER +// , +// BackendSolver::PARADOX +// , +// BackendSolver::VAMPIRE +// , +// BackendSolver::Z3 + ) + - var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv") - writer.append("size,") - for (var x = 0; x < REPS; x++) { - writer.append("tTransf" + x + "," + "tSolv" + x + ",") + var str = "" + + for (solver : BACKENDSOLVERS) { + str += solver.name.substring(0, 1) } - writer.append("medSolv,medTransf\n") + + var writer = new PrintWriter( + dataWorkspace.workspaceURI + "//_stats" + formattedDate + "-" + str + SZ_BOT + "to" + SZ_TOP + "by" + INC + + "x" + REPS + ".csv") + writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n") var solverTimes = newArrayList var transformationTimes = newArrayList - var modelFound = true var LogicResult solution = null - for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { - val num = (i - SZ_BOT) / INC - print("Generation " + num + ": SIZE=" + i + " Attempt: ") - writer.append(i + ",") - solverTimes.clear - transformationTimes.clear - modelFound = true - for (var j = 0; j < REPS; j++) { - print(j) + for (BESOLVER : BACKENDSOLVERS) { - val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) - var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) - var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, - new Viatra2LogicConfiguration) + for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { + val num = (i - SZ_BOT) / INC + println() + println("SOLVER: " + BESOLVER.name + ", SIZE=" + i) + println() - var problem = modelGenerationProblem.output - workspace.writeModel(problem, "Yakindu.logicproblem") + solverTimes.clear + transformationTimes.clear + for (var j = 0; j < REPS; j++) { + print("<> :") + + val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, + new Ecore2LogicConfiguration()) + var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel) + var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, + new Viatra2LogicConfiguration) + + var problem = modelGenerationProblem.output +// workspace.writeModel(problem, "Yakindu.logicproblem") // println("Problem created") // Start Time - var startTime = System.currentTimeMillis - - var VampireSolver reasoner - // * - reasoner = new VampireSolver - - // ///////////////////////////////////////////////////// - // Minimum Scope - val classMapMin = new HashMap - classMapMin.put(Region, 1) - classMapMin.put(Transition, 2) - classMapMin.put(CompositeElement, 3) - val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) - // Maximum Scope - val classMapMax = new HashMap - classMapMax.put(Region, 5) - classMapMax.put(Transition, 2) - val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) - // Define Config File - val size = i - val inc = INC - val iter = j - val vampireConfig = new VampireSolverConfiguration => [ - // add configuration things, in config file first - it.documentationLevel = DocumentationLevel::FULL - it.iteration = iter - it.runtimeLimit = 60 - it.typeScopes.maxNewElements = -1 - it.typeScopes.minNewElements = size - it.genModel = false - if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin - if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax - it.contCycleLevel = 5 - it.uniquenessDuplicates = false - ] - - solution = reasoner.solve(problem, vampireConfig, workspace) + var startTime = System.currentTimeMillis + + var VampireSolver reasoner + // * + reasoner = new VampireSolver + + // ///////////////////////////////////////////////////// + // Minimum Scope + val classMapMin = new HashMap + classMapMin.put(Region, 1) + classMapMin.put(Transition, 2) + classMapMin.put(CompositeElement, 3) + val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, + modelGenerationProblem.trace) + // Maximum Scope + val classMapMax = new HashMap + classMapMax.put(Region, 5) + classMapMax.put(Transition, 2) + val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, + modelGenerationProblem.trace) + // Define Config File + val size = i + val inc = INC + val iter = j + val vampireConfig = new VampireSolverConfiguration => [ + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + it.iteration = iter + it.runtimeLimit = RUNTIME +// it.typeScopes.maxNewElements = size + it.typeScopes.minNewElements = size + + it.genModel = true + it.server = true + it.solver = BESOLVER + +// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin +// if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.contCycleLevel = 5 + it.uniquenessDuplicates = false + ] + + solution = reasoner.solve(problem, vampireConfig, workspace) // print((solution as ModelResult).representation.get(0)) // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) // println(soln.confirmations) @@ -145,20 +180,35 @@ class YakinduTest { // modelFound = !soln.confirmations.filter [ // class == VLSFiniteModelImpl // ].isEmpty -// -// if (modelFound) { - val tTime = solution.statistics.transformationTime / 1000.0 - val sTime = solution.statistics.solverTime / 1000.0 - writer.append(tTime + "," + sTime + ",") - print("(" + tTime + "/" + sTime + "s)..") - solverTimes.add(sTime) - transformationTimes.add(tTime) +// ADD TO CSV + writer.append(vampireConfig.solver.name + ",") + writer.append(size + ",") + writer.append(solution.statistics.transformationTime / 1000.0 + ",") + + val satOut = (solution.statistics.entries.filter[name == "satOut"].get(0) as StringStatisticEntry). + value + val satTime = (solution.statistics.entries.filter[name == "satTime"].get(0) as RealStatisticEntry). + value + val modOut = (solution.statistics.entries.filter[name == "modOut"].get(0) as StringStatisticEntry). + value + val modTime = (solution.statistics.entries.filter[name == "modTime"].get(0) as RealStatisticEntry). + value + + writer.append(satOut + ",") + writer.append(satTime + ",") + writer.append(modOut + ",") + writer.append(modTime + ",") + writer.append("\n") + +// print("(" + tTime + "/" + sTime + "s)..") +// solverTimes.add(sTime) +// transformationTimes.add(tTime) // } else { // writer.append("MNF" + ",") //// print("MNF") // } - // println("Problem solved") - // visualisation, see + // println("Problem solved") + // visualisation, see // var interpretations = reasoner.getInterpretations(solution as ModelResult) // for (interpretation : interpretations) { // val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) @@ -168,15 +218,15 @@ class YakinduTest { // var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 // println("Problem solved") // println("Time was: " + totalTimeMin + ":" + totalTimeSec) + } +// println() +// var solverMed = solverTimes.sort.get(REPS / 2) +// var transformationMed = transformationTimes.sort.get(REPS / 2) +// writer.append(solverMed.toString + "," + transformationMed.toString) } - println() - var solverMed = solverTimes.sort.get(REPS / 2) - var transformationMed = transformationTimes.sort.get(REPS / 2) - writer.append(solverMed.toString + "," + transformationMed.toString) - writer.append("\n") + } writer.close - } } -- cgit v1.2.3-70-g09d2