diff options
author | 2020-11-04 01:16:22 -0500 | |
---|---|---|
committer | 2020-11-04 01:16:22 -0500 | |
commit | 93243cb3faf1ccd733081fcf380559ac03c9ad35 (patch) | |
tree | 421f9f174eb77c387b5acaa05f01e64a62cab3a7 /Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf | |
parent | add realistic solver (diff) | |
parent | Optimizing generator with linear objective functions (diff) | |
download | VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.tar.gz VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.tar.zst VIATRA-Generator-93243cb3faf1ccd733081fcf380559ac03c9ad35.zip |
merge with current master, comment numerical solver related logging
Diffstat (limited to 'Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf')
16 files changed, 1069 insertions, 364 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage | ||
4 | import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.mutated.Mutated | ||
5 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
6 | import java.io.File | ||
7 | import java.util.ArrayList | ||
8 | import java.util.Collection | ||
9 | import java.util.Comparator | ||
10 | import java.util.HashMap | ||
11 | import java.util.List | ||
12 | import java.util.Map | ||
13 | import java.util.TreeSet | ||
14 | import org.eclipse.emf.ecore.EObject | ||
15 | import org.eclipse.emf.ecore.resource.Resource | ||
16 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
17 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
18 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
19 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | ||
20 | import org.eclipse.viatra.query.runtime.emf.EMFScope | ||
21 | |||
22 | class QueryComparator implements Comparator<IQuerySpecification<?>>{ | ||
23 | |||
24 | override compare(IQuerySpecification<?> arg0, IQuerySpecification<?> arg1) { | ||
25 | arg0.fullyQualifiedName.compareTo(arg1.fullyQualifiedName) | ||
26 | } | ||
27 | } | ||
28 | |||
29 | class 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 | |||
163 | class 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 | |||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy |
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner |
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
27 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation | 27 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser |
28 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 28 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
29 | import java.util.LinkedList | 29 | import java.util.LinkedList |
30 | import java.util.List | 30 | import java.util.List |
@@ -32,9 +32,6 @@ import org.eclipse.emf.ecore.EObject | |||
32 | import org.eclipse.emf.ecore.resource.Resource | 32 | import org.eclipse.emf.ecore.resource.Resource |
33 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 33 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
34 | import org.eclipse.xtend.lib.annotations.Data | 34 | import org.eclipse.xtend.lib.annotations.Data |
35 | import org.eclipse.viatra.query.runtime.api.IQuerySpecification | ||
36 | import java.util.Set | ||
37 | import java.util.Comparator | ||
38 | 35 | ||
39 | enum Metamodel { | 36 | enum 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | ||
2 | |||
3 | import com.google.common.collect.ImmutableMap | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
5 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint | ||
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
10 | import java.util.Map | ||
11 | import org.eclipse.viatra.query.runtime.api.IPatternMatch | ||
12 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
13 | |||
14 | abstract 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..300f8b51 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/FileSystemHint.xtend | |||
@@ -0,0 +1,34 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
7 | import java.util.Map | ||
8 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
9 | |||
10 | class FileSystemHint extends Ecore2LogicTraceBasedHint { | ||
11 | static val REMAINING_CONTENTS_ROOT = "hint_root" | ||
12 | |||
13 | new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { | ||
14 | super(ecore2Logic, trace) | ||
15 | } | ||
16 | |||
17 | override getAdditionalPatterns(PatternGenerator it, Map<String, PQuery> fqnToPQuery) ''' | ||
18 | pattern «REMAINING_CONTENTS_ROOT»(problem:LogicProblem, interpretation:PartialInterpretation, remainingContents:java Integer) { | ||
19 | find interpretation(problem, interpretation); | ||
20 | remainingContents == sum find remainingContents_root_reference_Dir_helper(problem, interpretation, _, #_) | ||
21 | } | ||
22 | ''' | ||
23 | |||
24 | override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) { | ||
25 | val dirCount = createBuilder.add(1, "Dir".type).build | ||
26 | |||
27 | val remainingContentsRootMatcher = createMatcher(REMAINING_CONTENTS_ROOT) | ||
28 | |||
29 | return [ p | | ||
30 | dirCount.tightenLowerBound(remainingContentsRootMatcher.getCount(p)) | ||
31 | ] | ||
32 | } | ||
33 | |||
34 | } | ||
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..9cc6e415 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 | |||
@@ -1,10 +1,10 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | 1 | package hu.bme.mit.inf.dslreasoner.run |
2 | 2 | ||
3 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint |
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
7 | import org.eclipse.viatra.dse.base.ThreadContext | 6 | import org.eclipse.viatra.dse.base.ThreadContext |
7 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | ||
8 | 8 | ||
9 | class FileSystemInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstraint { | 9 | class FileSystemInconsistencyDetector extends ModelGenerationMethodBasedGlobalConstraint { |
10 | var PartialInterpretation partialInterpretation | 10 | var PartialInterpretation partialInterpretation |
@@ -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..cbc692b3 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | 1 | package hu.bme.mit.inf.dslreasoner.run |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage | 3 | import functionalarchitecture.FunctionalarchitecturePackage |
4 | import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Ecore | ||
4 | import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.FileSystem | 5 | import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.FileSystem |
5 | import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FilesystemPackage | 6 | import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.FilesystemPackage |
6 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern | 7 | import hu.bme.mit.inf.dslreasoner.domains.satellite.queries.internal.SatelliteQueriesAll |
8 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | ||
7 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage | 9 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage |
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor |
9 | import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns | 13 | import hu.bme.mit.inf.dslreasoner.partialsnapshot_mavo.yakindu.Patterns |
10 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | 14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor |
11 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint |
16 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | ||
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint |
13 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
14 | import java.util.Collection | 19 | import java.util.Collection |
20 | import java.util.HashMap | ||
15 | import java.util.LinkedHashMap | 21 | import java.util.LinkedHashMap |
16 | import java.util.List | 22 | import java.util.List |
23 | import java.util.Map | ||
17 | import java.util.Set | 24 | import java.util.Set |
18 | import org.eclipse.emf.ecore.EAttribute | 25 | import org.eclipse.emf.ecore.EAttribute |
19 | import org.eclipse.emf.ecore.EClass | 26 | import org.eclipse.emf.ecore.EClass |
@@ -21,61 +28,91 @@ import org.eclipse.emf.ecore.EEnum | |||
21 | import org.eclipse.emf.ecore.EEnumLiteral | 28 | import org.eclipse.emf.ecore.EEnumLiteral |
22 | import org.eclipse.emf.ecore.EObject | 29 | import org.eclipse.emf.ecore.EObject |
23 | import org.eclipse.emf.ecore.EReference | 30 | import org.eclipse.emf.ecore.EReference |
24 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
25 | import java.util.HashMap | ||
26 | import org.eclipse.emf.ecore.EcorePackage | 31 | import org.eclipse.emf.ecore.EcorePackage |
27 | import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Ecore | 32 | import org.eclipse.xtend.lib.annotations.Data |
33 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
34 | import satellite.SatellitePackage | ||
35 | |||
36 | @Data | ||
37 | class TypeQuantiles { | ||
38 | double low | ||
39 | double high | ||
40 | } | ||
28 | 41 | ||
29 | abstract class MetamodelLoader { | 42 | abstract 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 | ||
49 | class FAMLoader extends MetamodelLoader{ | 83 | class 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 | ||
93 | class YakinduLoader extends MetamodelLoader{ | 131 | class 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 | ||
170 | class FileSystemLoader extends MetamodelLoader{ | 249 | class 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 | ||
218 | class EcoreLoader extends MetamodelLoader { | 305 | class 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 | |||
386 | class 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 | |||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic |
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor | 29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.DiversityDescriptor |
29 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy |
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | 31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner |
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
33 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
32 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 34 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
33 | import java.io.BufferedReader | 35 | import java.io.BufferedReader |
34 | import java.io.InputStreamReader | 36 | import java.io.InputStreamReader |
@@ -37,9 +39,6 @@ import org.eclipse.emf.ecore.EObject | |||
37 | import org.eclipse.emf.ecore.resource.Resource | 39 | import org.eclipse.emf.ecore.resource.Resource |
38 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 40 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
39 | import org.junit.Test | 41 | import org.junit.Test |
40 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation | ||
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationSizePrinter | ||
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
43 | 42 | ||
44 | enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy} | 43 | enum UseSolver{Viatra, Smt, ViatraWithSmt, Alloy} |
45 | enum Domain{FAM, Yakindu, FileSystem,Ecore} | 44 | enum 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 | |||
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | 30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy |
31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | 31 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner |
32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | 32 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration |
33 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation | 33 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser |
34 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 34 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
35 | import java.io.BufferedReader | 35 | import java.io.BufferedReader |
36 | import java.io.InputStreamReader | 36 | import java.io.InputStreamReader |
@@ -44,7 +44,6 @@ import org.eclipse.emf.ecore.resource.Resource | |||
44 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 44 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
45 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine | 45 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine |
46 | import org.eclipse.viatra.query.runtime.emf.EMFScope | 46 | import org.eclipse.viatra.query.runtime.emf.EMFScope |
47 | import java.lang.invoke.VolatileCallSite | ||
48 | 47 | ||
49 | enum PartialModelSource { Homeworks, Random } | 48 | enum PartialModelSource { Homeworks, Random } |
50 | enum ValidationTechique {Alloy, Viatra} | 49 | enum 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..9a84f777 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphHint.xtend | |||
@@ -0,0 +1,48 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
7 | import java.util.Map | ||
8 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
9 | |||
10 | class SGraphHint extends Ecore2LogicTraceBasedHint { | ||
11 | new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { | ||
12 | super(ecore2Logic, trace) | ||
13 | } | ||
14 | |||
15 | override getAdditionalPatterns(extension PatternGenerator patternGenerator, Map<String, PQuery> fqnToPQuery) { | ||
16 | "" | ||
17 | } | ||
18 | |||
19 | override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) { | ||
20 | val newEntriesWithoutRegionCount = createBuilder.add(1, "Entry".type).add(-1, "Region".type).build | ||
21 | val newStatesWithoutRegionCount = createBuilder.add(1, "State".type).add(-1, "Region".type).build | ||
22 | val newTransitionWithoutNeedsOutgoingCount = createBuilder.add(1, "Transition".type).add(-1, "Entry".type). | ||
23 | add(-1, "Choice".type).build | ||
24 | val newTransitionWithoutNeedsIncomingCount = createBuilder.add(1, "Transition".type).add(-1, "Choice".type). | ||
25 | build | ||
26 | |||
27 | val regionsWithoutEntryMatcher = createMatcher( | ||
28 | "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noEntryInRegion") | ||
29 | val regionsWithoutStateMatcher = createMatcher( | ||
30 | "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noStateInRegion") | ||
31 | val entryHasNoOutgoingMatcher = createMatcher( | ||
32 | "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_noOutgoingTransitionFromEntry") | ||
33 | val choiceHasNoOutgoingMatcher = createMatcher( | ||
34 | "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoOutgoing") | ||
35 | val choiceHasNoIncomingMatcher = createMatcher( | ||
36 | "unfinishedBy_pattern_hu_bme_mit_inf_dslreasoner_partialsnapshot_mavo_yakindu_choiceHasNoIncoming") | ||
37 | val transitionWithoutTargetMatcher = createMatcher("unfinishedLowerMultiplicity_target_reference_Transition") | ||
38 | |||
39 | return [ p | | ||
40 | newEntriesWithoutRegionCount.assertEqualsTo(regionsWithoutEntryMatcher.countMatches(p)) | ||
41 | newStatesWithoutRegionCount.tightenLowerBound(regionsWithoutStateMatcher.countMatches(p)) | ||
42 | newTransitionWithoutNeedsOutgoingCount.tightenLowerBound( | ||
43 | entryHasNoOutgoingMatcher.countMatches(p) + choiceHasNoOutgoingMatcher.countMatches(p)) | ||
44 | newTransitionWithoutNeedsIncomingCount.tightenLowerBound( | ||
45 | choiceHasNoIncomingMatcher.countMatches(p) - transitionWithoutTargetMatcher.getCount(p)) | ||
46 | ] | ||
47 | } | ||
48 | } | ||
diff --git a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend index 22addd3d..b8167566 100644 --- a/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SGraphInconsistencyDetector.xtend | |||
@@ -1,7 +1,7 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | 1 | package hu.bme.mit.inf.dslreasoner.run |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethod | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint | 5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ModelGenerationMethodBasedGlobalConstraint |
6 | import org.eclipse.viatra.dse.base.ThreadContext | 6 | import org.eclipse.viatra.dse.base.ThreadContext |
7 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher | 7 | import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher |
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..28954d60 --- /dev/null +++ b/Tests/hu.bme.mit.inf.dslreasoner.run/src/hu/bme/mit/inf/dslreasoner/run/SatelliteHint.xtend | |||
@@ -0,0 +1,51 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeExpressionBuilderFactory | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns.PatternGenerator | ||
8 | import java.util.Map | ||
9 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery | ||
10 | |||
11 | class SatelliteHint extends Ecore2LogicTraceBasedHint { | ||
12 | static val INTERFEROMETY_PAYLOAD = "hint_interferometryPayload" | ||
13 | static val REMAINING_CONTENTS_KA_COMM_SUBSYSTEM = "hint_kaCommSubsystem" | ||
14 | |||
15 | new(Ecore2Logic ecore2Logic, Ecore2Logic_Trace trace) { | ||
16 | super(ecore2Logic, trace) | ||
17 | } | ||
18 | |||
19 | override getAdditionalPatterns(PatternGenerator it, Map<String, PQuery> fqnToPQuery) ''' | ||
20 | pattern «INTERFEROMETY_PAYLOAD»(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement) { | ||
21 | find interpretation(problem, interpretation); | ||
22 | find mustExist(problem, interpretation, object); | ||
23 | «typeIndexer.referInstanceOf("InterferometryPayload".type, Modality.MUST, "object")» | ||
24 | } | ||
25 | |||
26 | private pattern «REMAINING_CONTENTS_KA_COMM_SUBSYSTEM»_helper(problem:LogicProblem, interpretation:PartialInterpretation, object:DefinedElement, remainingContents:java Integer) { | ||
27 | find remainingContents_commSubsystem_reference_CommunicatingElement_helper(problem, interpretation, object, remainingContents); | ||
28 | «typeIndexer.referInstanceOf("SmallSat".type, Modality.MUST, "object")» | ||
29 | } | ||
30 | |||
31 | pattern «REMAINING_CONTENTS_KA_COMM_SUBSYSTEM»(problem:LogicProblem, interpretation:PartialInterpretation, remainingContents:java Integer) { | ||
32 | find interpretation(problem, interpretation); | ||
33 | remainingContents == sum find «REMAINING_CONTENTS_KA_COMM_SUBSYSTEM»_helper(problem, interpretation, _, #_); | ||
34 | } | ||
35 | ''' | ||
36 | |||
37 | override createConstraintUpdater(LinearTypeExpressionBuilderFactory it) { | ||
38 | val interferometryPayloadCount = createBuilder.add(1, "InterferometryPayload".type).build | ||
39 | val kaCommSubsystemWithoutSmallSatCount = createBuilder.add(1, "KaCommSubsystem".type).add(-2, "SmallSat".type). | ||
40 | build | ||
41 | |||
42 | val interferometryPayloadMatcher = createMatcher(INTERFEROMETY_PAYLOAD) | ||
43 | val kaCommSubsystemRemainingContentsMatcher = createMatcher(REMAINING_CONTENTS_KA_COMM_SUBSYSTEM) | ||
44 | |||
45 | return [ p | | ||
46 | interferometryPayloadCount.tightenLowerBound(2 - interferometryPayloadMatcher.countMatches(p)) | ||
47 | kaCommSubsystemWithoutSmallSatCount.tightenUpperBound(kaCommSubsystemRemainingContentsMatcher.getCount(p)) | ||
48 | ] | ||
49 | } | ||
50 | |||
51 | } | ||
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..5e2d0920 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,40 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | 1 | package hu.bme.mit.inf.dslreasoner.run |
2 | 2 | ||
3 | import functionalarchitecture.FunctionalarchitecturePackage | ||
4 | import hu.bme.mit.inf.dslreasoner.domains.alloyexamples.Filesystem.Model | ||
5 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | ||
16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | ||
17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
22 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
3 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 23 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
4 | import hu.bme.mit.inf.dslreasomer.domains.transima.fam.FunctionalArchitecture.FunctionalArchitecturePackage | 24 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
25 | import java.util.LinkedHashMap | ||
26 | import java.util.LinkedList | ||
5 | import java.util.List | 27 | import java.util.List |
28 | import org.eclipse.emf.ecore.EAttribute | ||
6 | import org.eclipse.emf.ecore.EClass | 29 | import org.eclipse.emf.ecore.EClass |
7 | import org.eclipse.emf.ecore.EEnumLiteral | ||
8 | import org.eclipse.emf.ecore.EReference | ||
9 | import org.eclipse.emf.ecore.EEnum | 30 | import org.eclipse.emf.ecore.EEnum |
10 | import org.eclipse.emf.ecore.EAttribute | 31 | import org.eclipse.emf.ecore.EEnumLiteral |
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor | ||
12 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
13 | import org.eclipse.emf.ecore.EObject | 32 | import org.eclipse.emf.ecore.EObject |
14 | import java.util.LinkedHashMap | 33 | import org.eclipse.emf.ecore.EReference |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor | ||
16 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
17 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
19 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
22 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod | ||
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.StateCoderStrategy | ||
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | ||
28 | import org.eclipse.emf.ecore.resource.Resource | 34 | import org.eclipse.emf.ecore.resource.Resource |
29 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 35 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
30 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | 36 | import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup |
31 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 37 | import org.eclipse.viatra.query.runtime.rete.matcher.ReteEngine |
32 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | ||
33 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
34 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
35 | import java.util.LinkedList | ||
36 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicStructureBuilder | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | ||
39 | 38 | ||
40 | class SimpleRun { | 39 | class SimpleRun { |
41 | 40 | ||
@@ -59,7 +58,8 @@ class SimpleRun { | |||
59 | 58 | ||
60 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) | 59 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel,new Ecore2LogicConfiguration()) |
61 | val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel) | 60 | val modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem,partialModel) |
62 | val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelGenerationProblem,new Viatra2LogicConfiguration) | 61 | val validModelExtensionProblem = viatra2Logic.transformQueries(queries,modelExtensionProblem,new Viatra2LogicConfiguration) |
62 | // workspace.writeModel(validModelExtensionProblem.output, "generation.logicproblem") | ||
63 | 63 | ||
64 | val logicProblem = validModelExtensionProblem.output | 64 | val logicProblem = validModelExtensionProblem.output |
65 | 65 | ||
@@ -71,11 +71,11 @@ class SimpleRun { | |||
71 | val viatraConfig = new ViatraReasonerConfiguration => [ | 71 | val viatraConfig = new ViatraReasonerConfiguration => [ |
72 | it.typeScopes.maxNewElements = 40 | 72 | it.typeScopes.maxNewElements = 40 |
73 | it.typeScopes.minNewElements = 40 | 73 | it.typeScopes.minNewElements = 40 |
74 | it.solutionScope.numberOfRequiredSolution = 1 | 74 | it.solutionScope.numberOfRequiredSolutions = 1 |
75 | it.existingQueries = queries.patterns.map[it.internalQueryRepresentation] | 75 | // it.scopePropagatorStrategy = ScopePropagatorStrategy.BasicTypeHierarchy |
76 | it.debugCongiguration.logging = false | 76 | it.documentationLevel = DocumentationLevel.NONE |
77 | it.debugCongiguration.partalInterpretationVisualisationFrequency = 1 | 77 | it.debugConfiguration.partalInterpretationVisualisationFrequency = 1 |
78 | it.debugCongiguration.partialInterpretatioVisualiser = new GraphvizVisualisation | 78 | it.debugConfiguration.partialInterpretatioVisualiser = new GraphvizVisualiser |
79 | ] | 79 | ] |
80 | solution = reasoner.solve(logicProblem,viatraConfig,workspace) | 80 | solution = reasoner.solve(logicProblem,viatraConfig,workspace) |
81 | /*/ | 81 | /*/ |
@@ -92,23 +92,20 @@ class SimpleRun { | |||
92 | 92 | ||
93 | println("Problem solved") | 93 | println("Problem solved") |
94 | 94 | ||
95 | val interpretations = reasoner.getInterpretations(solution as ModelResult) | 95 | val result = solution as ModelResult |
96 | val interpretations = reasoner.getInterpretations(result) | ||
96 | val models = new LinkedList | 97 | val models = new LinkedList |
97 | for(interpretation : interpretations) { | 98 | 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) | 99 | val instanceModel = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) |
104 | models+=instanceModel | 100 | models+=instanceModel |
105 | } | 101 | } |
102 | println(result.statistics.solverTime) | ||
106 | 103 | ||
107 | solution.writeSolution(workspace, #[]) | 104 | solution.writeSolution(workspace, #[]) |
108 | } | 105 | } |
109 | 106 | ||
110 | def private static loadMetamodel() { | 107 | def private static loadMetamodel() { |
111 | val pckg = FunctionalArchitecturePackage.eINSTANCE | 108 | val pckg = FunctionalarchitecturePackage.eINSTANCE |
112 | val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList | 109 | val List<EClass> classes = pckg.EClassifiers.filter(EClass).toList |
113 | val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList | 110 | val List<EEnum> enums = pckg.EClassifiers.filter(EEnum).toList |
114 | val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList | 111 | val List<EEnumLiteral> literals = enums.map[ELiterals].flatten.toList |
@@ -118,12 +115,10 @@ class SimpleRun { | |||
118 | } | 115 | } |
119 | 116 | ||
120 | def private static loadQueries(EcoreMetamodelDescriptor metamodel) { | 117 | def private static loadQueries(EcoreMetamodelDescriptor metamodel) { |
121 | val i = hu.bme.mit.inf.dslreasoner.domains.transima.fam.patterns.Pattern.instance | 118 | val i = FamPatterns.instance |
122 | val patterns = i.specifications.toList | 119 | val patterns = i.specifications.toList |
123 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet | 120 | val wfPatterns = patterns.filter[it.allAnnotations.exists[it.name== "Constraint"]].toSet |
124 | val derivedFeatures = new LinkedHashMap | 121 | val derivedFeatures = new LinkedHashMap |
125 | derivedFeatures.put(i.type,metamodel.attributes.filter[it.name == "type"].head) | ||
126 | derivedFeatures.put(i.model,metamodel.references.filter[it.name == "model"].head) | ||
127 | val res = new ViatraQuerySetDescriptor( | 122 | val res = new ViatraQuerySetDescriptor( |
128 | patterns, | 123 | patterns, |
129 | wfPatterns, | 124 | wfPatterns, |
@@ -133,6 +128,8 @@ class SimpleRun { | |||
133 | } | 128 | } |
134 | 129 | ||
135 | def static loadPartialModel(ReasonerWorkspace inputs) { | 130 | def static loadPartialModel(ReasonerWorkspace inputs) { |
131 | EMFPatternLanguageStandaloneSetup.doSetup | ||
132 | ReteEngine.getClass | ||
136 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); | 133 | Resource.Factory.Registry.INSTANCE.getExtensionToFactoryMap().put("*", new XMIResourceFactoryImpl()); |
137 | inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList | 134 | inputs.readModel(EObject,"FAM.xmi").eResource.allContents.toList |
138 | } | 135 | } |
@@ -160,8 +157,4 @@ class SimpleRun { | |||
160 | println("Solution saved and visualised") | 157 | println("Solution saved and visualised") |
161 | } | 158 | } |
162 | } | 159 | } |
163 | |||
164 | def static visualizeSolution() { | ||
165 | |||
166 | } | ||
167 | } \ No newline at end of file | 160 | } \ 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.domains.yakindu.sgraph.yakindumm.YakindummPackage | ||
4 | import java.io.File | ||
5 | import org.eclipse.emf.common.util.URI | ||
6 | import org.eclipse.emf.ecore.EPackage | ||
7 | import org.eclipse.emf.ecore.EcorePackage | ||
8 | import org.eclipse.emf.ecore.resource.Resource | ||
9 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl | ||
10 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
11 | |||
12 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run | 1 | package hu.bme.mit.inf.dslreasoner.run |
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage |
6 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | ||
4 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation |
5 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage | 8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage |
9 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
10 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
6 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 11 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
7 | import java.io.File | 12 | import java.io.File |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguagePackage | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage | ||
10 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage | ||
11 | import org.eclipse.emf.ecore.resource.Resource | 13 | import org.eclipse.emf.ecore.resource.Resource |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
13 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualisation | ||
14 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 14 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
15 | 15 | ||
16 | class VisualiseAllModelInDirectory { | 16 | class 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run.script | ||
2 | |||
3 | import java.util.List | ||
4 | import org.eclipse.xtend.lib.annotations.Accessors | ||
5 | |||
6 | @Accessors | ||
7 | class 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 | |||
29 | enum Domain { | ||
30 | fs, | ||
31 | ecore, | ||
32 | ecoreUnsat, | ||
33 | Yakindu, | ||
34 | YakinduUnsat, | ||
35 | FAM, | ||
36 | satellite, | ||
37 | satelliteUnsat | ||
38 | } | ||
39 | |||
40 | enum Scope { | ||
41 | none, | ||
42 | quantiles, | ||
43 | upperOnly, | ||
44 | unsat, | ||
45 | exactly | ||
46 | } | ||
47 | |||
48 | enum Solver { | ||
49 | ViatraSolver, | ||
50 | AlloySolver, | ||
51 | AlloyMiniSat | ||
52 | } | ||
53 | |||
54 | enum ScopePropagator { | ||
55 | none, | ||
56 | basic, | ||
57 | polyhedral | ||
58 | } | ||
59 | |||
60 | enum ScopeConstraints { | ||
61 | none, | ||
62 | typeHierarchy, | ||
63 | relations, | ||
64 | hints | ||
65 | } | ||
66 | |||
67 | enum PolyhedronSolver { | ||
68 | Z3Integer, | ||
69 | Z3Real, | ||
70 | Cbc, | ||
71 | Clp | ||
72 | } | ||
73 | |||
74 | enum 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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.run.script | ||
2 | |||
3 | import com.google.gson.Gson | ||
4 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolver | ||
5 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EClassMapper | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.IntStatisticEntry | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.Statistics | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry | ||
26 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
27 | import hu.bme.mit.inf.dslreasoner.run.EcoreLoader | ||
28 | import hu.bme.mit.inf.dslreasoner.run.FAMLoader | ||
29 | import hu.bme.mit.inf.dslreasoner.run.FileSystemLoader | ||
30 | import hu.bme.mit.inf.dslreasoner.run.MetamodelLoader | ||
31 | import hu.bme.mit.inf.dslreasoner.run.SatelliteLoader | ||
32 | import hu.bme.mit.inf.dslreasoner.run.YakinduLoader | ||
33 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil | ||
34 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | ||
35 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | ||
36 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorConstraints | ||
37 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.PolyhedralScopePropagatorSolver | ||
38 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy | ||
39 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | ||
40 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partial2logicannotations.PartialModelRelation2Assertion | ||
41 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasoner | ||
42 | import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.ViatraReasonerConfiguration | ||
43 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | ||
44 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
45 | import java.io.FileReader | ||
46 | import java.util.HashMap | ||
47 | import java.util.HashSet | ||
48 | import java.util.Map | ||
49 | import java.util.Set | ||
50 | import org.eclipse.emf.ecore.EObject | ||
51 | import org.eclipse.emf.ecore.resource.Resource | ||
52 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | ||
53 | import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup | ||
54 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions | ||
55 | import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory | ||
56 | import org.eclipse.xtend.lib.annotations.Data | ||
57 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver | ||
58 | |||
59 | class 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 | } | ||