1 files changed, 378 insertions, 0 deletions
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend
new file mode 100644
index 00000000..d8f75b89
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend
@@ -0,0 +1,378 @@
+package hu.bme.mit.inf.dslreasoner.run
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
+import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Statechart
+import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
+import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
+import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
+import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
+import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
+import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print
+import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver
+import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
+import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
+import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
+import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
+import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
+import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation
+import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
+import java.io.BufferedReader
+import java.io.InputStreamReader
+import java.util.ArrayList
+import java.util.Collections
+import java.util.LinkedList
+import java.util.List
+import java.util.Random
+import org.eclipse.emf.ecore.EObject
+import org.eclipse.emf.ecore.resource.Resource
+import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.emf.EMFScope
+import java.lang.invoke.VolatileCallSite
+enum PartialModelSource { Homeworks, Random }
+enum ValidationTechique {Alloy, Viatra}
+class RunModelExtensionMeasurements {
+        val String id
+        
+        new(String id) {
+                this.id = id
+                inputs = new FileSystemWorkspace('''initialModels/''',"")
+                workspace = new FileSystemWorkspace('''output_«id»/''',"")
+        }
+        
+        // Workspace
+        val FileSystemWorkspace inputs
+        val FileSystemWorkspace workspace
+        
+        // Mappers
+        val Ecore2Logic ecore2Logic = new Ecore2Logic
+        val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
+        val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
+        
+        // Solvers
+        val SMTSolver smtSolver = new SMTSolver
+        val ViatraReasoner viatraSolver = new ViatraReasoner
+        val ViatraReasoner viatraWithSmtSolver = new ViatraReasoner
+        val AlloySolver alloyReasoner = new AlloySolver
+        
+        def  dslLoader(Domain dsl) {
+                if(dsl == Domain::FAM) {
+                        return new FAMLoader(inputs)
+                } else if(dsl == Domain::Yakindu) {
+                        return new YakinduLoader(inputs) =>[it.useSynchronization = false useComplexStates = true]
+                } else if(dsl == Domain::FileSystem){
+                        return new FileSystemLoader(inputs)
+                } else if(dsl == Domain::Ecore) {
+                        return new EcoreLoader(inputs)
+                }else throw new IllegalArgumentException('''Unknown domain: «dsl»''')
+        }
+        def static init() {
+                LogiclanguagePackage.eINSTANCE.class
+                LogicproblemPackage.eINSTANCE.class
+                PartialinterpretationPackage.eINSTANCE.class
+                Ecore2logicannotationsPackage.eINSTANCE.class
+                Viatra2LogicAnnotationsPackage.eINSTANCE.class
+                YakindummPackage.eINSTANCE.class
+                Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*",new XMIResourceFactoryImpl)
+        }
+        
+        def transformMMtoLogic(EcoreMetamodelDescriptor mm) {
+                ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration())
+        }
+        def transformPSToLogic(List<EObject> objects, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) {
+                instanceModel2Logic.transform(metamodelProblem,objects)
+        }
+        def transformQueriesToLogic(ViatraQuerySetDescriptor descriptor, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) {
+                viatra2Logic.transformQueries(descriptor,metamodelProblem,new Viatra2LogicConfiguration)
+        }
+        
+        def executeSolver(
+                LogicProblem problem,
+                ViatraQuerySetDescriptor vq,
+                MetamodelLoader loader,
+                DiversityDescriptor diversityRequirement,
+                int size,
+                UseSolver solver)
+        {
+                if(solver == UseSolver.Smt) {
+                        val smtConfig = new SmtSolverConfiguration() => [
+                                it.typeScopes.maxNewElements = size
+                                it.typeScopes.minNewElements = size
+                                it.solutionScope.numberOfRequiredSolution = 1
+                                it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
+                        ]
+                        val solution = this.smtSolver.solve(
+                                problem,
+                                smtConfig,
+                                this.workspace
+                        )
+                        return solution
+                } if(solver==UseSolver::Alloy) {
+                        val alloyConfig = new AlloySolverConfiguration => [
+                                it.typeScopes.maxNewElements = size
+                                it.typeScopes.minNewElements = size
+                                it.solutionScope.numberOfRequiredSolution = 1
+                                it.typeScopes.maxNewIntegers = 0
+                                it.writeToFile = true
+                        ]
+                        val solution = this.alloyReasoner.solve(
+                                problem,
+                                alloyConfig,
+                                this.workspace
+                        )
+                        return solution
+                } else {
+                        val viatraConfig = new ViatraReasonerConfiguration => [
+                                it.runtimeLimit = 400
+                                it.typeScopes.maxNewElements = size
+                                it.typeScopes.minNewElements = size
+                                it.solutionScope.numberOfRequiredSolution = 1
+                                it.existingQueries = vq.patterns.map[it.internalQueryRepresentation]
+                                it.nameNewElements = false
+                                it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
+                                it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints
+                                it.stateCoderStrategy = StateCoderStrategy::Neighbourhood
+                                it.debugCongiguration.partalInterpretationVisualisationFrequency = 100
+                                //it.debugCongiguration.partialInterpretatioVisualiser =
+                                        //new GraphvizVisualisation
+                                        //new PartialInterpretationSizePrinter
+                        ]
+                        viatraConfig.diversityRequirement = diversityRequirement
+                        if (solver == UseSolver.Viatra) {
+                                val solution = this.viatraSolver.solve(
+                                        problem,
+                                        viatraConfig,
+                                        this.workspace
+                                )
+                                return solution
+                        } else if(solver == UseSolver.ViatraWithSmt) {
+                                val inconsistency = new SmtSolverConfiguration() => [
+                                        it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
+                                        it.runtimeLimit = 10
+                                ]
+                                val solution = this.viatraWithSmtSolver.solve(
+                                        problem,
+                                        viatraConfig =>[
+                                                it.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector = smtSolver
+                                                it.internalConsistencyCheckerConfiguration.internalInconsistencDetectorConfiguration = inconsistency
+                                        ],
+                                        this.workspace
+                                )
+                                return solution
+                        }
+                }
+        }
+        
+        def public static loadPartialModels(int size, int max) {
+                if(partialModelSource === PartialModelSource::Homeworks) {
+                        val hfs = new FileSystemWorkspace("D:/Eclipse/GIT/RemoHF/Extracted/output","")
+                        val allFileNames = hfs.allFiles.toList
+                        
+                        
+                        val models = allFileNames.map[hfs.readModel(Statechart,it)]
+                        //println("loaded")
+                        val filtered = if(size===-1) {
+                                        models
+                                } else {
+                                        models.filter[it.eAllContents.size + 1 >= size].toList
+                                }
+                        //println("filtered")
+                        
+                        val selected = if(max!==-1) {
+                                        Collections.shuffle(filtered);
+                                        filtered.subList(0,max)
+                                } else {
+                                        filtered
+                                }
+                        //println("selected "+ selected.size)
+                        val collected = selected.map[
+                                val r = new LinkedList
+                                r.add(it)
+                                r.addAll(it.eAllContents.toIterable)
+                                return r
+                        ].toList
+                        //println("collected to lists")
+                        
+                        val list = new ArrayList(collected.size)
+                        for(s : collected) {
+                                list.add(s.prune(size))
+                        }
+                        //println("pruned to " + size)
+                        
+                        return list
+                } else if(partialModelSource === PartialModelSource::Random) {
+                        
+                }
+        }
+        
+        static val Random pruningRandom = new Random(0)
+//      def private void prune(EObject root, int targetSize) {
+//              var size = root.eAllContents.size + 1
+//              while(size>targetSize) {
+//                      val leafs = root.eAllContents.filter[it.eContents.empty].toList
+//                      val leafToRemove = leafs.get(pruningRandom.nextInt(leafs.size))
+//                      EcoreUtil.delete(leafToRemove)
+//                      size--
+//              }
+//      }
+        def static private prune(List<EObject> objects, int targetSize) {
+                if(targetSize !== -1) {
+                        var size = objects.size
+                        while(size>targetSize) {
+                                val leafs = objects.filter[!it.eAllContents.toList.exists[child | objects.contains(child)]].toList
+                                if(leafs.exists[it instanceof Statechart]) {
+                                        println("Gebasz!")
+                                }
+                                objects.remove(leafs.get(pruningRandom.nextInt(leafs.size)))
+                                size--
+                        }
+                        if(!objects.exists[it instanceof Statechart]) {
+                                println("Gebasz2!")
+                        }
+                        
+                }
+                return objects;
+        }
+        
+        static val partialModelSource = PartialModelSource::Homeworks
+        static val monitoring = false
+        static val clean = true
+        public static var sizes =  #[-1/*,5,10,15,20,25,30,35,40,45,50*/]
+        
+        def static void waitForEnter() {
+                if(monitoring) {
+                        println('''  Press ENTER to continue''')
+                        (new BufferedReader(new InputStreamReader(System.in))).readLine
+                }
+        }
+        
+        def static runMeasure(String id, int size){
+                init
+                
+                val partialModels = loadPartialModels(size,-1)
+                var pmIndex = 1
+                
+                for(partialModel : partialModels) {
+                        
+                        val pmID = id+"_"+(pmIndex++)
+                        val r = new RunModelExtensionMeasurements(pmID)
+                        r.workspace.initAndClear
+                        print(pmID + ";")
+                        print(partialModel.size + ";")
+                        //println("- init")
+                        val dsl = r.dslLoader(Domain::Yakindu)
+                        val mm = dsl.loadMetamodel()
+                        val vq = dsl.loadQueries(mm)
+                        //println("- Queries loaded")
+                        
+                        val metamodelProblem = r.transformMMtoLogic(mm)
+                        r.transformPSToLogic(partialModel,metamodelProblem)
+                        r.transformQueriesToLogic(vq,metamodelProblem)
+                        val logicProblem = metamodelProblem.output
+                        
+                        //println("- DSL -> Logic problem transformation finished")
+                        
+                        waitForEnter
+                        
+                        val ValidationTechique validationTechnique = ValidationTechique::Viatra
+                        if(validationTechnique === ValidationTechique::Alloy) {
+                                val solution = r.executeSolver(logicProblem, vq, dsl, null, 0, UseSolver::Alloy)
+                                
+                                print(solution.class.simpleName+";");
+                                print(solution.statistics.transformationTime+";")
+                                print(solution.statistics.solverTime+";")
+                                print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries))
+                                
+                                waitForEnter
+                                
+                                if(solution instanceof ModelResult) {
+                                        val representations = solution.representation
+                                        for(representationIndex : 0..<representations.size) {
+                                                val representation = representations.get(representationIndex)
+                                                val representationNumber = representationIndex + 1
+                                                if(representation instanceof PartialInterpretation) {
+                                                        r.workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''')
+                                                        val partialInterpretation2GML = new PartialInterpretation2Gml
+                                                        val gml = partialInterpretation2GML.transform(representation)
+                                                        r.workspace.writeText('''solution«representationNumber».gml''',gml)
+                                                        if(representation.newElements.size <160) {
+                                                                val visualiser = new GraphvizVisualisation
+                                                                val visualisation = visualiser.visualiseConcretization(representation)
+                                                                visualisation.writeToFile(r.workspace,'''solution«representationNumber»''')
+                                                        }
+                
+                                                } else {
+                                                        r.workspace.writeText('''solution«representationNumber».txt''',representation.toString)
+                                                }
+                                        }
+                                        println('''saved''')
+                                } else {
+                                        val partial = logicProblem//.eContainer
+                                        r.workspace.writeModel(partial, "solution.partialinterpretation")
+                                        println('''saved''')
+                                }
+                        } else if(validationTechnique === ValidationTechique::Viatra) {
+                                val validationPatterns = vq.validationPatterns
+                                val resource = partialModel.head.eResource
+                                
+                                val startTime = System.currentTimeMillis
+                                val ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(resource) )
+                                val matchers = new ArrayList(validationPatterns.size)
+                                val validationResult = new ArrayList(validationPatterns.size)
+                                for(validationPattern : validationPatterns) {
+                                        val matcher = validationPattern.getMatcher(engine)
+                                        matchers += matcher
+                                        validationResult += matcher.hasMatch
+                                }
+                                val finishTime = System.currentTimeMillis-startTime
+                                
+                                print(finishTime + ";")
+                                print(!validationResult.exists[it] + ";")
+                                for(patternResult : validationResult) {
+                                        print(patternResult + ";")
+                                }
+                                println
+                        }
+                        
+                        System.gc System.gc System.gc
+                        Thread.sleep(2000)                      
+                }
+        }
+        
+        def static void main(String[] args) {
+                //val id = 50//args.get(0)
+                for(size : sizes) {
+                        val run = (1..1).map['''r«it»''']
+                        for(runIndex : run) {
+                                val runID = runIndex+"_"+size
+                                
+                                
+                                try {
+                                        runMeasure(runID,size)
+                                } catch(Exception e) {e.printStackTrace}
+                                
+                                System.gc System.gc System.gc
+                                Thread.sleep(2000)
+                        }
+                }
+                
+        }
+}
+\ No newline at end of file

diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend new file mode 100644 index 00000000..d8f75b89 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend
@@ -0,0 +1,378 @@
	1	package hu.bme.mit.inf.dslreasoner.run
	2
	3	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
	4	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
	5	import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.Statechart
	6	import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
	7	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
	8	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
	9	import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
	10	import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
	11	import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
	12	import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
	13	import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
	14	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
	15	import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
	16	import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
	17	import hu.bme.mit.inf.dslreasoner.logic.model.statistics.StatisticSections2Print
	18	import hu.bme.mit.inf.dslreasoner.smt.reasoner.SMTSolver
	19	import hu.bme.mit.inf.dslreasoner.smt.reasoner.SmtSolverConfiguration
	20	import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
	21	import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
	22	import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
	23	import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
	24	import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
	25	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
	26	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
	27	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
	28	import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
	29	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
	30	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
	31	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
	32	import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
	33	import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation
	34	import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
	35	import java.io.BufferedReader
	36	import java.io.InputStreamReader
	37	import java.util.ArrayList
	38	import java.util.Collections
	39	import java.util.LinkedList
	40	import java.util.List
	41	import java.util.Random
	42	import org.eclipse.emf.ecore.EObject
	43	import org.eclipse.emf.ecore.resource.Resource
	44	import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
	45	import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
	46	import org.eclipse.viatra.query.runtime.emf.EMFScope
	47	import java.lang.invoke.VolatileCallSite
	48
	49	enum PartialModelSource { Homeworks, Random }
	50	enum ValidationTechique {Alloy, Viatra}
	51
	52	class RunModelExtensionMeasurements {
	53	val String id
	54
	55	new(String id) {
	56	this.id = id
	57	inputs = new FileSystemWorkspace('''initialModels/''',"")
	58	workspace = new FileSystemWorkspace('''output_«id»/''',"")
	59	}
	60
	61	// Workspace
	62	val FileSystemWorkspace inputs
	63	val FileSystemWorkspace workspace
	64
	65	// Mappers
	66	val Ecore2Logic ecore2Logic = new Ecore2Logic
	67	val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
	68	val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
	69
	70	// Solvers
	71	val SMTSolver smtSolver = new SMTSolver
	72	val ViatraReasoner viatraSolver = new ViatraReasoner
	73	val ViatraReasoner viatraWithSmtSolver = new ViatraReasoner
	74	val AlloySolver alloyReasoner = new AlloySolver
	75
	76	def dslLoader(Domain dsl) {
	77	if(dsl == Domain::FAM) {
	78	return new FAMLoader(inputs)
	79	} else if(dsl == Domain::Yakindu) {
	80	return new YakinduLoader(inputs) =>[it.useSynchronization = false useComplexStates = true]
	81	} else if(dsl == Domain::FileSystem){
	82	return new FileSystemLoader(inputs)
	83	} else if(dsl == Domain::Ecore) {
	84	return new EcoreLoader(inputs)
	85	}else throw new IllegalArgumentException('''Unknown domain: «dsl»''')
	86	}
	87	def static init() {
	88	LogiclanguagePackage.eINSTANCE.class
	89	LogicproblemPackage.eINSTANCE.class
	90	PartialinterpretationPackage.eINSTANCE.class
	91	Ecore2logicannotationsPackage.eINSTANCE.class
	92	Viatra2LogicAnnotationsPackage.eINSTANCE.class
	93	YakindummPackage.eINSTANCE.class
	94	Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*",new XMIResourceFactoryImpl)
	95	}
	96
	97	def transformMMtoLogic(EcoreMetamodelDescriptor mm) {
	98	ecore2Logic.transformMetamodel(mm,new Ecore2LogicConfiguration())
	99	}
	100	def transformPSToLogic(List<EObject> objects, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) {
	101	instanceModel2Logic.transform(metamodelProblem,objects)
	102	}
	103	def transformQueriesToLogic(ViatraQuerySetDescriptor descriptor, TracedOutput<LogicProblem, Ecore2Logic_Trace> metamodelProblem) {
	104	viatra2Logic.transformQueries(descriptor,metamodelProblem,new Viatra2LogicConfiguration)
	105	}
	106
	107	def executeSolver(
	108	LogicProblem problem,
	109	ViatraQuerySetDescriptor vq,
	110	MetamodelLoader loader,
	111	DiversityDescriptor diversityRequirement,
	112	int size,
	113	UseSolver solver)
	114	{
	115	if(solver == UseSolver.Smt) {
	116	val smtConfig = new SmtSolverConfiguration() => [
	117	it.typeScopes.maxNewElements = size
	118	it.typeScopes.minNewElements = size
	119	it.solutionScope.numberOfRequiredSolution = 1
	120	it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
	121	]
	122	val solution = this.smtSolver.solve(
	123	problem,
	124	smtConfig,
	125	this.workspace
	126	)
	127	return solution
	128	} if(solver==UseSolver::Alloy) {
	129	val alloyConfig = new AlloySolverConfiguration => [
	130	it.typeScopes.maxNewElements = size
	131	it.typeScopes.minNewElements = size
	132	it.solutionScope.numberOfRequiredSolution = 1
	133	it.typeScopes.maxNewIntegers = 0
	134	it.writeToFile = true
	135	]
	136	val solution = this.alloyReasoner.solve(
	137	problem,
	138	alloyConfig,
	139	this.workspace
	140	)
	141	return solution
	142	} else {
	143	val viatraConfig = new ViatraReasonerConfiguration => [
	144	it.runtimeLimit = 400
	145	it.typeScopes.maxNewElements = size
	146	it.typeScopes.minNewElements = size
	147	it.solutionScope.numberOfRequiredSolution = 1
	148	it.existingQueries = vq.patterns.map[it.internalQueryRepresentation]
	149	it.nameNewElements = false
	150	it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
	151	it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints
	152	it.stateCoderStrategy = StateCoderStrategy::Neighbourhood
	153	it.debugCongiguration.partalInterpretationVisualisationFrequency = 100
	154	//it.debugCongiguration.partialInterpretatioVisualiser =
	155	//new GraphvizVisualisation
	156	//new PartialInterpretationSizePrinter
	157	]
	158	viatraConfig.diversityRequirement = diversityRequirement
	159	if (solver == UseSolver.Viatra) {
	160	val solution = this.viatraSolver.solve(
	161	problem,
	162	viatraConfig,
	163	this.workspace
	164	)
	165	return solution
	166	} else if(solver == UseSolver.ViatraWithSmt) {
	167	val inconsistency = new SmtSolverConfiguration() => [
	168	it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
	169	it.runtimeLimit = 10
	170	]
	171	val solution = this.viatraWithSmtSolver.solve(
	172	problem,
	173	viatraConfig =>[
	174	it.internalConsistencyCheckerConfiguration.internalIncosnsitencyDetector = smtSolver
	175	it.internalConsistencyCheckerConfiguration.internalInconsistencDetectorConfiguration = inconsistency
	176	],
	177	this.workspace
	178	)
	179	return solution
	180	}
	181	}
	182	}
	183
	184	def public static loadPartialModels(int size, int max) {
	185	if(partialModelSource === PartialModelSource::Homeworks) {
	186	val hfs = new FileSystemWorkspace("D:/Eclipse/GIT/RemoHF/Extracted/output","")
	187	val allFileNames = hfs.allFiles.toList
	188
	189
	190	val models = allFileNames.map[hfs.readModel(Statechart,it)]
	191	//println("loaded")
	192	val filtered = if(size===-1) {
	193	models
	194	} else {
	195	models.filter[it.eAllContents.size + 1 >= size].toList
	196	}
	197	//println("filtered")
	198
	199	val selected = if(max!==-1) {
	200	Collections.shuffle(filtered);
	201	filtered.subList(0,max)
	202	} else {
	203	filtered
	204	}
	205	//println("selected "+ selected.size)
	206	val collected = selected.map[
	207	val r = new LinkedList
	208	r.add(it)
	209	r.addAll(it.eAllContents.toIterable)
	210	return r
	211	].toList
	212	//println("collected to lists")
	213
	214	val list = new ArrayList(collected.size)
	215	for(s : collected) {
	216	list.add(s.prune(size))
	217	}
	218	//println("pruned to " + size)
	219
	220	return list
	221	} else if(partialModelSource === PartialModelSource::Random) {
	222
	223	}
	224	}
	225
	226	static val Random pruningRandom = new Random(0)
	227	// def private void prune(EObject root, int targetSize) {
	228	// var size = root.eAllContents.size + 1
	229	// while(size>targetSize) {
	230	// val leafs = root.eAllContents.filter[it.eContents.empty].toList
	231	// val leafToRemove = leafs.get(pruningRandom.nextInt(leafs.size))
	232	// EcoreUtil.delete(leafToRemove)
	233	// size--
	234	// }
	235	// }
	236	def static private prune(List<EObject> objects, int targetSize) {
	237	if(targetSize !== -1) {
	238	var size = objects.size
	239	while(size>targetSize) {
	240	val leafs = objects.filter[!it.eAllContents.toList.exists[child \| objects.contains(child)]].toList
	241	if(leafs.exists[it instanceof Statechart]) {
	242	println("Gebasz!")
	243	}
	244	objects.remove(leafs.get(pruningRandom.nextInt(leafs.size)))
	245	size--
	246	}
	247	if(!objects.exists[it instanceof Statechart]) {
	248	println("Gebasz2!")
	249	}
	250
	251	}
	252	return objects;
	253	}
	254
	255	static val partialModelSource = PartialModelSource::Homeworks
	256	static val monitoring = false
	257	static val clean = true
	258	public static var sizes = #[-1/,5,10,15,20,25,30,35,40,45,50/]
	259
	260	def static void waitForEnter() {
	261	if(monitoring) {
	262	println(''' Press ENTER to continue''')
	263	(new BufferedReader(new InputStreamReader(System.in))).readLine
	264	}
	265	}
	266
	267	def static runMeasure(String id, int size){
	268	init
	269
	270	val partialModels = loadPartialModels(size,-1)
	271	var pmIndex = 1
	272
	273	for(partialModel : partialModels) {
	274
	275	val pmID = id+"_"+(pmIndex++)
	276	val r = new RunModelExtensionMeasurements(pmID)
	277	r.workspace.initAndClear
	278	print(pmID + ";")
	279	print(partialModel.size + ";")
	280	//println("- init")
	281	val dsl = r.dslLoader(Domain::Yakindu)
	282	val mm = dsl.loadMetamodel()
	283	val vq = dsl.loadQueries(mm)
	284	//println("- Queries loaded")
	285
	286	val metamodelProblem = r.transformMMtoLogic(mm)
	287	r.transformPSToLogic(partialModel,metamodelProblem)
	288	r.transformQueriesToLogic(vq,metamodelProblem)
	289	val logicProblem = metamodelProblem.output
	290
	291	//println("- DSL -> Logic problem transformation finished")
	292
	293	waitForEnter
	294
	295	val ValidationTechique validationTechnique = ValidationTechique::Viatra
	296	if(validationTechnique === ValidationTechique::Alloy) {
	297	val solution = r.executeSolver(logicProblem, vq, dsl, null, 0, UseSolver::Alloy)
	298
	299	print(solution.class.simpleName+";");
	300	print(solution.statistics.transformationTime+";")
	301	print(solution.statistics.solverTime+";")
	302	print((new StatisticSections2Print).transformStatisticDatas2CSV(solution.statistics.entries))
	303
	304	waitForEnter
	305
	306	if(solution instanceof ModelResult) {
	307	val representations = solution.representation
	308	for(representationIndex : 0..<representations.size) {
	309	val representation = representations.get(representationIndex)
	310	val representationNumber = representationIndex + 1
	311	if(representation instanceof PartialInterpretation) {
	312	r.workspace.writeModel(representation, '''solution«representationNumber».partialinterpretation''')
	313	val partialInterpretation2GML = new PartialInterpretation2Gml
	314	val gml = partialInterpretation2GML.transform(representation)
	315	r.workspace.writeText('''solution«representationNumber».gml''',gml)
	316	if(representation.newElements.size <160) {
	317	val visualiser = new GraphvizVisualisation
	318	val visualisation = visualiser.visualiseConcretization(representation)
	319	visualisation.writeToFile(r.workspace,'''solution«representationNumber»''')
	320	}
	321
	322	} else {
	323	r.workspace.writeText('''solution«representationNumber».txt''',representation.toString)
	324	}
	325	}
	326	println('''saved''')
	327	} else {
	328	val partial = logicProblem//.eContainer
	329	r.workspace.writeModel(partial, "solution.partialinterpretation")
	330	println('''saved''')
	331	}
	332	} else if(validationTechnique === ValidationTechique::Viatra) {
	333	val validationPatterns = vq.validationPatterns
	334	val resource = partialModel.head.eResource
	335
	336	val startTime = System.currentTimeMillis
	337	val ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(resource) )
	338	val matchers = new ArrayList(validationPatterns.size)
	339	val validationResult = new ArrayList(validationPatterns.size)
	340	for(validationPattern : validationPatterns) {
	341	val matcher = validationPattern.getMatcher(engine)
	342	matchers += matcher
	343	validationResult += matcher.hasMatch
	344	}
	345	val finishTime = System.currentTimeMillis-startTime
	346
	347	print(finishTime + ";")
	348	print(!validationResult.exists[it] + ";")
	349	for(patternResult : validationResult) {
	350	print(patternResult + ";")
	351	}
	352	println
	353	}
	354
	355	System.gc System.gc System.gc
	356	Thread.sleep(2000)
	357	}
	358	}
	359
	360	def static void main(String[] args) {
	361	//val id = 50//args.get(0)
	362	for(size : sizes) {
	363	val run = (1..1).map['''r«it»''']
	364	for(runIndex : run) {
	365	val runID = runIndex+"_"+size
	366
	367
	368	try {
	369	runMeasure(runID,size)
	370	} catch(Exception e) {e.printStackTrace}
	371
	372	System.gc System.gc System.gc
	373	Thread.sleep(2000)
	374	}
	375	}
	376
	377	}
	378	} \ No newline at end of file