3 files changed, 128 insertions, 35 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
index 637752b0..7db9e0ea 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
@@ -6,28 +6,30 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
 class Alloy2LogicMapper {
        val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
        
-        public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
+        public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
-                if(solution == null) {
+                val models = monitoredAlloySolution.aswers.map[it.key].toList
+                
+                if(monitoredAlloySolution.finishedBeforeTimeout) {
                        return createInsuficientResourcesResult => [
                                it.problem = problem
-                                it.statistics = transformStatistics(solution,transformationTime)
+                                it.representation += models
+                                it.trace = trace
+                                it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                        ]
                } else {
-                        val logicResult = solution.solution
+                        if(models.last.satisfiable || requiredNumberOfSolution == -1) {
-                        if(logicResult.satisfiable) {
                                return createModelResult => [
                                        it.problem = problem
-                                        it.representation += solution
+                                        it.representation += models
-                                        it.maxInteger = logicResult.max
-                                        it.minInteger = logicResult.min
                                        it.trace = trace
-                                        it.statistics = transformStatistics(solution,transformationTime)
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                                ]
                        } else {
                                return createInconsistencyResult => [
                                        it.problem = problem
-                                        //trace?
+                                        it.representation += models
-                                        it.statistics = transformStatistics(solution,transformationTime)
+                                        it.trace = trace
+                                        it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
                                ]
                        }
                }
@@ -36,13 +38,29 @@ class Alloy2LogicMapper {
        def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
                createStatistics => [
                        it.transformationTime = transformationTime as int
-                        if(solution != null) {
+                        for(solutionIndex : 0..<solution.aswers.size) {
-                                it.solverTime = solution.runtimeTime as int
+                                val solutionTime = solution.aswers.get(solutionIndex).value
-                                it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [
+                                 it.entries+= createIntStatisticEntry => [
-                                        it.name = "KoodkodToCNFTransformationTime"
+                                        it.name = '''Answer«solutionIndex»Time'''
-                                        it.value = solution.getKodkodTime as int
+                                        it.value = solutionTime.intValue
                                ]
                        }
+                        it.entries+= createIntStatisticEntry => [
+                                it.name = "Alloy2KodKodTransformationTime"
+                                it.value = solution.kodkodTime as int
+                        ]
+                        it.entries+= createIntStatisticEntry => [
+                                it.name = "Alloy2KodKodTransformationTime"
+                                it.value = solution.kodkodTime as int
+                        ]
+                        it.entries+= createStringStatisticEntry => [
+                                it.name = "warnings"
+                                it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
+                        ]
                ]
        }
+        
+        def sum(Iterable<Long> ints) {
+                ints.reduce[p1, p2|p1+p2]
+        }
 }
 \ No newline at end of file
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 6bac4130..17220776 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
@@ -21,6 +21,11 @@ import org.eclipse.emf.common.CommonPlugin
 import java.util.ArrayList
 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
 import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
+import com.google.common.util.concurrent.SimpleTimeLimiter
+import java.util.concurrent.Callable
+import java.util.concurrent.TimeUnit
+import com.google.common.util.concurrent.UncheckedTimeoutException
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
 class AlloySolverException extends Exception{
        new(String s) { super(s) }
@@ -34,9 +39,8 @@ class AlloySolverException extends Exception{
        List<String> warnings
        List<String> debugs
        long kodkodTime
-        long runtimeTime
+        val List<Pair<A4Solution, Long>> aswers
-        
+        val boolean finishedBeforeTimeout
-        A4Solution solution
 }
 class AlloyHandler {
@@ -63,6 +67,7 @@ class AlloyHandler {
                        if(configuration.solver.externalSolver) {
                                it.solverDirectory = configuration.solverPath
                        }
+                        //it.inferPartialInstance
                        it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
                ]
                
@@ -70,8 +75,8 @@ class AlloyHandler {
                var Command command = null;
                var CompModule compModule = null
                
+                // Start: Alloy -> Kodkod
                val kodkodTransformStart = System.currentTimeMillis();
-                
                try {
                        if(configuration.writeToFile) {
                                compModule = CompUtil.parseEverything_fromFile(reporter,null,path)
@@ -85,23 +90,26 @@ class AlloyHandler {
                        throw new AlloySolverException(e.message,warnings,e)
                }
                val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
+                // Finish: Alloy -> Kodkod
                
-                //Execute
+                val limiter = new SimpleTimeLimiter
-                var A4Solution answer = null;
+                val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution)
-                try {
+                var List<Pair<A4Solution, Long>> answers
-                        answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
+                var boolean finished
-                }catch(Exception e) {
+                if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {
-                        warnings +=e.message
+                        answers = callable.call
-                }
+                        finished = true
-                
-                var long runtimeFromAnswer;
-                if(runtime.empty) {
-                        runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish)
                } else {
-                        runtimeFromAnswer = runtime.head
+                        try{
+                                answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)
+                                finished = true
+                        } catch (UncheckedTimeoutException e) {
+                                answers = callable.partialAnswers
+                                finished = false
+                        }
                }
-                
-                return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer)
+                new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)
        }
        
        val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap
@@ -138,6 +146,73 @@ class AlloyHandler {
        }
 }
+class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
+        
+        val List<String> warnings
+        val List<String> debugs
+        val A4Reporter reporter
+        val A4Options options
+        
+        val Command command
+        val CompModule compModule
+        val int numberOfRequiredSolution
+        
+        val List<Pair<A4Solution,Long>> answers = new LinkedList()
+        
+        new(List<String> warnings,
+                List<String> debugs,
+                A4Reporter reporter,
+                A4Options options,
+                Command command,
+                CompModule compModule,
+                int numberOfRequiredSolution)
+        {
+                this.warnings = warnings
+                this.debugs = debugs
+                this.reporter = reporter
+                this.options = options
+                this.command = command
+                this.compModule = compModule
+                this.numberOfRequiredSolution = numberOfRequiredSolution
+        }
+        
+        override call() throws Exception {
+                val startTime = System.currentTimeMillis
+                
+                // Start: Execute
+                var A4Solution lastAnswer = null
+                try {
+                        do{
+                                if(lastAnswer == null) {
+                                        lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
+                                } else {
+                                        lastAnswer = lastAnswer.next
+                                }
+                                
+                                val runtime = System.currentTimeMillis -startTime
+                                synchronized(this) {
+                                        answers += lastAnswer->runtime
+                                }
+                                println( answers.size )
+                        } while(lastAnswer.satisfiable != false && hasEnoughSolution(answers))
+                        
+                }catch(Exception e) {
+                        warnings +=e.message
+                }
+                // Finish: execute
+                return answers
+        }
+        
+        def hasEnoughSolution(List<?> answers) {
+                if(numberOfRequiredSolution < 0) return false
+                else return answers.size < numberOfRequiredSolution
+        }
+        
+        public def getPartialAnswers() {
+                return answers
+        }
+}
 @Data class SolverConfiguration {
        AlloyBackendSolver backedSolver
        String path
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
index 23b9027f..65fdcfdf 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
@@ -277,7 +277,7 @@ class Logic2AlloyLanguageMapper {
                        it.typeScopes+= createALSSigScope => [
                                it.type= typeMapper.getUndefinedSupertype(trace)
                                it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 
-                                //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements)
+                                it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
                        ]
                        if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(
                                '''An integer scope have to be specified for Alloy!''')

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend index 637752b0..7db9e0ea 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend
@@ -6,28 +6,30 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory
6	class Alloy2LogicMapper {	6	class Alloy2LogicMapper {
7	val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE	7	val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE
8		8
9	public def transformOutput(LogicProblem problem, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {	9	public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
10	if(solution == null) {	10	val models = monitoredAlloySolution.aswers.map[it.key].toList
		11
		12	if(monitoredAlloySolution.finishedBeforeTimeout) {
11	return createInsuficientResourcesResult => [	13	return createInsuficientResourcesResult => [
12	it.problem = problem	14	it.problem = problem
13	it.statistics = transformStatistics(solution,transformationTime)	15	it.representation += models
		16	it.trace = trace
		17	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
14	]	18	]
15	} else {	19	} else {
16	val logicResult = solution.solution	20	if(models.last.satisfiable \|\| requiredNumberOfSolution == -1) {
17	if(logicResult.satisfiable) {
18	return createModelResult => [	21	return createModelResult => [
19	it.problem = problem	22	it.problem = problem
20	it.representation += solution	23	it.representation += models
21	it.maxInteger = logicResult.max
22	it.minInteger = logicResult.min
23	it.trace = trace	24	it.trace = trace
24	it.statistics = transformStatistics(solution,transformationTime)	25	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
25	]	26	]
26	} else {	27	} else {
27	return createInconsistencyResult => [	28	return createInconsistencyResult => [
28	it.problem = problem	29	it.problem = problem
29	//trace?	30	it.representation += models
30	it.statistics = transformStatistics(solution,transformationTime)	31	it.trace = trace
		32	it.statistics = transformStatistics(monitoredAlloySolution,transformationTime)
31	]	33	]
32	}	34	}
33	}	35	}
@@ -36,13 +38,29 @@ class Alloy2LogicMapper {
36	def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {	38	def transformStatistics(MonitoredAlloySolution solution, long transformationTime) {
37	createStatistics => [	39	createStatistics => [
38	it.transformationTime = transformationTime as int	40	it.transformationTime = transformationTime as int
39	if(solution != null) {	41	for(solutionIndex : 0..<solution.aswers.size) {
40	it.solverTime = solution.runtimeTime as int	42	val solutionTime = solution.aswers.get(solutionIndex).value
41	it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [	43	it.entries+= createIntStatisticEntry => [
42	it.name = "KoodkodToCNFTransformationTime"	44	it.name = '''Answer«solutionIndex»Time'''
43	it.value = solution.getKodkodTime as int	45	it.value = solutionTime.intValue
44	]	46	]
45	}	47	}
		48	it.entries+= createIntStatisticEntry => [
		49	it.name = "Alloy2KodKodTransformationTime"
		50	it.value = solution.kodkodTime as int
		51	]
		52	it.entries+= createIntStatisticEntry => [
		53	it.name = "Alloy2KodKodTransformationTime"
		54	it.value = solution.kodkodTime as int
		55	]
		56	it.entries+= createStringStatisticEntry => [
		57	it.name = "warnings"
		58	it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]'''
		59	]
46	]	60	]
47	}	61	}
		62
		63	def sum(Iterable<Long> ints) {
		64	ints.reduce[p1, p2\|p1+p2]
		65	}
48	} \ No newline at end of file	66	} \ No newline at end of file


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 6bac4130..17220776 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
@@ -21,6 +21,11 @@ import org.eclipse.emf.common.CommonPlugin
21	import java.util.ArrayList	21	import java.util.ArrayList
22	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument	22	import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
23	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration	23	import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
		24	import com.google.common.util.concurrent.SimpleTimeLimiter
		25	import java.util.concurrent.Callable
		26	import java.util.concurrent.TimeUnit
		27	import com.google.common.util.concurrent.UncheckedTimeoutException
		28	import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
24		29
25	class AlloySolverException extends Exception{	30	class AlloySolverException extends Exception{
26	new(String s) { super(s) }	31	new(String s) { super(s) }
@@ -34,9 +39,8 @@ class AlloySolverException extends Exception{
34	List<String> warnings	39	List<String> warnings
35	List<String> debugs	40	List<String> debugs
36	long kodkodTime	41	long kodkodTime
37	long runtimeTime	42	val List<Pair<A4Solution, Long>> aswers
38		43	val boolean finishedBeforeTimeout
39	A4Solution solution
40	}	44	}
41		45
42	class AlloyHandler {	46	class AlloyHandler {
@@ -63,6 +67,7 @@ class AlloyHandler {
63	if(configuration.solver.externalSolver) {	67	if(configuration.solver.externalSolver) {
64	it.solverDirectory = configuration.solverPath	68	it.solverDirectory = configuration.solverPath
65	}	69	}
		70	//it.inferPartialInstance
66	it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString	71	it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString
67	]	72	]
68		73
@@ -70,8 +75,8 @@ class AlloyHandler {
70	var Command command = null;	75	var Command command = null;
71	var CompModule compModule = null	76	var CompModule compModule = null
72		77
		78	// Start: Alloy -> Kodkod
73	val kodkodTransformStart = System.currentTimeMillis();	79	val kodkodTransformStart = System.currentTimeMillis();
74
75	try {	80	try {
76	if(configuration.writeToFile) {	81	if(configuration.writeToFile) {
77	compModule = CompUtil.parseEverything_fromFile(reporter,null,path)	82	compModule = CompUtil.parseEverything_fromFile(reporter,null,path)
@@ -85,23 +90,26 @@ class AlloyHandler {
85	throw new AlloySolverException(e.message,warnings,e)	90	throw new AlloySolverException(e.message,warnings,e)
86	}	91	}
87	val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart	92	val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
		93	// Finish: Alloy -> Kodkod
88		94
89	//Execute	95	val limiter = new SimpleTimeLimiter
90	var A4Solution answer = null;	96	val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration.solutionScope.numberOfRequiredSolution)
91	try {	97	var List<Pair<A4Solution, Long>> answers
92	answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)	98	var boolean finished
93	}catch(Exception e) {	99	if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) {
94	warnings +=e.message	100	answers = callable.call
95	}	101	finished = true
96
97	var long runtimeFromAnswer;
98	if(runtime.empty) {
99	runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish)
100	} else {	102	} else {
101	runtimeFromAnswer = runtime.head	103	try{
		104	answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true)
		105	finished = true
		106	} catch (UncheckedTimeoutException e) {
		107	answers = callable.partialAnswers
		108	finished = false
		109	}
102	}	110	}
103		111
104	return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer)	112	new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished)
105	}	113	}
106		114
107	val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap	115	val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap
@@ -138,6 +146,73 @@ class AlloyHandler {
138	}	146	}
139	}	147	}
140		148
		149	class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
		150
		151	val List<String> warnings
		152	val List<String> debugs
		153	val A4Reporter reporter
		154	val A4Options options
		155
		156	val Command command
		157	val CompModule compModule
		158	val int numberOfRequiredSolution
		159
		160	val List<Pair<A4Solution,Long>> answers = new LinkedList()
		161
		162	new(List<String> warnings,
		163	List<String> debugs,
		164	A4Reporter reporter,
		165	A4Options options,
		166	Command command,
		167	CompModule compModule,
		168	int numberOfRequiredSolution)
		169	{
		170	this.warnings = warnings
		171	this.debugs = debugs
		172	this.reporter = reporter
		173	this.options = options
		174	this.command = command
		175	this.compModule = compModule
		176	this.numberOfRequiredSolution = numberOfRequiredSolution
		177	}
		178
		179	override call() throws Exception {
		180	val startTime = System.currentTimeMillis
		181
		182	// Start: Execute
		183	var A4Solution lastAnswer = null
		184	try {
		185	do{
		186	if(lastAnswer == null) {
		187	lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options)
		188	} else {
		189	lastAnswer = lastAnswer.next
		190	}
		191
		192	val runtime = System.currentTimeMillis -startTime
		193	synchronized(this) {
		194	answers += lastAnswer->runtime
		195	}
		196	println( answers.size )
		197	} while(lastAnswer.satisfiable != false && hasEnoughSolution(answers))
		198
		199	}catch(Exception e) {
		200	warnings +=e.message
		201	}
		202	// Finish: execute
		203	return answers
		204	}
		205
		206	def hasEnoughSolution(List<?> answers) {
		207	if(numberOfRequiredSolution < 0) return false
		208	else return answers.size < numberOfRequiredSolution
		209	}
		210
		211	public def getPartialAnswers() {
		212	return answers
		213	}
		214	}
		215
141	@Data class SolverConfiguration {	216	@Data class SolverConfiguration {
142	AlloyBackendSolver backedSolver	217	AlloyBackendSolver backedSolver
143	String path	218	String path


diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend index 23b9027f..65fdcfdf 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend
@@ -277,7 +277,7 @@ class Logic2AlloyLanguageMapper {
277	it.typeScopes+= createALSSigScope => [	277	it.typeScopes+= createALSSigScope => [
278	it.type= typeMapper.getUndefinedSupertype(trace)	278	it.type= typeMapper.getUndefinedSupertype(trace)
279	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)	279	it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)
280	//it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements)	280	it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
281	]	281	]
282	if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(	282	if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException(
283	'''An integer scope have to be specified for Alloy!''')	283	'''An integer scope have to be specified for Alloy!''')