aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Alloy-Solver')
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF24
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml32
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend2
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend6
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch18
5 files changed, 32 insertions, 50 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
index 87ff7abc..b944302b 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF
@@ -4,22 +4,22 @@ Bundle-Name: %pluginName
4Bundle-SymbolicName: hu.bme.mit.inf.dlsreasoner.alloy.reasoner;singleton:=true 4Bundle-SymbolicName: hu.bme.mit.inf.dlsreasoner.alloy.reasoner;singleton:=true
5Bundle-Version: 1.0.0.qualifier 5Bundle-Version: 1.0.0.qualifier
6Bundle-ClassPath: lib/alloy4.2_2015-02-22.jar, 6Bundle-ClassPath: lib/alloy4.2_2015-02-22.jar,
7 . 7 .
8Bundle-Vendor: %providerName 8Bundle-Vendor: %providerName
9Bundle-Localization: plugin 9Bundle-Localization: plugin
10Export-Package: hu.bme.mit.inf.dlsreasoner.alloy.reasoner, 10Export-Package: hu.bme.mit.inf.dlsreasoner.alloy.reasoner,
11 hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder, 11 hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder,
12 hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries 12 hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries
13Require-Bundle: com.google.guava, 13Require-Bundle: com.google.guava,
14 org.eclipse.xtend.lib, 14 org.eclipse.xtend.lib,
15 org.eclipse.xtext.xbase.lib, 15 org.eclipse.xtext.xbase.lib,
16 org.eclipse.core.runtime, 16 org.eclipse.core.runtime,
17 org.eclipse.emf.ecore;visibility:=reexport, 17 org.eclipse.emf.ecore;visibility:=reexport,
18 hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, 18 hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport,
19 hu.bme.mit.inf.dslreasoner.alloy.language;bundle-version="1.0.0", 19 hu.bme.mit.inf.dslreasoner.alloy.language;bundle-version="1.0.0",
20 org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0", 20 org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0",
21 hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", 21 hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0",
22 org.eclipse.viatra.query.runtime;bundle-version="2.0.0" 22 org.eclipse.viatra.query.runtime;bundle-version="2.0.0"
23Import-Package: org.apache.log4j;version="1.2.15" 23Import-Package: org.apache.log4j;version="1.2.15"
24Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner 24Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner
25Bundle-ActivationPolicy: lazy 25Bundle-ActivationPolicy: lazy
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
index 5457d70c..e57b595a 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml
@@ -1,17 +1,17 @@
1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!-- 1<?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!--
2--><plugin> 2--><plugin>
3 <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" point="org.eclipse.viatra.query.runtime.queryspecification"> 3 <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
4 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries"> 4 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.SignatureQueries">
5 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.directSubset"/> 5 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.directSubset"/>
6 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.subset"/> 6 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.subset"/>
7 </group> 7 </group>
8 </extension> 8 </extension>
9 <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" point="org.eclipse.viatra.query.runtime.queryspecification"> 9 <extension id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" point="org.eclipse.viatra.query.runtime.queryspecification">
10 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries"> 10 <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries" id="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries">
11 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.supertype"/> 11 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.supertype"/>
12 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.topmostCommonSubtypes"/> 12 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.topmostCommonSubtypes"/>
13 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowermostCommonSupertype"/> 13 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowermostCommonSupertype"/>
14 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowestCommonSupertypeOfAllOccuranceOfElement"/> 14 <query-specification fqn="hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.lowestCommonSupertypeOfAllOccuranceOfElement"/>
15 </group> 15 </group>
16 </extension> 16 </extension>
17</plugin> 17</plugin>
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
index 432651af..ceb78e99 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend
@@ -57,7 +57,7 @@ class AlloySolver extends LogicReasoner{
57 val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) 57 val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode)
58 alloyConfig.progressMonitor.workedSearchFinished 58 alloyConfig.progressMonitor.workedSearchFinished
59 59
60 val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) 60 val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolutions,result2,forwardTrace,transformationTime)
61 alloyConfig.progressMonitor.workedBackwardTransformationFinished 61 alloyConfig.progressMonitor.workedBackwardTransformationFinished
62 //val solverFinish = System.currentTimeMillis-solverStart 62 //val solverFinish = System.currentTimeMillis-solverStart
63 // Finish: Solving Alloy problem 63 // Finish: Solving Alloy problem
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
index ebbca624..033ced04 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend
@@ -184,7 +184,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
184 } else { 184 } else {
185 lastAnswer = lastAnswer.next 185 lastAnswer = lastAnswer.next
186 } 186 }
187 configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) 187 configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolutions)
188 188
189 val runtime = System.currentTimeMillis -startTime 189 val runtime = System.currentTimeMillis -startTime
190 synchronized(this) { 190 synchronized(this) {
@@ -201,8 +201,8 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
201 } 201 }
202 202
203 def hasEnoughSolution(List<?> answers) { 203 def hasEnoughSolution(List<?> answers) {
204 if(configuration.solutionScope.numberOfRequiredSolution < 0) return false 204 if(configuration.solutionScope.numberOfRequiredSolutions < 0) return false
205 else return answers.size() == configuration.solutionScope.numberOfRequiredSolution 205 else return answers.size() == configuration.solutionScope.numberOfRequiredSolutions
206 } 206 }
207 207
208 public def getPartialAnswers() { 208 public def getPartialAnswers() {
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch
deleted file mode 100644
index 77031bf1..00000000
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch
+++ /dev/null
@@ -1,18 +0,0 @@
1<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2<launchConfiguration type="org.eclipse.emf.mwe2.launch.Mwe2LaunchConfigurationType">
3<stringAttribute key="org.eclipse.debug.core.ATTR_REFRESH_SCOPE" value="${working_set:&lt;?xml version=&quot;1.0&quot; encoding=&quot;UTF-8&quot;?&gt;&#10;&lt;launchConfigurationWorkingSet factoryID=&quot;org.eclipse.ui.internal.WorkingSetFactory&quot; id=&quot;1299248699643_13&quot; label=&quot;working set&quot; name=&quot;working set&quot;&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language.generator&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language.tests&quot; type=&quot;4&quot;/&gt;&#10;&lt;item factoryID=&quot;org.eclipse.ui.internal.model.ResourceFactory&quot; path=&quot;/hu.bme.mit.inf.dslreasoner.alloy.language.ui&quot; type=&quot;4&quot;/&gt;&#10;&lt;/launchConfigurationWorkingSet&gt;}"/>
4<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_PATHS">
5<listEntry value="/hu.bme.mit.inf.dslreasoner.alloy.language"/>
6</listAttribute>
7<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_TYPES">
8<listEntry value="4"/>
9</listAttribute>
10<listAttribute key="org.eclipse.debug.ui.favoriteGroups">
11<listEntry value="org.eclipse.debug.ui.launchGroup.debug"/>
12<listEntry value="org.eclipse.debug.ui.launchGroup.run"/>
13</listAttribute>
14<stringAttribute key="org.eclipse.jdt.launching.MAIN_TYPE" value="org.eclipse.emf.mwe2.launch.runtime.Mwe2Launcher"/>
15<stringAttribute key="org.eclipse.jdt.launching.PROGRAM_ARGUMENTS" value="src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2"/>
16<stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="hu.bme.mit.inf.dslreasoner.alloy.language"/>
17<stringAttribute key="org.eclipse.jdt.launching.VM_ARGUMENTS" value="-Xmx512m"/>
18</launchConfiguration>