aboutsummaryrefslogtreecommitdiffstats
path: root/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run
diff options
context:
space:
mode:
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run')
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/CountMatches.xtend176
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend13
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/Ecore2LogicTraceBasedHint.xtend56
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend32
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend6
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend391
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend17
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunModelExtension.xtend18
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphHint.xtend46
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend49
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend95
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/TypeDistributionCalculator.xtend35
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend12
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend77
-rw-r--r--Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend400
15 files changed, 1063 insertions, 360 deletions
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/CountMatches.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/CountMatches.xtend
deleted file mode 100644
index 02caf9dd..00000000
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/CountMatches.xtend
+++ /dev/null
@@ -1,176 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
4import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.Mutated
5import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
6import java.io.File
7import java.util.ArrayList
8import java.util.Collection
9import java.util.Comparator
10import java.util.HashMap
11import java.util.List
12import java.util.Map
13import java.util.TreeSet
14import org.eclipse.emf.ecore.EObject
15import org.eclipse.emf.ecore.resource.Resource
16import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
17import org.eclipse.viatra.query.runtime.api.IPatternMatch
18import org.eclipse.viatra.query.runtime.api.IQuerySpecification
19import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
20import org.eclipse.viatra.query.runtime.emf.EMFScope
21
22class QueryComparator implements Comparator<IQuerySpecification<?>>{
23
24 override compare(IQuerySpecification<?> arg0, IQuerySpecification<?> arg1) {
25 arg0.fullyQualifiedName.compareTo(arg1.fullyQualifiedName)
26 }
27}
28
29class CountMatches {
30 var static List<IQuerySpecification<?>> wfPatterns;
31 var static Map<IQuerySpecification<?>,IQuerySpecification<?>> query2Reference
32
33 def static void main(String[] args) {
34 YakindummPackage.eINSTANCE.eClass
35 Resource.Factory.Registry.INSTANCE.extensionToFactoryMap.put("*",new XMIResourceFactoryImpl)
36
37 wfPatterns = Mutated.instance.specifications.toList;
38 //wfPatterns = wfPatterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toList
39 wfPatterns.sort(new QueryComparator)
40
41 val groupName2Representant = new HashMap
42 query2Reference = new HashMap
43 for(wfPattern : wfPatterns) {
44 val groupName = wfPattern.groupName
45 if(groupName2Representant.containsKey(groupName)) {
46 val representant = groupName2Representant.get(groupName)
47 query2Reference.put(wfPattern,representant)
48 } else {
49 groupName2Representant.put(groupName,wfPattern)
50 }
51 }
52
53
54 println('''modelpath;run;model;«
55 FOR wfPattern:wfPatterns SEPARATOR ";"»#(«
56 wfPattern.fullyQualifiedName.split("\\.").last»);hash(«
57 wfPattern.fullyQualifiedName.split("\\.").last»)«ENDFOR»;«
58 FOR mutant : wfPatterns.filter[query2Reference.keySet.contains(it)] SEPARATOR ';'»diff(«
59 mutant.fullyQualifiedName.split("\\.").last»)«ENDFOR»'''
60 )
61 countMatches('''D:/FASE18Meas/RemoHF''')
62 }
63
64 def private static simpleName(IQuerySpecification<?> wfPattern) {
65 wfPattern.fullyQualifiedName.split("\\.").last
66 }
67 def private static groupName(IQuerySpecification<?> wfPattern) {
68 wfPattern.simpleName.split('_').head
69 }
70
71 def static void countMatches(String path) {
72 val file = new File(path)
73 if(file.isDirectory) {
74 for(subFileName : file.list) {
75 (path + "/" + subFileName).countMatches
76 }
77 } else if(file.isFile) {
78 if(path.endsWith("xmi")) {
79 countMatches(file,path)
80 }
81 }
82 }
83
84 def static void countMatches(File file, String path) {
85
86
87 val pathSegments = path.split("/")
88 val groupName = pathSegments.get(pathSegments.size-2).split("\\.").last.split("_").get(0)
89 print(groupName +";")
90 val nameExtension = pathSegments.get(pathSegments.size-1).split("\\.").get(0).split("_")
91 try{
92 val runNumber = nameExtension.get(1)
93 val modelNumber = nameExtension.get(2)
94 print('''«runNumber»;«modelNumber»''')
95 } catch(Exception e) {
96 print('''«file.name»;0''')
97 }
98
99 val parent = file.parent
100 val workspace = new FileSystemWorkspace(parent,"")
101 val model = workspace.readModel(EObject,file.name)
102
103 val engine = ViatraQueryEngine.on(new EMFScope(model))
104 val objectCode = model.eResource.calculateObjectCode
105
106 val pattern2Hash = new HashMap
107 for(pattern : wfPatterns) {
108 val matcher = pattern.getMatcher(engine)
109 val matches = matcher.allMatches
110 val hash = matches.getMatchSetDescriptor(objectCode)
111 pattern2Hash.put(pattern,hash)
112 print(''';«matcher.countMatches»;«hash»''')
113 }
114 var mutantsKilled = 0
115 for(mutant : wfPatterns.filter[query2Reference.keySet.contains(it)]) {
116 val equals = pattern2Hash.get(mutant) == pattern2Hash.get(query2Reference.get(mutant))
117 print(''';''')
118 if(equals) {
119 print('0')
120 } else {
121 print('1')
122 mutantsKilled++
123 }
124 }
125 //print(''';«mutantsKilled»''')
126 println()
127 }
128
129 def static Map<EObject,Integer> calculateObjectCode(Resource resource) {
130 val res = new HashMap
131 val iterator = resource.allContents
132 var index = 1
133 while(iterator.hasNext) {
134 res.put(iterator.next,index++)
135 }
136 return res
137 }
138
139 def static getMatchSetDescriptor(Collection<? extends IPatternMatch> matchSet, Map<EObject,Integer> objectCode) {
140 val set = new TreeSet(new ArrayComparator)
141 for(match: matchSet) {
142 val size = match.parameterNames.size
143 val idArray = new ArrayList<Integer>(size)
144 for(i:0..<size) {
145 val objectInMatch = match.get(i)
146 if(objectInMatch instanceof EObject) {
147 val id = objectCode.get(objectInMatch)
148 if(id!== null) {
149 idArray+= id
150 } else {
151 throw new IllegalArgumentException('''Unindexed object in match: «objectInMatch»''')
152 }
153 } else {
154 throw new IllegalArgumentException('''Unknown type object in match: "«objectInMatch.class.simpleName»"''')
155 }
156 }
157 set += idArray
158 }
159 return '''«FOR match : set SEPARATOR ','»[«FOR index : match SEPARATOR ','»«index»«ENDFOR»]«ENDFOR»'''.toString.hashCode
160 }
161}
162
163class ArrayComparator implements Comparator<List<Integer>> {
164
165 override compare(List<Integer> arg0, List<Integer> arg1) {
166 if(arg0.size === arg1.size) {
167 for(i : 0..<arg0.size) {
168 val comparison = arg0.get(i).compareTo(arg1.get(i))
169 if(comparison !== 0) return comparison
170 }
171 return 0
172 } else {
173 throw new IllegalArgumentException('''the arrays need to be in the same size''')
174 }
175 }
176} \ No newline at end of file
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend
index daa932fd..e15dbf3f 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/DiverseMeasurementRunner.xtend
@@ -24,7 +24,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy 24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner 25import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration 26import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
27import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation 27import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
28import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 28import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
29import java.util.LinkedList 29import java.util.LinkedList
30import java.util.List 30import java.util.List
@@ -32,9 +32,6 @@ import org.eclipse.emf.ecore.EObject
32import org.eclipse.emf.ecore.resource.Resource 32import org.eclipse.emf.ecore.resource.Resource
33import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 33import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
34import org.eclipse.xtend.lib.annotations.Data 34import org.eclipse.xtend.lib.annotations.Data
35import org.eclipse.viatra.query.runtime.api.IQuerySpecification
36import java.util.Set
37import java.util.Comparator
38 35
39enum Metamodel { 36enum Metamodel {
40 FAM, YakinduWOSynch, Yakindu 37 FAM, YakinduWOSynch, Yakindu
@@ -187,8 +184,7 @@ class ScenarioRunner {
187 it.runtimeLimit = 300 184 it.runtimeLimit = 300
188 it.typeScopes.maxNewElements = scenario.size 185 it.typeScopes.maxNewElements = scenario.size
189 it.typeScopes.minNewElements = scenario.size 186 it.typeScopes.minNewElements = scenario.size
190 it.solutionScope.numberOfRequiredSolution = scenario.number 187 it.solutionScope.numberOfRequiredSolutions = scenario.number
191 it.existingQueries = vq.patterns.map[it.internalQueryRepresentation]
192 it.nameNewElements = false 188 it.nameNewElements = false
193 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis 189 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
194 it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints 190 it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints
@@ -223,9 +219,8 @@ class ScenarioRunner {
223 it.runtimeLimit = 300 219 it.runtimeLimit = 300
224 it.typeScopes.maxNewElements = scenario.size 220 it.typeScopes.maxNewElements = scenario.size
225 it.typeScopes.minNewElements = scenario.size 221 it.typeScopes.minNewElements = scenario.size
226 it.solutionScope.numberOfRequiredSolution = scenario.number 222 it.solutionScope.numberOfRequiredSolutions = scenario.number
227 it.typeScopes.maxNewIntegers = 0 223 it.typeScopes.maxNewIntegers = 0
228 it.writeToFile=true
229 it.randomise = run-1 224 it.randomise = run-1
230 ] 225 ]
231 } 226 }
@@ -259,7 +254,7 @@ class ScenarioRunner {
259// ecore2GML.transform(root) 254// ecore2GML.transform(root)
260// workspace.writeText('''solutionVisualisation«representationNumber».gml''',gml) 255// workspace.writeText('''solutionVisualisation«representationNumber».gml''',gml)
261// 256//
262 val visualiser = new GraphvizVisualisation 257 val visualiser = new GraphvizVisualiser
263 val visualisation = visualiser.visualiseConcretization(representation) 258 val visualisation = visualiser.visualiseConcretization(representation)
264 visualisation.writeToFile(workspace,'''solutionVisualisation«representationNumber»''') 259 visualisation.writeToFile(workspace,'''solutionVisualisation«representationNumber»''')
265 260
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/Ecore2LogicTraceBasedHint.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/Ecore2LogicTraceBasedHint.xtend
new file mode 100644
index 00000000..dc2de30c
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/Ecore2LogicTraceBasedHint.xtend
@@ -0,0 +1,56 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import com.google.common.collect.ImmutableMap
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
5import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
8import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
10import java.util.Map
11import org.eclipse.viatra.query.runtime.api.IPatternMatch
12import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
13
14abstract class Ecore2LogicTraceBasedHint implements LinearTypeConstraintHint {
15 val Map<String, Type> nameToType
16 val Map<String, Map<String, RelationDeclaration>> nameToRelation
17
18 protected new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
19 nameToType = ImmutableMap.copyOf(ecore2Logic.allClassesInScope(trace).toMap[name].mapValues [ eClass |
20 ecore2Logic.TypeofEClass(trace, eClass)
21 ])
22 nameToRelation = ImmutableMap.copyOf(ecore2Logic.allReferencesInScope(trace).groupBy[EContainingClass.name].
23 mapValues [ references |
24 ImmutableMap.copyOf(references.toMap[name].mapValues [ reference |
25 ecore2Logic.relationOfReference(trace, reference)
26 ])
27 ])
28 }
29
30 protected def getType(String name) {
31 nameToType.get(name)
32 }
33
34 protected def relation(String typeName, String relationName) {
35 nameToRelation.get(typeName).get(relationName)
36 }
37
38 protected static def <T extends IPatternMatch> int countMatches(ViatraQueryMatcher<T> matcher, PartialInterpretation p) {
39 val match = matcher.newEmptyMatch
40 match.set(0, p.problem)
41 match.set(1, p)
42 matcher.countMatches(match)
43 }
44
45 protected static def <T extends IPatternMatch> int getCount(ViatraQueryMatcher<T> matcher, PartialInterpretation p) {
46 val match = matcher.newEmptyMatch
47 match.set(0, p.problem)
48 match.set(1, p)
49 val realMatch = matcher.getOneArbitraryMatch(match)
50 if (realMatch.present) {
51 realMatch.get.get(2) as Integer
52 } else {
53 0
54 }
55 }
56}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend
new file mode 100644
index 00000000..8d6523b1
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend
@@ -0,0 +1,32 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
7
8class FileSystemHint extends Ecore2LogicTraceBasedHint {
9 static val REMAINING_CONTENTS_ROOT = "hint_root"
10
11 new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
12 super(ecore2Logic, trace)
13 }
14
15 override getAdditionalPatterns(PatternGenerator it) '''
16 pattern «REMAINING_CONTENTS_ROOT»(problem:LogicProblem, interpretation:PartialInterpretation, remainingContents:java Integer) {
17 find interpretation(problem, interpretation);
18 remainingContents == sum find remainingContents_root_reference_Dir_helper(problem, interpretation, _, #_)
19 }
20 '''
21
22 override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) {
23 val dirCount = createBuilder.add(1, "Dir".type).build
24
25 val remainingContentsRootMatcher = createMatcher(REMAINING_CONTENTS_ROOT)
26
27 return [ p |
28 dirCount.tightenLowerBound(remainingContentsRootMatcher.getCount(p))
29 ]
30 }
31
32}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend
index e79a6261..f4f36951 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemInconsistencyDetector.xtend
@@ -35,11 +35,11 @@ class FileSystemInconsistencyDetector extends ModelGenerationMethodBasedGlobalCo
35 35
36 override checkGlobalConstraint(ThreadContext context) { 36 override checkGlobalConstraint(ThreadContext context) {
37 var requiredNewObjects = 37 var requiredNewObjects =
38 filesystem.countMatches*2 + 38 root.countMatches*2 +
39 root.countMatches 39 filesystem.countMatches
40 val availableNewObjects = partialInterpretation.maxNewElements 40 val availableNewObjects = partialInterpretation.maxNewElements
41 val res = availableNewObjects >= requiredNewObjects 41 val res = availableNewObjects >= requiredNewObjects
42 //println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''') 42 println('''[«availableNewObjects» >= «requiredNewObjects»] = «res»''')
43 return res 43 return res
44 } 44 }
45 45
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
index 43d145d3..bf9ca274 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/MetamodelLoader.xtend
@@ -1,19 +1,26 @@
1package hu.bme.mit.inf.dslreasoner.run 1package hu.bme.mit.inf.dslreasoner.run
2 2
3import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage 3import functionalarchitecture.FunctionalarchitecturePackage
4import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Ecore
4import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.FileSystem 5import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.FileSystem
5import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FilesystemPackage 6import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FilesystemPackage
6import hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern 7import hu.bme.mit.inf.dslreasoner.domains.satellite.queries.internal.SatelliteQueriesAll
8import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns
7import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage 9import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
11import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
8import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor 12import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
9import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns 13import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns
10import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor 14import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
11import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod 15import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod
16import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint
12import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint 17import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint
13import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace 18import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
14import java.util.Collection 19import java.util.Collection
20import java.util.HashMap
15import java.util.LinkedHashMap 21import java.util.LinkedHashMap
16import java.util.List 22import java.util.List
23import java.util.Map
17import java.util.Set 24import java.util.Set
18import org.eclipse.emf.ecore.EAttribute 25import org.eclipse.emf.ecore.EAttribute
19import org.eclipse.emf.ecore.EClass 26import org.eclipse.emf.ecore.EClass
@@ -21,61 +28,91 @@ import org.eclipse.emf.ecore.EEnum
21import org.eclipse.emf.ecore.EEnumLiteral 28import org.eclipse.emf.ecore.EEnumLiteral
22import org.eclipse.emf.ecore.EObject 29import org.eclipse.emf.ecore.EObject
23import org.eclipse.emf.ecore.EReference 30import org.eclipse.emf.ecore.EReference
24import org.eclipse.xtext.xbase.lib.Functions.Function1
25import java.util.HashMap
26import org.eclipse.emf.ecore.EcorePackage 31import org.eclipse.emf.ecore.EcorePackage
27import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Ecore 32import org.eclipse.xtend.lib.annotations.Data
33import org.eclipse.xtext.xbase.lib.Functions.Function1
34import satellite.SatellitePackage
35
36@Data
37class TypeQuantiles {
38 double low
39 double high
40}
28 41
29abstract class MetamodelLoader { 42abstract class MetamodelLoader {
43 public static val UNSAT_PREFIX = "unsat_"
44
30 protected val ReasonerWorkspace workspace 45 protected val ReasonerWorkspace workspace
31 public new(ReasonerWorkspace workspace) { 46
47 new(ReasonerWorkspace workspace) {
32 this.workspace = workspace 48 this.workspace = workspace
33 } 49 }
50
34 def EcoreMetamodelDescriptor loadMetamodel() 51 def EcoreMetamodelDescriptor loadMetamodel()
52
35 def Set<EClass> getRelevantTypes(EcoreMetamodelDescriptor descriptor) 53 def Set<EClass> getRelevantTypes(EcoreMetamodelDescriptor descriptor)
54
36 def Set<EReference> getRelevantReferences(EcoreMetamodelDescriptor descriptor) 55 def Set<EReference> getRelevantReferences(EcoreMetamodelDescriptor descriptor)
56
37 def ViatraQuerySetDescriptor loadQueries(EcoreMetamodelDescriptor metamodel) 57 def ViatraQuerySetDescriptor loadQueries(EcoreMetamodelDescriptor metamodel)
58
38 def List<EObject> loadPartialModel() 59 def List<EObject> loadPartialModel()
60
61 def List<Function1<ModelGenerationMethod, ModelGenerationMethodBasedGlobalConstraint>> additionalConstraints()
62
63 def Map<String, TypeQuantiles> getTypeQuantiles() {
64 emptyMap
65 }
39 66
40 def List<Function1<ModelGenerationMethod,ModelGenerationMethodBasedGlobalConstraint>> additionalConstraints() 67 def Map<String, TypeQuantiles> getUnsatTypeQuantiles() {
41 68 throw new UnsupportedOperationException("This domain has no type quantiles for unsatisfiable problems")
42 def <T> filterByNames(Iterable<T> collection, Function1<T,String> nameExtractor, Collection<String> requiredNames) { 69 }
70
71 def List<LinearTypeConstraintHint> getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
72 emptyList
73 }
74
75 def <T> filterByNames(Iterable<T> collection, Function1<T, String> nameExtractor,
76 Collection<String> requiredNames) {
43 val res = collection.filter[requiredNames.contains(nameExtractor.apply(it))] 77 val res = collection.filter[requiredNames.contains(nameExtractor.apply(it))]
44 if(res.size != requiredNames.size) throw new IllegalArgumentException 78 if(res.size != requiredNames.size) throw new IllegalArgumentException
45 return res.toSet 79 return res.toSet
46 } 80 }
47} 81}
48 82
49class FAMLoader extends MetamodelLoader{ 83class FAMLoader extends MetamodelLoader {
50 84
51 new(ReasonerWorkspace workspace) { 85 new(ReasonerWorkspace workspace) {
52 super(workspace) 86 super(workspace)
53 } 87 }
54 88
55 override loadMetamodel() { 89 override loadMetamodel() {
56 val package = FunctionalArchitecturePackage.eINSTANCE 90 val package = FunctionalarchitecturePackage.eINSTANCE
57 val List<EClass> classes = package.EClassifiers.filter(EClass).toList 91 val List<EClass> classes = package.EClassifiers.filter(EClass).toList
58 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList 92 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList
59 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList 93 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
60 val List<EReference> references = classes.map[EReferences].flatten.toList 94 val List<EReference> references = classes.map[EReferences].flatten.filter [ reference |
95 !#{"model", "type"}.contains(reference.name)
96 ].toList
61 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList 97 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList
62 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) 98 return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes)
63 } 99 }
64 100
65 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) { 101 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) {
66 return descriptor.classes.filterByNames([it.name],#["FunctionalElement"]) 102 return descriptor.classes.filterByNames([it.name], #["FunctionalElement"])
67 } 103 }
104
68 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { 105 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) {
69 return descriptor.references.filterByNames([it.name],#["subElements"]) 106 return descriptor.references.filterByNames([it.name], #["subElements"])
70 } 107 }
71 108
72 override loadQueries(EcoreMetamodelDescriptor metamodel) { 109 override loadQueries(EcoreMetamodelDescriptor metamodel) {
73 val i = Pattern.instance 110 val i = FamPatterns.instance
74 val patterns = i.specifications.toList 111 val patterns = i.specifications.toList
75 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet 112 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
76 val derivedFeatures = new LinkedHashMap 113 val derivedFeatures = new LinkedHashMap
77 derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) 114// derivedFeatures.put(Type.instance,metamodel.attributes.filter[it.name == "type"].head)
78 derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) 115// derivedFeatures.put(Model.instance,metamodel.references.filter[it.name == "model"].head)
79 val res = new ViatraQuerySetDescriptor( 116 val res = new ViatraQuerySetDescriptor(
80 patterns, 117 patterns,
81 wfPatterns, 118 wfPatterns,
@@ -83,65 +120,75 @@ class FAMLoader extends MetamodelLoader{
83 ) 120 )
84 return res 121 return res
85 } 122 }
123
86 override loadPartialModel() { 124 override loadPartialModel() {
87 this.workspace.readModel(EObject,"FAM.xmi").eResource.allContents.toList 125 this.workspace.readModel(EObject, "FAM.xmi").eResource.allContents.toList
88 } 126 }
89 127
90 override additionalConstraints() { #[] } 128 override additionalConstraints() { #[] }
91} 129}
92 130
93class YakinduLoader extends MetamodelLoader{ 131class YakinduLoader extends MetamodelLoader {
94 132
95 private var useSynchronization = true; 133 var useSynchronization = true;
96 private var useComplexStates = false; 134 var useComplexStates = false;
97 public static val patternsWithSynchronization = #[ 135 public static val patternsWithSynchronization = #["synchHasNoOutgoing", "synchHasNoIncoming",
98 "synchHasNoOutgoing", "synchHasNoIncoming", "SynchronizedIncomingInSameRegion", "notSynchronizingStates", 136 "SynchronizedIncomingInSameRegion", "SynchronizedIncomingInSameRegionHelper1",
99 "hasMultipleOutgoingTrainsition", "hasMultipleIncomingTrainsition", "SynchronizedRegionsAreNotSiblings", 137 "SynchronizedIncomingInSameRegionHelper2", "notSynchronizingStates", "hasMultipleOutgoingTrainsition",
100 "SynchronizedRegionDoesNotHaveMultipleRegions", "synchThree", "twoSynch","noSynch2","synch","noSynch4","noSynch3","noSynch"] 138 "hasMultipleIncomingTrainsition", "SynchronizedRegionsAreNotSiblings",
101 public static val patternsWithComplexStates =#["outgoingFromExit","outgoingFromFinal","choiceHasNoOutgoing","choiceHasNoIncoming"] 139 "SynchronizedRegionsAreNotSiblingsHelper1", "SynchronizedRegionsAreNotSiblingsHelper2",
140 "SynchronizedRegionDoesNotHaveMultipleRegions", "synchThree", "twoSynch", "noSynch2", "synch", "noSynch4",
141 "noSynch3", "noSynch"]
142 public static val patternsWithComplexStates = #["outgoingFromExit", "outgoingFromFinal", "choiceHasNoOutgoing",
143 "choiceHasNoIncoming"]
144
145 val boolean satisfiable
146
102 new(ReasonerWorkspace workspace) { 147 new(ReasonerWorkspace workspace) {
148 this(workspace, true)
149 }
150
151 new(ReasonerWorkspace workspace, boolean satisfiable) {
103 super(workspace) 152 super(workspace)
104 YakindummPackage.eINSTANCE.eClass 153 this.satisfiable = satisfiable
105 } 154 }
106 155
107 public def setUseSynchronization(boolean useSynchronization) { 156 def setUseSynchronization(boolean useSynchronization) {
108 this.useSynchronization = useSynchronization 157 this.useSynchronization = useSynchronization
109 } 158 }
110 public def setUseComplexStates(boolean useComplexStates) { 159
160 def setUseComplexStates(boolean useComplexStates) {
111 this.useComplexStates = useComplexStates 161 this.useComplexStates = useComplexStates
112 } 162 }
113 163
114 override loadMetamodel() { 164 override loadMetamodel() {
115 val useSynchInThisLoad = this.useSynchronization 165 val useSynchInThisLoad = this.useSynchronization
116 val useComplexStates = this.useComplexStates 166 val useComplexStates = this.useComplexStates
117 167
118 val package = YakindummPackage.eINSTANCE 168 val package = YakindummPackage.eINSTANCE
119 val List<EClass> classes = package.EClassifiers.filter(EClass) 169 val List<EClass> classes = package.EClassifiers.filter(EClass).filter [
120 .filter[useSynchInThisLoad || (it.name != "Synchronization")] 170 useSynchInThisLoad || (it.name != "Synchronization")
121 .filter[useComplexStates || (it.name != "Choice" && it.name != "Exit" && it.name != "FinalState")] 171 ].filter[useComplexStates || (it.name != "Choice" && it.name != "Exit" && it.name != "FinalState")].toList
122 .toList
123 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList 172 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList
124 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList 173 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
125 val List<EReference> references = classes.map[EReferences].flatten.toList 174 val List<EReference> references = classes.map[EReferences].flatten.toList
126 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList 175 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList
127 176
128 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) 177 return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes)
129 } 178 }
179
130 override loadQueries(EcoreMetamodelDescriptor metamodel) { 180 override loadQueries(EcoreMetamodelDescriptor metamodel) {
131 val useSynchInThisLoad = this.useSynchronization 181 val useSynchInThisLoad = this.useSynchronization
132 182
133 val i = Patterns.instance 183 val i = Patterns.instance
134 val patterns = i.specifications 184 val patterns = i.specifications.filter [ spec |
135 .filter[spec | 185 useSynchInThisLoad || !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)]
136 useSynchInThisLoad || 186 ].filter [ spec |
137 !patternsWithSynchronization.exists[spec.fullyQualifiedName.endsWith(it)] 187 useComplexStates || !patternsWithComplexStates.exists[spec.fullyQualifiedName.endsWith(it)]
138 ] 188 ].filter [
139 .filter[spec | 189 !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX)
140 useComplexStates || 190 ].toList
141 !patternsWithComplexStates.exists[spec.fullyQualifiedName.endsWith(it)] 191 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
142 ]
143 .toList
144 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet
145 val derivedFeatures = new LinkedHashMap 192 val derivedFeatures = new LinkedHashMap
146 val res = new ViatraQuerySetDescriptor( 193 val res = new ViatraQuerySetDescriptor(
147 patterns, 194 patterns,
@@ -150,53 +197,85 @@ class YakinduLoader extends MetamodelLoader{
150 ) 197 )
151 return res 198 return res
152 } 199 }
200
153 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) { 201 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) {
154 descriptor.classes.filterByNames([it.name],#["Vertex","Transition","Synchronization"]) 202 descriptor.classes.filterByNames([it.name], #["Vertex", "Transition", "Synchronization"])
155 } 203 }
156 204
157 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { 205 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) {
158 descriptor.references.filterByNames([it.name],#["source","target"]) 206 descriptor.references.filterByNames([it.name], #["source", "target"])
159 } 207 }
160 208
161 override loadPartialModel() { 209 override loadPartialModel() {
162 this.workspace.readModel(EObject,"Yakindu.xmi").eResource.allContents.toList 210 this.workspace.readModel(EObject, "Yakindu.xmi").eResource.allContents.toList
211 }
212
213 override additionalConstraints() {
214 // #[[method|new SGraphInconsistencyDetector(method)]]
215 emptyList
216 }
217
218 override getTypeQuantiles() {
219 #{
220 "Choice" -> new TypeQuantiles(0.118279569892473, 0.154020979020979),
221 "Entry" -> new TypeQuantiles(0.0283018867924528, 0.0620167525773196),
222 "Exit" -> new TypeQuantiles(0, 0),
223 "FinalState" -> new TypeQuantiles(0, 0),
224 "Region" -> new TypeQuantiles(0.0294117647058824, 0.0633258678611422),
225 "State" -> new TypeQuantiles(0.132023636740618, 0.175925925925926),
226// "Statechart" -> new TypeQuantiles(0.00961538461538462, 0.010752688172043),
227 "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581)
228 }
163 } 229 }
164 230
165 override additionalConstraints() { //#[] 231 override getUnsatTypeQuantiles() {
166 #[[method | new SGraphInconsistencyDetector(method)]] 232 #{
233 "Choice" -> new TypeQuantiles(0.118279569892473, 0.154020979020979),
234 "Entry" -> new TypeQuantiles(0.2, 0.4),
235 "Exit" -> new TypeQuantiles(0, 0),
236 "FinalState" -> new TypeQuantiles(0, 0),
237 "Region" -> new TypeQuantiles(0.0294117647058824, 0.0633258678611422),
238 "State" -> new TypeQuantiles(0.132023636740618, 0.175925925925926),
239// "Statechart" -> new TypeQuantiles(0.00961538461538462, 0.010752688172043),
240 "Transition" -> new TypeQuantiles(0.581632653061224, 0.645161290322581)
241 }
242 }
243
244 override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
245 #[new SGraphHint(ecore2Logic, trace)]
167 } 246 }
168} 247}
169 248
170class FileSystemLoader extends MetamodelLoader{ 249class FileSystemLoader extends MetamodelLoader {
171 250
172 new(ReasonerWorkspace workspace) { 251 new(ReasonerWorkspace workspace) {
173 super(workspace) 252 super(workspace)
174 } 253 }
175 254
176 override loadMetamodel() { 255 override loadMetamodel() {
177 val package = FilesystemPackage.eINSTANCE 256 val package = FilesystemPackage.eINSTANCE
178 val List<EClass> classes = package.EClassifiers.filter(EClass).toList 257 val List<EClass> classes = package.EClassifiers.filter(EClass).toList
179 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList 258 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList
180 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList 259 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
181 val List<EReference> references = classes.map[EReferences].flatten.toList 260 val List<EReference> references = classes.map[EReferences].flatten.filter[name != "live"].toList
182 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList 261 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList
183 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) 262 return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes)
184 } 263 }
185 264
186 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) { 265 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) {
187 return null 266 return null
188 } 267 }
189 268
190 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { 269 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) {
191 null 270 null
192 } 271 }
193 272
194 override loadQueries(EcoreMetamodelDescriptor metamodel) { 273 override loadQueries(EcoreMetamodelDescriptor metamodel) {
195 val patternGroup = FileSystem.instance 274 val patternGroup = FileSystem.instance
196 val patterns = patternGroup.specifications.toList 275 val patterns = patternGroup.specifications.toList
197 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet 276 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
198 val derivedFeatures = new HashMap 277 val derivedFeatures = new HashMap
199 derivedFeatures.put(patternGroup.live,metamodel.references.filter[it.name == "live"].head) 278// derivedFeatures.put(patternGroup.live,metamodel.references.filter[it.name == "live"].head)
200 return new ViatraQuerySetDescriptor( 279 return new ViatraQuerySetDescriptor(
201 patterns, 280 patterns,
202 wfPatterns, 281 wfPatterns,
@@ -204,45 +283,69 @@ class FileSystemLoader extends MetamodelLoader{
204 ) 283 )
205 284
206 } 285 }
207 286
208 override loadPartialModel() { 287 override loadPartialModel() {
209 this.workspace.readModel(EObject,"fs.xmi").eResource.allContents.toList 288 this.workspace.readModel(EObject, "fs.xmi").eResource.allContents.toList
210 } 289 }
211 290
212 override additionalConstraints() { 291 override additionalConstraints() {
213 #[[method | new FileSystemInconsistencyDetector(method)]] 292 // #[[method|new FileSystemInconsistencyDetector(method)]]
293 emptyList
294 }
295
296 override getTypeQuantiles() {
297 #{
298 "Filesystem" -> new TypeQuantiles(0, 0.05),
299 "Dir" -> new TypeQuantiles(0.15, 0.3),
300 "File" -> new TypeQuantiles(0.25, 0.85)
301 }
214 } 302 }
215
216} 303}
217 304
218class EcoreLoader extends MetamodelLoader { 305class EcoreLoader extends MetamodelLoader {
219 306 val boolean satisfiable
307
220 new(ReasonerWorkspace workspace) { 308 new(ReasonerWorkspace workspace) {
309 this(workspace, true)
310 }
311
312 new(ReasonerWorkspace workspace, boolean satisfiable) {
221 super(workspace) 313 super(workspace)
314 this.satisfiable = satisfiable
222 } 315 }
223 316
224 override loadMetamodel() { 317 override loadMetamodel() {
225 val package = EcorePackage.eINSTANCE 318 val package = EcorePackage.eINSTANCE
226 val List<EClass> classes = package.EClassifiers.filter(EClass).filter[it.name!="EFactory"].toList 319 val List<EClass> classes = package.EClassifiers.filter(EClass).filter [
320 it.name != "EFactory" && it.name != "EObject" && it.name != "EResource"
321 ].toList
227 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList 322 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList
228 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList 323 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
229 val List<EReference> references = classes.map[EReferences].flatten.filter[it.name!="eFactoryInstance"].filter[!it.derived].toList 324 val List<EReference> references = classes.map[EReferences].flatten.filter [
230 val List<EAttribute> attributes = #[] //classes.map[EAttributes].flatten.toList 325 it.name != "eFactoryInstance" && it.name != "contents" && it.name != "references" &&
231 return new EcoreMetamodelDescriptor(classes,#{},false,enums,literals,references,attributes) 326 it.name != "eGenericType" && it.name != "eGenericSuperTypes"
327 ].filter[!it.derived].toList
328 val List<EAttribute> attributes = #[] // classes.map[EAttributes].flatten.toList
329 return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes)
232 } 330 }
233 331
234 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) { 332 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) {
235 return null 333 return null
236 } 334 }
237 335
238 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) { 336 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) {
239 null 337 null
240 } 338 }
241 339
242 override loadQueries(EcoreMetamodelDescriptor metamodel) { 340 override loadQueries(EcoreMetamodelDescriptor metamodel) {
243 val patternGroup = Ecore.instance 341 val patternGroup = Ecore.instance
244 val patterns = patternGroup.specifications.toList 342 val patterns = patternGroup.specifications.toList
245 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet 343 val allWfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
344 val wfPatterns = if (satisfiable) {
345 allWfPatterns.filter[!it.simpleName.startsWith(UNSAT_PREFIX)].toSet
346 } else {
347 allWfPatterns
348 }
246 val derivedFeatures = new HashMap 349 val derivedFeatures = new HashMap
247 return new ViatraQuerySetDescriptor( 350 return new ViatraQuerySetDescriptor(
248 patterns, 351 patterns,
@@ -251,13 +354,111 @@ class EcoreLoader extends MetamodelLoader {
251 ) 354 )
252 355
253 } 356 }
254 357
255 override loadPartialModel() { 358 override loadPartialModel() {
256 this.workspace.readModel(EObject,"ecore.xmi").eResource.allContents.toList 359 this.workspace.readModel(EObject, "ecore.xmi").eResource.allContents.toList
257 } 360 }
258 361
259 override additionalConstraints() { 362 override additionalConstraints() {
260 #[] 363 #[]
261 } 364 }
262 365
263} \ No newline at end of file 366 override getTypeQuantiles() {
367 #{
368 "EAnnotation" -> new TypeQuantiles(0, 0),
369 "EAttribute" -> new TypeQuantiles(0.14, 0.300943396226415),
370 "EClass" -> new TypeQuantiles(0.224014336917563, 0.372881355932203),
371 "EDataType" -> new TypeQuantiles(0, 0),
372 "EEnum" -> new TypeQuantiles(0, 0.0275208638045255),
373 "EEnumLiteral" -> new TypeQuantiles(0, 0.105204907665065),
374 "EGenericType" -> new TypeQuantiles(0, 0),
375 "EOperation" -> new TypeQuantiles(0, 0),
376 "EPackage" -> new TypeQuantiles(0.0119047619047619, 0.0192307692307692),
377 "EParameter" -> new TypeQuantiles(0, 0),
378 "EReference" -> new TypeQuantiles(0.217599234815878, 0.406779661016949),
379 "EStringToStringMapEntry" -> new TypeQuantiles(0, 0),
380 "ETypeParameter" -> new TypeQuantiles(0, 0)
381 }
382 }
383
384}
385
386class SatelliteLoader extends MetamodelLoader {
387 val boolean satisfiable
388
389 new(ReasonerWorkspace workspace) {
390 this(workspace, true)
391 }
392
393 new(ReasonerWorkspace workspace, boolean satisfiable) {
394 super(workspace)
395 this.satisfiable = satisfiable
396 }
397
398 override loadMetamodel() {
399 val package = SatellitePackage.eINSTANCE
400 val List<EClass> classes = package.EClassifiers.filter(EClass).toList
401 val List<EEnum> enums = package.EClassifiers.filter(EEnum).toList
402 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
403 val List<EReference> references = classes.map[EReferences].flatten.toList
404 val List<EAttribute> attributes = classes.map[EAttributes].flatten.toList
405 return new EcoreMetamodelDescriptor(classes, #{}, false, enums, literals, references, attributes)
406 }
407
408 override getRelevantTypes(EcoreMetamodelDescriptor descriptor) {
409 null
410 }
411
412 override getRelevantReferences(EcoreMetamodelDescriptor descriptor) {
413 null
414 }
415
416 override loadQueries(EcoreMetamodelDescriptor metamodel) {
417 val i = SatelliteQueriesAll.instance
418 val patterns = i.specifications.filter [
419 !satisfiable || !it.simpleName.startsWith(UNSAT_PREFIX)
420 ].toList
421 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name == "Constraint"]].toSet
422 val derivedFeatures = new LinkedHashMap
423 val res = new ViatraQuerySetDescriptor(
424 patterns,
425 wfPatterns,
426 derivedFeatures
427 )
428 return res
429 }
430
431 override loadPartialModel() {
432 this.workspace.readModel(EObject, "satellite.xmi").eResource.allContents.toList
433 }
434
435 override additionalConstraints() { #[] }
436
437 override getHints(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
438 #[new SatelliteHint(ecore2Logic, trace)]
439 }
440
441 override getTypeQuantiles() {
442 #{
443 "CubeSat3U" -> new TypeQuantiles(0.1, 0.25),
444 "CubeSat6U" -> new TypeQuantiles(0, 0.25),
445 "SmallSat" -> new TypeQuantiles(0, 0.15),
446 "UHFCommSubsystem" -> new TypeQuantiles(0.08, 0.25),
447 "XCommSubsystem" -> new TypeQuantiles(0.08, 0.25),
448 "KaCommSubsystem" -> new TypeQuantiles(0, 0.1),
449 "InterferometryPayload" -> new TypeQuantiles(0.15, 0.25)
450 }
451 }
452
453 override getUnsatTypeQuantiles() {
454 #{
455 "CubeSat3U" -> new TypeQuantiles(0.1, 0.25),
456 "CubeSat6U" -> new TypeQuantiles(0.1, 0.25),
457 "SmallSat" -> new TypeQuantiles(0.1, 0.25),
458 "UHFCommSubsystem" -> new TypeQuantiles(0.08, 0.1),
459 "XCommSubsystem" -> new TypeQuantiles(0, 0.1),
460 "KaCommSubsystem" -> new TypeQuantiles(0, 0.05),
461 "InterferometryPayload" -> new TypeQuantiles(0.15, 0.25)
462 }
463 }
464}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend
index 8d96958d..ae810a9b 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/RunMeasurements.xtend
@@ -25,10 +25,12 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
25import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic 25import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
26import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 26import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage 27import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
28import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
28import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor 29import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
29import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy 30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner 31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration 32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
33import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
32import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 34import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
33import java.io.BufferedReader 35import java.io.BufferedReader
34import java.io.InputStreamReader 36import java.io.InputStreamReader
@@ -37,9 +39,6 @@ import org.eclipse.emf.ecore.EObject
37import org.eclipse.emf.ecore.resource.Resource 39import org.eclipse.emf.ecore.resource.Resource
38import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 40import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
39import org.junit.Test 41import org.junit.Test
40import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation
41import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationSizePrinter
42import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
43 42
44enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy} 43enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy}
45enum Domain{FAM, Yakindu, FileSystem,Ecore} 44enum Domain{FAM, Yakindu, FileSystem,Ecore}
@@ -129,7 +128,7 @@ class RunMeasurements {
129 val smtConfig = new SmtSolverConfiguration() => [ 128 val smtConfig = new SmtSolverConfiguration() => [
130 it.typeScopes.maxNewElements = size 129 it.typeScopes.maxNewElements = size
131 it.typeScopes.minNewElements = size 130 it.typeScopes.minNewElements = size
132 it.solutionScope.numberOfRequiredSolution = number 131 it.solutionScope.numberOfRequiredSolutions = number
133 it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' 132 it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
134 ] 133 ]
135 val solution = this.smtSolver.solve( 134 val solution = this.smtSolver.solve(
@@ -142,9 +141,8 @@ class RunMeasurements {
142 val alloyConfig = new AlloySolverConfiguration => [ 141 val alloyConfig = new AlloySolverConfiguration => [
143 it.typeScopes.maxNewElements = size 142 it.typeScopes.maxNewElements = size
144 it.typeScopes.minNewElements = size 143 it.typeScopes.minNewElements = size
145 it.solutionScope.numberOfRequiredSolution = number 144 it.solutionScope.numberOfRequiredSolutions = number
146 it.typeScopes.maxNewIntegers = 0 145 it.typeScopes.maxNewIntegers = 0
147 it.writeToFile = true
148 ] 146 ]
149 val solution = this.alloyReasoner.solve( 147 val solution = this.alloyReasoner.solve(
150 problem, 148 problem,
@@ -157,13 +155,12 @@ class RunMeasurements {
157 it.runtimeLimit = 400 155 it.runtimeLimit = 400
158 it.typeScopes.maxNewElements = size 156 it.typeScopes.maxNewElements = size
159 it.typeScopes.minNewElements = size 157 it.typeScopes.minNewElements = size
160 it.solutionScope.numberOfRequiredSolution = number 158 it.solutionScope.numberOfRequiredSolutions = number
161 it.existingQueries = vq.patterns.map[it.internalQueryRepresentation]
162 it.nameNewElements = false 159 it.nameNewElements = false
163 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis 160 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
164 it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints 161 it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints
165 it.stateCoderStrategy = StateCoderStrategy::Neighbourhood 162 it.stateCoderStrategy = StateCoderStrategy::Neighbourhood
166 it.debugCongiguration.partalInterpretationVisualisationFrequency = 100 163 it.debugConfiguration.partalInterpretationVisualisationFrequency = 100
167 //it.debugCongiguration.partialInterpretatioVisualiser = 164 //it.debugCongiguration.partialInterpretatioVisualiser =
168 //new GraphvizVisualisation 165 //new GraphvizVisualisation
169 //new PartialInterpretationSizePrinter 166 //new PartialInterpretationSizePrinter
@@ -267,7 +264,7 @@ class RunMeasurements {
267 val gml = partialInterpretation2GML.transform(representation) 264 val gml = partialInterpretation2GML.transform(representation)
268 r.workspace.writeText('''solution«representationNumber».gml''',gml) 265 r.workspace.writeText('''solution«representationNumber».gml''',gml)
269 if(representation.newElements.size <160) { 266 if(representation.newElements.size <160) {
270 val visualiser = new GraphvizVisualisation 267 val visualiser = new GraphvizVisualiser
271 val visualisation = visualiser.visualiseConcretization(representation) 268 val visualisation = visualiser.visualiseConcretization(representation)
272 visualisation.writeToFile(r.workspace,'''solution«representationNumber»''') 269 visualisation.writeToFile(r.workspace,'''solution«representationNumber»''')
273 } 270 }
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
index d8f75b89..1b8fe3e9 100644
--- 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
@@ -30,7 +30,7 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor
30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy 30import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner 31import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration 32import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
33import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation 33import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
34import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 34import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
35import java.io.BufferedReader 35import java.io.BufferedReader
36import java.io.InputStreamReader 36import java.io.InputStreamReader
@@ -44,7 +44,6 @@ import org.eclipse.emf.ecore.resource.Resource
44import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 44import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
45import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine 45import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
46import org.eclipse.viatra.query.runtime.emf.EMFScope 46import org.eclipse.viatra.query.runtime.emf.EMFScope
47import java.lang.invoke.VolatileCallSite
48 47
49enum PartialModelSource { Homeworks, Random } 48enum PartialModelSource { Homeworks, Random }
50enum ValidationTechique {Alloy, Viatra} 49enum ValidationTechique {Alloy, Viatra}
@@ -116,7 +115,7 @@ class RunModelExtensionMeasurements {
116 val smtConfig = new SmtSolverConfiguration() => [ 115 val smtConfig = new SmtSolverConfiguration() => [
117 it.typeScopes.maxNewElements = size 116 it.typeScopes.maxNewElements = size
118 it.typeScopes.minNewElements = size 117 it.typeScopes.minNewElements = size
119 it.solutionScope.numberOfRequiredSolution = 1 118 it.solutionScope.numberOfRequiredSolutions = 1
120 it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"''' 119 it.solverPath = '''"D:/Programs/Z3/4.3/z3.exe"'''
121 ] 120 ]
122 val solution = this.smtSolver.solve( 121 val solution = this.smtSolver.solve(
@@ -129,9 +128,8 @@ class RunModelExtensionMeasurements {
129 val alloyConfig = new AlloySolverConfiguration => [ 128 val alloyConfig = new AlloySolverConfiguration => [
130 it.typeScopes.maxNewElements = size 129 it.typeScopes.maxNewElements = size
131 it.typeScopes.minNewElements = size 130 it.typeScopes.minNewElements = size
132 it.solutionScope.numberOfRequiredSolution = 1 131 it.solutionScope.numberOfRequiredSolutions = 1
133 it.typeScopes.maxNewIntegers = 0 132 it.typeScopes.maxNewIntegers = 0
134 it.writeToFile = true
135 ] 133 ]
136 val solution = this.alloyReasoner.solve( 134 val solution = this.alloyReasoner.solve(
137 problem, 135 problem,
@@ -144,16 +142,12 @@ class RunModelExtensionMeasurements {
144 it.runtimeLimit = 400 142 it.runtimeLimit = 400
145 it.typeScopes.maxNewElements = size 143 it.typeScopes.maxNewElements = size
146 it.typeScopes.minNewElements = size 144 it.typeScopes.minNewElements = size
147 it.solutionScope.numberOfRequiredSolution = 1 145 it.solutionScope.numberOfRequiredSolutions = 1
148 it.existingQueries = vq.patterns.map[it.internalQueryRepresentation]
149 it.nameNewElements = false 146 it.nameNewElements = false
150 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis 147 it.typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis
151 it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints 148 it.searchSpaceConstraints.additionalGlobalConstraints += loader.additionalConstraints
152 it.stateCoderStrategy = StateCoderStrategy::Neighbourhood 149 it.stateCoderStrategy = StateCoderStrategy::Neighbourhood
153 it.debugCongiguration.partalInterpretationVisualisationFrequency = 100 150 it.debugConfiguration.partalInterpretationVisualisationFrequency = 100
154 //it.debugCongiguration.partialInterpretatioVisualiser =
155 //new GraphvizVisualisation
156 //new PartialInterpretationSizePrinter
157 ] 151 ]
158 viatraConfig.diversityRequirement = diversityRequirement 152 viatraConfig.diversityRequirement = diversityRequirement
159 if (solver == UseSolver.Viatra) { 153 if (solver == UseSolver.Viatra) {
@@ -314,7 +308,7 @@ class RunModelExtensionMeasurements {
314 val gml = partialInterpretation2GML.transform(representation) 308 val gml = partialInterpretation2GML.transform(representation)
315 r.workspace.writeText('''solution«representationNumber».gml''',gml) 309 r.workspace.writeText('''solution«representationNumber».gml''',gml)
316 if(representation.newElements.size <160) { 310 if(representation.newElements.size <160) {
317 val visualiser = new GraphvizVisualisation 311 val visualiser = new GraphvizVisualiser
318 val visualisation = visualiser.visualiseConcretization(representation) 312 val visualisation = visualiser.visualiseConcretization(representation)
319 visualisation.writeToFile(r.workspace,'''solution«representationNumber»''') 313 visualisation.writeToFile(r.workspace,'''solution«representationNumber»''')
320 } 314 }
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphHint.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphHint.xtend
new file mode 100644
index 00000000..97ce4ee6
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphHint.xtend
@@ -0,0 +1,46 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
7
8class SGraphHint extends Ecore2LogicTraceBasedHint {
9 new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
10 super(ecore2Logic, trace)
11 }
12
13 override getAdditionalPatterns(extension PatternGenerator patternGenerator) {
14 ""
15 }
16
17 override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) {
18 val newEntriesWithoutRegionCount = createBuilder.add(1, "Entry".type).add(-1, "Region".type).build
19 val newStatesWithoutRegionCount = createBuilder.add(1, "State".type).add(-1, "Region".type).build
20 val newTransitionWithoutNeedsOutgoingCount = createBuilder.add(1, "Transition".type).add(-1, "Entry".type).
21 add(-1, "Choice".type).build
22 val newTransitionWithoutNeedsIncomingCount = createBuilder.add(1, "Transition".type).add(-1, "Choice".type).
23 build
24
25 val regionsWithoutEntryMatcher = createMatcher(
26 "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion")
27 val regionsWithoutStateMatcher = createMatcher(
28 "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion")
29 val entryHasNoOutgoingMatcher = createMatcher(
30 "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry")
31 val choiceHasNoOutgoingMatcher = createMatcher(
32 "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoOutgoing")
33 val choiceHasNoIncomingMatcher = createMatcher(
34 "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoIncoming")
35 val transitionWithoutTargetMatcher = createMatcher("unfinishedLowerMultiplicity_target_reference_Transition")
36
37 return [ p |
38 newEntriesWithoutRegionCount.assertEqualsTo(regionsWithoutEntryMatcher.countMatches(p))
39 newStatesWithoutRegionCount.tightenLowerBound(regionsWithoutStateMatcher.countMatches(p))
40 newTransitionWithoutNeedsOutgoingCount.tightenLowerBound(
41 entryHasNoOutgoingMatcher.countMatches(p) + choiceHasNoOutgoingMatcher.countMatches(p))
42 newTransitionWithoutNeedsIncomingCount.tightenLowerBound(
43 choiceHasNoIncomingMatcher.countMatches(p) - transitionWithoutTargetMatcher.getCount(p))
44 ]
45 }
46}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend
new file mode 100644
index 00000000..ef5b779e
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend
@@ -0,0 +1,49 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality
6import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory
7import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator
8
9class SatelliteHint extends Ecore2LogicTraceBasedHint {
10 static val INTERFEROMETY_PAYLOAD = "hint_interferometryPayload"
11 static val REMAINING_CONTENTS_KA_COMM_SUBSYSTEM = "hint_kaCommSubsystem"
12
13 new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) {
14 super(ecore2Logic, trace)
15 }
16
17 override getAdditionalPatterns(PatternGenerator it) '''
18 pattern «INTERFEROMETY_PAYLOAD»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement) {
19 find interpretation(problem, interpretation);
20 find mustExist(problem, interpretation, object);
21 «typeIndexer.referInstanceOf("InterferometryPayload".type, Modality.MUST, "object")»
22 }
23
24 private pattern «REMAINING_CONTENTS_KA_COMM_SUBSYSTEM»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingContents:java Integer) {
25 find remainingContents_commSubsystem_reference_CommunicatingElement_helper(problem, interpretation, object, remainingContents);
26 «typeIndexer.referInstanceOf("SmallSat".type, Modality.MUST, "object")»
27 }
28
29 pattern «REMAINING_CONTENTS_KA_COMM_SUBSYSTEM»(problem:LogicProblem, interpretation:PartialInterpretation, remainingContents:java Integer) {
30 find interpretation(problem, interpretation);
31 remainingContents == sum find «REMAINING_CONTENTS_KA_COMM_SUBSYSTEM»_helper(problem, interpretation, _, #_);
32 }
33 '''
34
35 override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) {
36 val interferometryPayloadCount = createBuilder.add(1, "InterferometryPayload".type).build
37 val kaCommSubsystemWithoutSmallSatCount = createBuilder.add(1, "KaCommSubsystem".type).add(-2, "SmallSat".type).
38 build
39
40 val interferometryPayloadMatcher = createMatcher(INTERFEROMETY_PAYLOAD)
41 val kaCommSubsystemRemainingContentsMatcher = createMatcher(REMAINING_CONTENTS_KA_COMM_SUBSYSTEM)
42
43 return [ p |
44 interferometryPayloadCount.tightenLowerBound(2 - interferometryPayloadMatcher.countMatches(p))
45 kaCommSubsystemWithoutSmallSatCount.tightenUpperBound(kaCommSubsystemRemainingContentsMatcher.getCount(p))
46 ]
47 }
48
49}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend
index 863a91c8..b65826ad 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SimpleRun.xtend
@@ -1,41 +1,42 @@
1package hu.bme.mit.inf.dslreasoner.run 1package hu.bme.mit.inf.dslreasoner.run
2 2
3import functionalarchitecture.FunctionalarchitecturePackage
4import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns
5import hu.bme.mit.inf.dslreasoner.domains.transima.fam.Model
6import hu.bme.mit.inf.dslreasoner.domains.transima.fam.Type
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
12import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
13import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
14import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
15import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
16import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
17import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
18import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
19import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
20import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
21import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
22import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
24import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
3import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 25import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
4import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage 26import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
27import java.util.LinkedHashMap
28import java.util.LinkedList
5import java.util.List 29import java.util.List
30import org.eclipse.emf.ecore.EAttribute
6import org.eclipse.emf.ecore.EClass 31import org.eclipse.emf.ecore.EClass
7import org.eclipse.emf.ecore.EEnumLiteral
8import org.eclipse.emf.ecore.EReference
9import org.eclipse.emf.ecore.EEnum 32import org.eclipse.emf.ecore.EEnum
10import org.eclipse.emf.ecore.EAttribute 33import org.eclipse.emf.ecore.EEnumLiteral
11import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor
12import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
13import org.eclipse.emf.ecore.EObject 34import org.eclipse.emf.ecore.EObject
14import java.util.LinkedHashMap 35import org.eclipse.emf.ecore.EReference
15import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor
16import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
17import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
18import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
19import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
20import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
21import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
22import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod
23import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy
24import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
25import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
26import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
27import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
28import org.eclipse.emf.ecore.resource.Resource 36import org.eclipse.emf.ecore.resource.Resource
29import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 37import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
30import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml 38import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup
31import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration 39import org.eclipse.viatra.query.runtime.rete.matcher.ReteEngine
32import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
33import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
34import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner
35import java.util.LinkedList
36import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation
37import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicStructureBuilder
38import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
39 40
40class SimpleRun { 41class SimpleRun {
41 42
@@ -59,7 +60,8 @@ class SimpleRun {
59 60
60 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) 61 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration())
61 val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel) 62 val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel)
62 val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration) 63 val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelExtensionProblem,new Viatra2LogicConfiguration)
64// workspace.writeModel(validModelExtensionProblem.output, "generation.logicproblem")
63 65
64 val logicProblem = validModelExtensionProblem.output 66 val logicProblem = validModelExtensionProblem.output
65 67
@@ -71,11 +73,11 @@ class SimpleRun {
71 val viatraConfig = new ViatraReasonerConfiguration => [ 73 val viatraConfig = new ViatraReasonerConfiguration => [
72 it.typeScopes.maxNewElements = 40 74 it.typeScopes.maxNewElements = 40
73 it.typeScopes.minNewElements = 40 75 it.typeScopes.minNewElements = 40
74 it.solutionScope.numberOfRequiredSolution = 1 76 it.solutionScope.numberOfRequiredSolutions = 1
75 it.existingQueries = queries.patterns.map[it.internalQueryRepresentation] 77// it.scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy
76 it.debugCongiguration.logging = false 78 it.documentationLevel = DocumentationLevel.NONE
77 it.debugCongiguration.partalInterpretationVisualisationFrequency = 1 79 it.debugConfiguration.partalInterpretationVisualisationFrequency = 1
78 it.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualisation 80 it.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser
79 ] 81 ]
80 solution = reasoner.solve(logicProblem,viatraConfig,workspace) 82 solution = reasoner.solve(logicProblem,viatraConfig,workspace)
81 /*/ 83 /*/
@@ -92,23 +94,20 @@ class SimpleRun {
92 94
93 println("Problem solved") 95 println("Problem solved")
94 96
95 val interpretations = reasoner.getInterpretations(solution as ModelResult) 97 val result = solution as ModelResult
98 val interpretations = reasoner.getInterpretations(result)
96 val models = new LinkedList 99 val models = new LinkedList
97 for(interpretation : interpretations) { 100 for(interpretation : interpretations) {
98 val extension b = new LogicStructureBuilder
99 val extension a = new LogicProblemBuilder
100
101
102
103 val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) 101 val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace)
104 models+=instanceModel 102 models+=instanceModel
105 } 103 }
104 println(result.statistics.solverTime)
106 105
107 solution.writeSolution(workspace, #[]) 106 solution.writeSolution(workspace, #[])
108 } 107 }
109 108
110 def private static loadMetamodel() { 109 def private static loadMetamodel() {
111 val pckg = FunctionalArchitecturePackage.eINSTANCE 110 val pckg = FunctionalarchitecturePackage.eINSTANCE
112 val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList 111 val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList
113 val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList 112 val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList
114 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList 113 val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList
@@ -118,12 +117,12 @@ class SimpleRun {
118 } 117 }
119 118
120 def private static loadQueries(EcoreMetamodelDescriptor metamodel) { 119 def private static loadQueries(EcoreMetamodelDescriptor metamodel) {
121 val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance 120 val i = FamPatterns.instance
122 val patterns = i.specifications.toList 121 val patterns = i.specifications.toList
123 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet 122 val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet
124 val derivedFeatures = new LinkedHashMap 123 val derivedFeatures = new LinkedHashMap
125 derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) 124 derivedFeatures.put(Type.instance,metamodel.attributes.filter[it.name == "type"].head)
126 derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) 125 derivedFeatures.put(Model.instance,metamodel.references.filter[it.name == "model"].head)
127 val res = new ViatraQuerySetDescriptor( 126 val res = new ViatraQuerySetDescriptor(
128 patterns, 127 patterns,
129 wfPatterns, 128 wfPatterns,
@@ -133,6 +132,8 @@ class SimpleRun {
133 } 132 }
134 133
135 def static loadPartialModel(ReasonerWorkspace inputs) { 134 def static loadPartialModel(ReasonerWorkspace inputs) {
135 EMFPatternLanguageStandaloneSetup.doSetup
136 ReteEngine.getClass
136 Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); 137 Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl());
137 inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList 138 inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList
138 } 139 }
@@ -160,8 +161,4 @@ class SimpleRun {
160 println("Solution saved and visualised") 161 println("Solution saved and visualised")
161 } 162 }
162 } 163 }
163
164 def static visualizeSolution() {
165
166 }
167} \ No newline at end of file 164} \ No newline at end of file
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/TypeDistributionCalculator.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/TypeDistributionCalculator.xtend
new file mode 100644
index 00000000..e2d6e6ca
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/TypeDistributionCalculator.xtend
@@ -0,0 +1,35 @@
1package hu.bme.mit.inf.dslreasoner.run
2
3import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage
4import java.io.File
5import org.eclipse.emf.common.util.URI
6import org.eclipse.emf.ecore.EPackage
7import org.eclipse.emf.ecore.EcorePackage
8import org.eclipse.emf.ecore.resource.Resource
9import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl
10import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
11
12class TypeDistributionCalculator {
13 public static def void main(String[] args) {
14 Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl)
15 EPackage.Registry.INSTANCE.put(EcorePackage.eNS_URI, EcorePackage.eINSTANCE)
16 EPackage.Registry.INSTANCE.put(YakindummPackage.eNS_URI, YakindummPackage.eINSTANCE)
17
18 println("model,className,count")
19 val directory = new File(args.get(0))
20 for (file : directory.listFiles) {
21 val modelName = file.name
22 val resourceSet = new ResourceSetImpl
23 val resource = resourceSet.getResource(URI.createFileURI(file.absolutePath), true)
24 val objectsByTypeName = resource.allContents.filter [ obj |
25 val featureName = obj.eContainingFeature?.name
26 // Filter out "derived containment" references in Ecore.
27 // See https://stackoverflow.com/a/46340165
28 featureName != "eGenericType" && featureName != "eGenericSuperTypes"
29 ].groupBy[eClass.name]
30 for (pair : objectsByTypeName.entrySet) {
31 println('''«modelName»,«pair.key»,«pair.value.size»''')
32 }
33 }
34 }
35}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend
index 6b74d161..3a100ace 100644
--- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/VisualiseAllModelInDirectory.xtend
@@ -1,16 +1,16 @@
1package hu.bme.mit.inf.dslreasoner.run 1package hu.bme.mit.inf.dslreasoner.run
2 2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
3import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage 5import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
6import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
4import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation 7import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
5import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage 8import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage
9import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
10import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser
6import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace 11import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
7import java.io.File 12import java.io.File
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage
9import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage
10import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage
11import org.eclipse.emf.ecore.resource.Resource 13import org.eclipse.emf.ecore.resource.Resource
12import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml
13import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation
14import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 14import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
15 15
16class VisualiseAllModelInDirectory { 16class VisualiseAllModelInDirectory {
@@ -62,7 +62,7 @@ class VisualiseAllModelInDirectory {
62 } 62 }
63 63
64 if(!hasPng && model.newElements.size <160) { 64 if(!hasPng && model.newElements.size <160) {
65 val visualiser = new GraphvizVisualisation 65 val visualiser = new GraphvizVisualiser
66 val visualisation = visualiser.visualiseConcretization(model) 66 val visualisation = visualiser.visualiseConcretization(model)
67 visualisation.writeToFile(workspace,fileNameWithoutExtension) 67 visualisation.writeToFile(workspace,fileNameWithoutExtension)
68 println('''«fileNameWithoutExtension».png''') 68 println('''«fileNameWithoutExtension».png''')
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
new file mode 100644
index 00000000..f842afb5
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScript.xtend
@@ -0,0 +1,77 @@
1package hu.bme.mit.inf.dslreasoner.run.script
2
3import java.util.List
4import org.eclipse.xtend.lib.annotations.Accessors
5
6@Accessors
7class MeasurementScript {
8 String inputPath
9 String outputPath
10 int timeout
11 boolean saveModels
12 boolean saveTemporaryFiles
13 int warmupIterations
14 int iterations
15 Domain domain
16 Scope scope
17 List<Integer> sizes
18 Solver solver
19 ScopePropagator scopePropagator
20 ScopeConstraints propagatedConstraints
21 PolyhedronSolver polyhedronSolver
22 ScopeHeuristic scopeHeuristic
23
24 def toCsvHeader() {
25 '''«domain»,«scope»,«solver»,«scopePropagator ?: "NULL"»,«propagatedConstraints ?: "NULL"»,«polyhedronSolver ?: "NULL"»,«scopeHeuristic ?: "NULL"»'''
26 }
27}
28
29enum Domain {
30 fs,
31 ecore,
32 ecoreUnsat,
33 Yakindu,
34 YakinduUnsat,
35 FAM,
36 satellite,
37 satelliteUnsat
38}
39
40enum Scope {
41 none,
42 quantiles,
43 upperOnly,
44 unsat,
45 exactly
46}
47
48enum Solver {
49 ViatraSolver,
50 AlloySolver,
51 AlloyMiniSat
52}
53
54enum ScopePropagator {
55 none,
56 basic,
57 polyhedral
58}
59
60enum ScopeConstraints {
61 none,
62 typeHierarchy,
63 relations,
64 hints
65}
66
67enum PolyhedronSolver {
68 Z3Integer,
69 Z3Real,
70 Cbc,
71 Clp
72}
73
74enum ScopeHeuristic {
75 basic,
76 polyhedral
77}
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
new file mode 100644
index 00000000..973c3d13
--- /dev/null
+++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/script/MeasurementScriptRunner.xtend
@@ -0,0 +1,400 @@
1package hu.bme.mit.inf.dslreasoner.run.script
2
3import com.google.gson.Gson
4import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver
5import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
6import hu.bme.mit.inf.dslreasoner.ecore2logic.EClassMapper
7import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
8import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
12import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
14import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral
16import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
19import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
20import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry
21import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
22import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
23import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry
24import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics
25import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry
26import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore
27import hu.bme.mit.inf.dslreasoner.run.EcoreLoader
28import hu.bme.mit.inf.dslreasoner.run.FAMLoader
29import hu.bme.mit.inf.dslreasoner.run.FileSystemLoader
30import hu.bme.mit.inf.dslreasoner.run.MetamodelLoader
31import hu.bme.mit.inf.dslreasoner.run.SatelliteLoader
32import hu.bme.mit.inf.dslreasoner.run.YakinduLoader
33import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil
34import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic
35import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration
36import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints
37import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver
38import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy
39import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic
40import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion
41import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner
42import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration
43import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
44import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
45import java.io.FileReader
46import java.util.HashMap
47import java.util.HashSet
48import java.util.Map
49import java.util.Set
50import org.eclipse.emf.ecore.EObject
51import org.eclipse.emf.ecore.resource.Resource
52import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
53import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup
54import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions
55import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory
56import org.eclipse.xtend.lib.annotations.Data
57import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver
58
59class MeasurementScriptRunner {
60 static val MODEL_SIZE_GAP = 0
61 static val SCOPE_PROPAGATOR_TIMEOUT = 10
62 static val USEC_TO_MSEC = 1000000
63
64 static extension val LogicresultFactory = LogicresultFactory.eINSTANCE
65
66 val MeasurementScript script
67 val ReasonerWorkspace inputWorkspace
68 val ReasonerWorkspace outputWorkspace
69 val MetamodelLoader metamodelLoader
70
71 new(MeasurementScript script) {
72 this.script = script
73 inputWorkspace = new FileSystemWorkspace(script.inputPath + "/", "")
74 outputWorkspace = new FileSystemWorkspace(script.outputPath +
75 "/", '''«script.domain»_«script.solver»_«script.scope»_«script.scopePropagator ?: "na"»_«script.propagatedConstraints ?: "na"»_«script.polyhedronSolver ?: "na"»_«script.scopeHeuristic ?: "na"»_''')
76 metamodelLoader = switch (script.domain) {
77 case fs: new FileSystemLoader(inputWorkspace)
78 case ecore: new EcoreLoader(inputWorkspace)
79 case ecoreUnsat: new EcoreLoader(inputWorkspace, false)
80 case Yakindu: new YakinduLoader(inputWorkspace) => [useSynchronization = false; useComplexStates = true]
81 case YakinduUnsat: new YakinduLoader(inputWorkspace, false) => [useSynchronization = false; useComplexStates = true]
82 case FAM: new FAMLoader(inputWorkspace)
83 case satellite: new SatelliteLoader(inputWorkspace)
84 case satelliteUnsat: new SatelliteLoader(inputWorkspace, false)
85 default: throw new IllegalArgumentException("Unsupported domain: " + script.domain)
86 }
87 }
88
89 def run() {
90 if (script.sizes.empty) {
91 return
92 }
93 val start = System.currentTimeMillis
94 val warmupSize = script.sizes.head
95 for (var int i = 0; i < script.warmupIterations; i++) {
96 System.err.println('''Warmup «i + 1»/«script.warmupIterations»...''')
97 runExperiment(warmupSize)
98 }
99 val warmupEnd = System.currentTimeMillis
100 System.err.println('''Warmup completed in «(warmupEnd - start) / 1000» seconds''')
101 for (size : script.sizes) {
102 var int failures = 0
103 for (var int i = 0; i < script.iterations; i++) {
104 System.err.println("Running GC...")
105 runGc()
106 System.err.println('''Iteration «i + 1»/«script.iterations» of size «size»...''')
107 val startTime = System.currentTimeMillis
108 val result = runExperiment(size)
109 val headerPrefix = '''«script.toCsvHeader»,«size»,«i + 1»,«result.resultName»'''
110 println('''«headerPrefix»,startTime,«startTime»''')
111 println('''«headerPrefix»,logic2SolverTransformationTime,«result.statistics.transformationTime»''')
112 println('''«headerPrefix»,solverTime,«result.statistics.solverTime»''')
113 for (statistic : result.statistics.entries) {
114 val valueString = switch (statistic) {
115 IntStatisticEntry: statistic.value.toString
116 RealStatisticEntry: statistic.value.toString
117 StringStatisticEntry: statistic.value.toString
118 default: statistic.toString
119 }
120 println('''«headerPrefix»,«statistic.name»,«valueString»''')
121 }
122 if (script.saveModels && result.model !== null) {
123 outputWorkspace.writeModel(result.model, '''«size»_«i + 1».xmi''')
124 }
125 if (result.resultName === "InsuficientResourcesResultImpl") {
126 failures++
127 }
128 System.out.flush
129 }
130 if (failures == script.iterations) {
131 System.err.println("All measurements failed")
132 return
133 }
134 }
135 val end = System.currentTimeMillis
136 System.err.println('''Measurement completed in «(end - start) / 1000» seconds''')
137 }
138
139 private static def void runGc() {
140 System.gc
141 Thread.sleep(100)
142 System.gc
143 Thread.sleep(100)
144 System.gc
145 Thread.sleep(800)
146 }
147
148 private def createViatraConfig() {
149 val config = new ViatraReasonerConfiguration
150 config.debugConfiguration.partialInterpretatioVisualiser = null
151 config.searchSpaceConstraints.additionalGlobalConstraints += metamodelLoader.additionalConstraints
152 config.scopePropagatorStrategy = switch (script.scopePropagator) {
153 case none:
154 ScopePropagatorStrategy.None
155 case basic:
156 switch (script.propagatedConstraints) {
157 case none:
158 ScopePropagatorStrategy.Basic
159 case typeHierarchy:
160 ScopePropagatorStrategy.BasicTypeHierarchy
161 case relations,
162 case hints:
163 throw new IllegalArgumentException(
164 "Basic scope propagator does not support relational and hint constraints")
165 default:
166 throw new IllegalArgumentException("Unknown scope constraints: " + script.propagatedConstraints)
167 }
168 case polyhedral: {
169 val constraints = switch (script.propagatedConstraints) {
170 case none:
171 throw new IllegalArgumentException(
172 "Polyhedral scope propagator needs at least type hierarchy constraints")
173 case typeHierarchy:
174 PolyhedralScopePropagatorConstraints.TypeHierarchy
175 case relations,
176 case hints:
177 PolyhedralScopePropagatorConstraints.Relational
178 default:
179 throw new IllegalArgumentException("Unknown scope constraints: " + script.propagatedConstraints)
180 }
181 val polyhedronSolver = switch (script.polyhedronSolver) {
182 case Z3Integer: PolyhedralScopePropagatorSolver.Z3Integer
183 case Z3Real: PolyhedralScopePropagatorSolver.Z3Real
184 case Cbc: PolyhedralScopePropagatorSolver.Cbc
185 case Clp: PolyhedralScopePropagatorSolver.Clp
186 default: throw new IllegalArgumentException("Unknown polyhedron solver: " + script.polyhedronSolver)
187 }
188 val updateHeuristic = script.scopeHeuristic != ScopeHeuristic.basic
189 new ScopePropagatorStrategy.Polyhedral(constraints, polyhedronSolver, updateHeuristic,
190 SCOPE_PROPAGATOR_TIMEOUT)
191 }
192 default:
193 throw new IllegalArgumentException("Unknown scope propagator: " + script.scopePropagator)
194 }
195 config
196 }
197
198 private def createAlloyConfig(AlloyBackendSolver backendSolver) {
199 val config = new AlloySolverConfiguration
200 config.solver = backendSolver
201 config
202 }
203
204 private def createConfig(int modelSize) {
205 val config = switch (solver : script.solver) {
206 case ViatraSolver: createViatraConfig()
207 case AlloySolver: createAlloyConfig(AlloyBackendSolver.SAT4J)
208 case AlloyMiniSat: createAlloyConfig(AlloyBackendSolver.MiniSatJNI)
209 default: throw new IllegalArgumentException("Unknown solver: " + solver)
210 }
211 config.solutionScope.numberOfRequiredSolutions = 1
212 config.runtimeLimit = script.timeout
213 config.documentationLevel = if(script.saveTemporaryFiles) DocumentationLevel.NORMAL else DocumentationLevel.NONE
214 config
215 }
216
217 private def runExperiment(int modelSize) {
218 val config = createConfig(modelSize)
219 val modelLoadingStart = System.nanoTime
220 val metamodelDescriptor = metamodelLoader.loadMetamodel
221 val partialModelDescriptor = metamodelLoader.loadPartialModel
222 val queryDescriptor = metamodelLoader.loadQueries(metamodelDescriptor)
223 val modelLoadingTime = System.nanoTime - modelLoadingStart
224
225 val domain2LogicTransformationStart = System.nanoTime
226 val Ecore2Logic ecore2Logic = new Ecore2Logic
227 val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic)
228 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic
229 var modelGeneration = ecore2Logic.transformMetamodel(metamodelDescriptor, new Ecore2LogicConfiguration())
230 var problem = modelGeneration.output
231 problem = instanceModel2Logic.transform(
232 modelGeneration,
233 partialModelDescriptor
234 ).output
235 problem = viatra2Logic.transformQueries(
236 queryDescriptor,
237 modelGeneration,
238 new Viatra2LogicConfiguration
239 ).output
240 initializeScope(config, modelSize, problem, ecore2Logic, modelGeneration.trace)
241 if (config instanceof ViatraReasonerConfiguration && script.propagatedConstraints == ScopeConstraints.hints) {
242 (config as ViatraReasonerConfiguration).hints = metamodelLoader.getHints(ecore2Logic, modelGeneration.trace)
243 }
244 val domain2LogicTransformationTime = System.nanoTime - domain2LogicTransformationStart
245
246 if (config.documentationLevel != DocumentationLevel.NONE) {
247 outputWorkspace.writeModel(problem, "initial.logicproblem")
248 }
249
250 val solver = switch (solver : script.solver) {
251 case ViatraSolver: new ViatraReasoner
252 case AlloySolver,
253 case AlloyMiniSat: new AlloySolver
254 default: throw new IllegalArgumentException("Unknown solver: " + solver)
255 }
256 val result = solver.solve(problem, config, outputWorkspace)
257 val statistics = result.statistics
258 statistics.entries += createIntStatisticEntry => [
259 name = "modelLoadingTime"
260 value = (modelLoadingTime / USEC_TO_MSEC) as int
261 ]
262 statistics.entries += createIntStatisticEntry => [
263 name = "domain2LogicTransformationTime"
264 value = (domain2LogicTransformationTime / USEC_TO_MSEC) as int
265 ]
266 var EObject modelResult = null
267 if (result instanceof ModelResult) {
268 val intepretations = solver.getInterpretations(result)
269 if (intepretations.size != 1) {
270 throw new IllegalStateException("Expected 1 interpretation, got " + intepretations.size)
271 }
272 var resultTransformationStart = System.nanoTime
273 val logic2Ecore = new Logic2Ecore(ecore2Logic)
274 modelResult = logic2Ecore.transformInterpretation(intepretations.head, modelGeneration.trace)
275 val resultTransformationTime = System.nanoTime - resultTransformationStart
276 statistics.entries += createIntStatisticEntry => [
277 name = "ecore2LogicTransformationTime"
278 value = (resultTransformationTime / USEC_TO_MSEC) as int
279 ]
280 }
281
282 new ExperimentResult(result.class.simpleName, statistics, modelResult)
283 }
284
285 private def initializeScope(LogicSolverConfiguration config, int modelSize, LogicProblem problem,
286 EClassMapper eClassMapper, Ecore2Logic_Trace trace) {
287 val knownElements = initializeKnownElements(problem, config.typeScopes)
288 if (modelSize < 0) {
289 config.typeScopes.minNewElements = 0
290 config.typeScopes.maxNewElements = TypeScopes.Unlimited
291 } else {
292 val numberOfKnownElements = knownElements.values.flatten.toSet.size
293 val newElementCount = modelSize - numberOfKnownElements
294 switch (script.scope) {
295 case upperOnly:
296 config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
297 case exactly: {
298 config.typeScopes.minNewElements = newElementCount
299 config.typeScopes.maxNewElements = newElementCount
300 }
301 default: {
302 config.typeScopes.minNewElements = newElementCount
303 config.typeScopes.maxNewElements = newElementCount + MODEL_SIZE_GAP
304 }
305 }
306 }
307 switch (scope : script.scope) {
308 case none,
309 case exactly:
310 return
311 case quantiles,
312 case unsat,
313 case upperOnly: {
314 val quantiles = if (scope == Scope.unsat) {
315 metamodelLoader.unsatTypeQuantiles
316 } else {
317 metamodelLoader.typeQuantiles
318 }
319 for (eClassInScope : eClassMapper.allClassesInScope(trace)) {
320 val quantile = quantiles.get(eClassInScope.name)
321 if (quantile !== null) {
322 val type = eClassMapper.TypeofEClass(trace, eClassInScope)
323 val knownInstances = knownElements.get(type)
324 val currentCount = if(knownInstances === null) 0 else knownInstances.size
325 val lowCount = Math.floor(modelSize * quantile.low) as int
326 val highCount = Math.ceil((modelSize + MODEL_SIZE_GAP) * quantile.high) as int
327// println('''«type.name» «lowCount» «highCount»''')
328 if (script.scope != Scope.upperOnly) {
329 config.typeScopes.minNewElementsByType.put(type, Math.max(lowCount - currentCount, 0))
330 }
331 config.typeScopes.maxNewElementsByType.put(type, highCount - currentCount)
332 }
333 }
334 }
335 default:
336 throw new IllegalArgumentException("Unknown scope: " + script.scope)
337 }
338 }
339
340 /*
341 * Copied from hu.bme.mit.inf.dslreasoner.application.execution.ScopeLoader.initialiseknownElements(LogicProblem, TypeScopes)
342 */
343 private static def initializeKnownElements(LogicProblem p, TypeScopes s) {
344 val Map<Type, Set<DefinedElement>> res = new HashMap
345
346 // 1. fill map with every types
347 for (t : p.types) {
348 res.put(t, new HashSet)
349 }
350
351 // 2. fill map with every objects
352 for (definedType : p.types.filter(TypeDefinition)) {
353 val supertypes = CollectionsUtil.<Type>transitiveClosureStar(definedType)[supertypes]
354 for (supertype : supertypes) {
355 for (element : definedType.elements) {
356 res.get(supertype).add(element)
357 }
358 }
359 }
360 val partialModelContents = p.annotations.filter(PartialModelRelation2Assertion).map[target].toList.map [
361 eAllContents.toIterable
362 ].flatten.toList
363 s.knownIntegers += partialModelContents.filter(IntLiteral).map[it.value]
364 s.knownReals += partialModelContents.filter(RealLiteral).map[it.value]
365 s.knownStrings += partialModelContents.filter(StringLiteral).map[it.value]
366
367 res
368 }
369
370 public static def void main(String[] args) {
371 if (args.length != 1) {
372 System.err.println("Missing measurement script name.")
373 System.exit(-1)
374 }
375 EMFPatternLanguageStandaloneSetup.doSetup
376 ViatraQueryEngineOptions.setSystemDefaultBackends(ReteBackendFactory.INSTANCE, ReteBackendFactory.INSTANCE,
377 ReteBackendFactory.INSTANCE)
378 Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl)
379 val config = readConfig(args.get(0))
380 val runnner = new MeasurementScriptRunner(config)
381 runnner.run()
382 }
383
384 static def readConfig(String scriptPath) {
385 val gson = new Gson
386 val reader = new FileReader(scriptPath)
387 try {
388 gson.fromJson(reader, MeasurementScript)
389 } finally {
390 reader.close
391 }
392 }
393
394 @Data
395 private static class ExperimentResult {
396 String resultName
397 Statistics statistics
398 EObject model
399 }
400}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-01 17:14:39 +0000