1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
package ca.mcgill.ecse.dslreasoner.vampire.icse;
import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
import functionalarchitecture.Function;
import functionalarchitecture.FunctionalArchitectureModel;
import functionalarchitecture.FunctionalOutput;
import functionalarchitecture.FunctionalarchitecturePackage;
import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;
import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;
import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor;
import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation;
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;
import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;
import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2PartialInterpretation;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml;
import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation;
import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser;
import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.resource.Resource;
import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;
import org.eclipse.xtend2.lib.StringConcatenation;
import org.eclipse.xtext.xbase.lib.Exceptions;
import org.eclipse.xtext.xbase.lib.InputOutput;
import org.eclipse.xtext.xbase.lib.IteratorExtensions;
import org.eclipse.xtext.xbase.lib.ObjectExtensions;
import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
@SuppressWarnings("all")
public class FAMTest {
public static void main(final String[] args) {
try {
final Ecore2Logic ecore2Logic = new Ecore2Logic();
final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic);
final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);
final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();
final InstanceModel2PartialInterpretation im2pi = new InstanceModel2PartialInterpretation();
StringConcatenation _builder = new StringConcatenation();
_builder.append("initialModels/");
final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");
StringConcatenation _builder_1 = new StringConcatenation();
_builder_1.append("output/FAMTest/");
final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");
workspace.initAndClear();
final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;
final Map<String, Object> map = reg.getExtensionToFactoryMap();
XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();
map.put("logicproblem", _xMIResourceFactoryImpl);
InputOutput.<String>println("Input and output workspaces are created");
final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);
final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi");
final Object queries = null;
InputOutput.<String>println("DSL loaded");
Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
LogicProblem problem = modelGenerationProblem.getOutput();
problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();
workspace.writeModel(problem, "Fam.logicproblem");
InputOutput.<String>println("Problem created");
long startTime = System.currentTimeMillis();
VampireSolver reasoner = null;
VampireSolver _vampireSolver = new VampireSolver();
reasoner = _vampireSolver;
final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
classMapMin.put(FunctionalOutput.class, Integer.valueOf(3));
final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
classMapMax.put(FunctionalArchitectureModel.class, Integer.valueOf(3));
classMapMax.put(Function.class, Integer.valueOf(5));
classMapMax.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(3));
classMapMax.put(FunctionalOutput.class, Integer.valueOf(4));
final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
it.documentationLevel = DocumentationLevel.FULL;
it.typeScopes.minNewElements = 4;
it.typeScopes.maxNewElements = 5;
it.contCycleLevel = 5;
it.uniquenessDuplicates = false;
};
final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);
LogicResult solution = reasoner.solve(problem, vampireConfig, workspace);
List<? extends LogicModelInterpretation> interpretations = reasoner.getInterpretations(((ModelResult) solution));
for (final LogicModelInterpretation interpretation : interpretations) {
{
final EObject model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.getTrace());
workspace.writeModel(model, "model.xmi");
final PartialInterpretation representation = im2pi.transform(modelGenerationProblem, IteratorExtensions.<EObject>toList(model.eAllContents()), false);
if ((representation instanceof PartialInterpretation)) {
final PartialInterpretation2Gml vis1 = new PartialInterpretation2Gml();
final String gml = vis1.transform(representation);
workspace.writeText("model.gml", gml);
final GraphvizVisualiser vis2 = new GraphvizVisualiser();
final PartialInterpretationVisualisation dot = vis2.visualiseConcretization(representation);
dot.writeToFile(workspace, "model.png");
} else {
InputOutput.<String>println("ERROR");
}
}
}
long _currentTimeMillis = System.currentTimeMillis();
long _minus = (_currentTimeMillis - startTime);
long totalTimeMin = (_minus / 60000);
long _currentTimeMillis_1 = System.currentTimeMillis();
long _minus_1 = (_currentTimeMillis_1 - startTime);
long _divide = (_minus_1 / 1000);
long totalTimeSec = (_divide % 60);
InputOutput.<String>println("Problem solved");
InputOutput.<String>println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec)));
} catch (Throwable _e) {
throw Exceptions.sneakyThrow(_e);
}
}
}
|
