aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder
diff options
context:
space:
mode:
authorLibravatar 20001LastOrder <boqi.chen@mail.mcgill.ca>2020-11-04 01:33:58 -0500
committerLibravatar 20001LastOrder <boqi.chen@mail.mcgill.ca>2020-11-04 01:33:58 -0500
commita20af4d0dbf5eab84ee271d426528aabb5a8ac3b (patch)
treea9ab772ee313125aaf3a941d66e131b408d949ba /Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder
parentchanges in settings of measurements (diff)
parentmerge with current master, comment numerical solver related logging (diff)
downloadVIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.gz
VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.tar.zst
VIATRA-Generator-a20af4d0dbf5eab84ee271d426528aabb5a8ac3b.zip
fix merging issue
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder')
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend2
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend22
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend2
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend63
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend11
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend13
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend6
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend44
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend212
9 files changed, 290 insertions, 85 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 2efd6b29..328ca176 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
@@ -9,7 +9,7 @@ class Alloy2LogicMapper {
9 public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { 9 public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) {
10 val models = monitoredAlloySolution.aswers.map[it.key].toList 10 val models = monitoredAlloySolution.aswers.map[it.key].toList
11 11
12 if(!monitoredAlloySolution.finishedBeforeTimeout) { 12 if(models.empty || !monitoredAlloySolution.finishedBeforeTimeout) {
13 return createInsuficientResourcesResult => [ 13 return createInsuficientResourcesResult => [
14 it.problem = problem 14 it.problem = problem
15 it.representation += models 15 it.representation += models
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..451aad6e 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
@@ -1,7 +1,5 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder 1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2 2
3import com.google.common.util.concurrent.SimpleTimeLimiter
4import com.google.common.util.concurrent.UncheckedTimeoutException
5import edu.mit.csail.sdg.alloy4.A4Reporter 3import edu.mit.csail.sdg.alloy4.A4Reporter
6import edu.mit.csail.sdg.alloy4.Err 4import edu.mit.csail.sdg.alloy4.Err
7import edu.mit.csail.sdg.alloy4.ErrorWarning 5import edu.mit.csail.sdg.alloy4.ErrorWarning
@@ -23,7 +21,11 @@ import java.util.LinkedList
23import java.util.List 21import java.util.List
24import java.util.Map 22import java.util.Map
25import java.util.concurrent.Callable 23import java.util.concurrent.Callable
24import java.util.concurrent.ExecutionException
25import java.util.concurrent.ExecutorService
26import java.util.concurrent.Executors
26import java.util.concurrent.TimeUnit 27import java.util.concurrent.TimeUnit
28import java.util.concurrent.TimeoutException
27import org.eclipse.xtend.lib.annotations.Data 29import org.eclipse.xtend.lib.annotations.Data
28 30
29class AlloySolverException extends Exception{ 31class AlloySolverException extends Exception{
@@ -46,7 +48,7 @@ class AlloyHandler {
46 48
47 //val fileName = "problem.als" 49 //val fileName = "problem.als"
48 50
49 public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { 51 def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) {
50 52
51 //Prepare 53 //Prepare
52 val warnings = new LinkedList<String> 54 val warnings = new LinkedList<String>
@@ -87,7 +89,6 @@ class AlloyHandler {
87 val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart 89 val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart
88 // Finish: Alloy -> Kodkod 90 // Finish: Alloy -> Kodkod
89 91
90 val limiter = new SimpleTimeLimiter
91 val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) 92 val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration)
92 var List<Pair<A4Solution, Long>> answers 93 var List<Pair<A4Solution, Long>> answers
93 var boolean finished 94 var boolean finished
@@ -95,10 +96,13 @@ class AlloyHandler {
95 answers = callable.call 96 answers = callable.call
96 finished = true 97 finished = true
97 } else { 98 } else {
99 val ExecutorService executor = Executors.newCachedThreadPool();
100 val future = executor.submit(callable)
98 try{ 101 try{
99 answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) 102 answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS)
100 finished = true 103 finished = true
101 } catch (UncheckedTimeoutException e) { 104 } catch (TimeoutException | InterruptedException | ExecutionException e) {
105 future.cancel(true)
102 answers = callable.partialAnswers 106 answers = callable.partialAnswers
103 finished = false 107 finished = false
104 } 108 }
@@ -184,7 +188,7 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
184 } else { 188 } else {
185 lastAnswer = lastAnswer.next 189 lastAnswer = lastAnswer.next
186 } 190 }
187 configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) 191 configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolutions)
188 192
189 val runtime = System.currentTimeMillis -startTime 193 val runtime = System.currentTimeMillis -startTime
190 synchronized(this) { 194 synchronized(this) {
@@ -201,8 +205,8 @@ class AlloyCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{
201 } 205 }
202 206
203 def hasEnoughSolution(List<?> answers) { 207 def hasEnoughSolution(List<?> answers) {
204 if(configuration.solutionScope.numberOfRequiredSolution < 0) return false 208 if(configuration.solutionScope.numberOfRequiredSolutions < 0) return false
205 else return answers.size() == configuration.solutionScope.numberOfRequiredSolution 209 else return answers.size() == configuration.solutionScope.numberOfRequiredSolutions
206 } 210 }
207 211
208 public def getPartialAnswers() { 212 public def getPartialAnswers() {
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
index 107aa001..bbee35fc 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -117,7 +117,7 @@ class AlloyModelInterpretation implements LogicModelInterpretation{
117 for(atom: allAtoms) { 117 for(atom: allAtoms) {
118 val typeName = getName(atom.type) 118 val typeName = getName(atom.type)
119 val atomName = atom.name 119 val atomName = atom.name
120 println(atom.toString + " < - " + typeName) 120 //println(atom.toString + " < - " + typeName)
121 if(typeName == forwardTrace.logicLanguage.name) { 121 if(typeName == forwardTrace.logicLanguage.name) {
122 this.logicLanguage = atom 122 this.logicLanguage = atom
123 } else if(typeName == "Int" || typeName == "seq/Int") { 123 } else if(typeName == "Int" || typeName == "seq/Int") {
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
index 8019c6b5..ac75b2a1 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
@@ -1,20 +1,73 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder 1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2 2
3import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar 3import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
4import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
5import java.util.Map
6import edu.mit.csail.sdg.alloy4compiler.ast.Sig 4import edu.mit.csail.sdg.alloy4compiler.ast.Sig
7import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field 5import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field
6import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration 9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
10import java.util.ArrayList
10import java.util.List 11import java.util.List
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory 12import java.util.Map
13
14import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
12 15
13class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ 16class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{
14 protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE 17 protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE
15 18
16 override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String, Sig> name2AlloySig, Map<String, Field> name2AlloyField, Map<String, DefinedElement> expression2DefinedElement, Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) { 19 override resolveUnknownAtoms(
17 throw new UnsupportedOperationException("TODO: auto-generated method stub") 20 Iterable<ExprVar> objectAtoms,
21 A4Solution solution,
22 Logic2AlloyLanguageMapperTrace forwardTrace,
23 Map<String, Sig> name2AlloySig,
24 Map<String, Field> name2AlloyField,
25 Map<String,DefinedElement> expression2DefinedElement,
26 Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)
27 {
28 /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap()
29 val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/
30
31 val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
32
33 // 1. Evaluate the defined elements
34 for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) {
35 val name = definedElementMappingEntry.value.name
36 val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
37 val elementsOfSingletonSignature = solution.eval(matchingSig)
38 if(elementsOfSingletonSignature.size != 1) {
39 throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''')
40 } else {
41 val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar
42 expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key)
43 }
44 }
45
46 // 2. evaluate the signatures and create new elements if necessary
47 for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) {
48 val type = type2SingatureEntry.key
49 if(type instanceof TypeDeclaration) {
50 val name = type2SingatureEntry.value.name
51 val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)
52 val elementsOfSignature = solution.eval(matchingSig)
53 val elementList = new ArrayList(elementsOfSignature.size)
54 var newVariableIndex = 1;
55 for(elementOfSignature : elementsOfSignature) {
56 val expressionOfDefinedElement = elementOfSignature.atom(0)
57 if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) {
58 elementList += expressionOfDefinedElement.lookup(expression2DefinedElement)
59 } else {
60 val newElementName = '''newObject «newVariableIndex.toString»'''
61 val newRepresentation = createDefinedElement => [
62 it.name = newElementName
63 ]
64 elementList += newRepresentation
65 expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation)
66 }
67 }
68 interpretationOfUndefinedType.put(type,elementList)
69 }
70 }
18 } 71 }
19 72
20} \ No newline at end of file 73} \ 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/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 3fc3971d..e1ffe531 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
@@ -194,13 +194,12 @@ class Logic2AlloyLanguageMapper {
194 val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) 194 val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace)
195 val type = relation.type 195 val type = relation.type
196 196
197 if(type instanceof ALSDirectProduct) {
198 type.rightMultiplicit = type.rightMultiplicit.addUpper
199 } else {
200 relation.multiplicity = relation.multiplicity.addUpper
201 }
202
203 if(assertion.upper === 1) { 197 if(assertion.upper === 1) {
198 if(type instanceof ALSDirectProduct) {
199 type.rightMultiplicit = type.rightMultiplicit.addUpper
200 } else {
201 relation.multiplicity = relation.multiplicity.addUpper
202 }
204 return true 203 return true
205 } else { 204 } else {
206 return transformAssertion(assertion.target,trace) 205 return transformAssertion(assertion.target,trace)
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
index 0762efce..8de9688b 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend
@@ -133,11 +133,11 @@ class Logic2AlloyLanguageMapper_RelationMapper {
133 public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { 133 public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) {
134 if(relation.parameters.size === 2) { 134 if(relation.parameters.size === 2) {
135 /** 1. Create a relation that can be used in ^relation expressions */ 135 /** 1. Create a relation that can be used in ^relation expressions */
136 val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) 136 val declaration = this.createRelationDeclaration(support.toID('''AsDeclaration «relation.name»'''),relation.parameters,trace)
137 trace.relationInTransitiveToHosterField.put(relation,declaration) 137 trace.relationInTransitiveToHosterField.put(relation,declaration)
138 /** 2. Add fact that the declaration corresponds to the definition */ 138 /** 2. Add fact that the declaration corresponds to the definition */
139 val fact = createALSFactDeclaration => [ 139 val fact = createALSFactDeclaration => [
140 it.name = '''EqualsAsDeclaration «relation.name»''' 140 it.name = support.toID('''EqualsAsDeclaration «relation.name»''')
141 it.term = createALSQuantifiedEx => [ 141 it.term = createALSQuantifiedEx => [
142 val a = createALSVariableDeclaration => [ 142 val a = createALSVariableDeclaration => [
143 it.name = "a" 143 it.name = "a"
@@ -157,7 +157,7 @@ class Logic2AlloyLanguageMapper_RelationMapper {
157 it.params += createALSReference => [ it.referred = b ] 157 it.params += createALSReference => [ it.referred = b ]
158 ] 158 ]
159 it.rightOperand = createALSSubset => [ 159 it.rightOperand = createALSSubset => [
160 it.leftOperand = createALSJoin => [ 160 it.leftOperand = createALSDirectProduct => [
161 it.leftOperand = createALSReference => [ referred = a ] 161 it.leftOperand = createALSReference => [ referred = a ]
162 it.rightOperand = createALSReference => [ referred = b ] 162 it.rightOperand = createALSReference => [ referred = b ]
163 ] 163 ]
@@ -183,12 +183,15 @@ class Logic2AlloyLanguageMapper_RelationMapper {
183 rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] 183 rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ]
184 ] 184 ]
185 } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ 185 } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){
186 createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] 186 createALSJoin => [
187 leftOperand = createALSReference => [referred = trace.logicLanguage]
188 rightOperand = createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ]
189 ]
187 } else { 190 } else {
188 throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') 191 throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''')
189 } 192 }
190 return createALSSubset => [ 193 return createALSSubset => [
191 it.leftOperand = createALSJoin => [ 194 it.leftOperand = createALSDirectProduct => [
192 it.leftOperand = source 195 it.leftOperand = source
193 it.rightOperand = target 196 it.rightOperand = target
194 ] 197 ]
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
index 397fb84b..3379ba20 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -123,8 +123,8 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL
123 // 7. Each type is in the intersection of the supertypes 123 // 7. Each type is in the intersection of the supertypes
124 for(type : types.filter[it.supertypes.size>=2]) { 124 for(type : types.filter[it.supertypes.size>=2]) {
125 trace.specification.factDeclarations += createALSFactDeclaration => [ 125 trace.specification.factDeclarations += createALSFactDeclaration => [
126 it.name = support.toIDMultiple("abstract",type.name) 126 it.name = support.toIDMultiple("supertypeIsInIntersection",type.name)
127 it.term = createALSEquals => [ 127 it.term = createALSSubset => [
128 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] 128 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
129 it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| 129 it.rightOperand = support.unfoldIntersection(type.supertypes.map[e|
130 createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) 130 createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]])
@@ -135,7 +135,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL
135 // 8. Each abstract type is equal to the union of the subtypes 135 // 8. Each abstract type is equal to the union of the subtypes
136 for(type : types.filter[isIsAbstract]) { 136 for(type : types.filter[isIsAbstract]) {
137 trace.specification.factDeclarations += createALSFactDeclaration => [ 137 trace.specification.factDeclarations += createALSFactDeclaration => [
138 it.name = support.toIDMultiple("abstract",type.name) 138 it.name = support.toIDMultiple("abstractIsUnion",type.name)
139 it.term = createALSEquals => [ 139 it.term = createALSEquals => [
140 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] 140 it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ]
141 it.rightOperand = support.unfoldPlus(type.subtypes.map[e| 141 it.rightOperand = support.unfoldPlus(type.subtypes.map[e|
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend
new file mode 100644
index 00000000..a270cb73
--- /dev/null
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeScopeMapping.xtend
@@ -0,0 +1,44 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
6
7interface Logic2AlloyLanguageMapper_TypeScopeMapping {
8 def void addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
9 def void addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace)
10}
11
12class Logic2AlloyLanguageMapper_AsConstraint implements Logic2AlloyLanguageMapper_TypeScopeMapping {
13 val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
14 val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
15 val Logic2AlloyLanguageMapper_TypeMapper typeMapper
16
17 new(Logic2AlloyLanguageMapper_TypeMapper mapper) {
18 this.typeMapper = mapper
19 }
20
21 override addLowerMultiplicity(ALSDocument document, Type type, int lowerMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
22 document.factDeclarations += createALSFactDeclaration => [
23 it.name = support.toID(#["LowerMultiplicity",support.toID(type.name),lowerMultiplicty.toString])
24 it.term = createALSLeq => [
25 it.leftOperand = createALSCardinality => [
26 it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
27 ]
28 it.rightOperand = createALSNumberLiteral => [it.value = lowerMultiplicty]
29 ]
30 ]
31 }
32
33 override addUpperMultiplicity(ALSDocument document, Type type, int upperMultiplicty, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
34 document.factDeclarations += createALSFactDeclaration => [
35 it.name = support.toID(#["UpperMultiplicity",support.toID(type.name),upperMultiplicty.toString])
36 it.term = createALSMeq => [
37 it.leftOperand = createALSCardinality => [
38 it.operand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
39 ]
40 it.rightOperand = createALSNumberLiteral => [it.value = upperMultiplicty]
41 ]
42 ]
43 }
44} \ 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/RunCommandMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
index 3e96f7f4..b74017d8 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend
@@ -3,25 +3,30 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration 3import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument 4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt 5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumberLiteral
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRunCommand
8import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSString
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm 9import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory 10import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
8import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration 11import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition 13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
10import java.util.LinkedList
11import java.util.List 14import java.util.List
12 15
13import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
14 17
15class RunCommandMapper { 18class RunCommandMapper {
16 private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE 19 val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
17 private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; 20 val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
18 private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; 21 val Logic2AlloyLanguageMapper_TypeMapper typeMapper;
22 val Logic2AlloyLanguageMapper_TypeScopeMapping typeScopeMapping;
19 23
20 public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { 24 new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) {
21 this.typeMapper = typeMapper 25 this.typeMapper = typeMapper
26 this.typeScopeMapping = new Logic2AlloyLanguageMapper_AsConstraint(typeMapper)
22 } 27 }
23 28
24 def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) 29 def transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config)
25 { 30 {
26 //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size 31 //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size
27 32
@@ -36,28 +41,47 @@ class RunCommandMapper {
36 it.term = support.unfoldAnd(equals) 41 it.term = support.unfoldAnd(equals)
37 ] 42 ]
38 } 43 }
39 val typeScopes = new LinkedList 44
40 for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { 45 /*
41 val key = definedScope.key 46 val upperLimits = new LinkedList
42 val amount = definedScope.value 47 val lowerLimits = new LinkedList
43 val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount 48
44 49 /*val typesWithScopeConstraint = config.typeScopes.maxNewElementsByType.keySet + config.typeScopes.minNewElementsByType.keySet
45 val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet 50 for(type : typesWithScopeConstraint) {
46 if(amount == 0 && exactly) { 51 val max = if(config.typeScopes.maxNewElementsByType.containsKey(type)) {
47 specification.factDeclarations += createALSFactDeclaration => [ 52 config.typeScopes.maxNewElementsByType.get(type)
48 it.term = createALSEquals => [ 53 } else {
49 it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) 54 LogicSolverConfiguration::Unlimited
50 it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) 55 }
51 ] 56 val min = if(config.typeScopes.minNewElementsByType.containsKey(type)) {
57 config.typeScopes.minNewElementsByType.get(type)
58 } else {
59 0
60 }
61
62 val exactly = min === max
63
64 if(max === 0) {
65 val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
66 specification.factDeclarations += createALSFactDeclaration => [
67 it.term = createALSEquals => [
68 it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(type,mapper,trace).map[t|createALSReference => [it.referred = t]].toList)
69 it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList )
52 ] 70 ]
53 } 71 ]
54 val int n = existing.size-amount 72 } else if(max !== LogicSolverConfiguration::Unlimited) {
55 typeScopes += createALSSigScope => [ 73 upperLimits += createALSSigScope => [
56 it.type = typeMapper.transformTypeReference(key,mapper,trace).head 74 it.type = typeMapper.transformTypeReference(type,mapper,trace).head
57 it.number = n 75 it.number = max
58 it.exactly =exactly 76 it.exactly =exactly
59 ] 77 ]
78 } else {
79 // do nothing
80 }
81 if(min != 0 && ! exactly) {
82 lowerLimits += type->min
60 } 83 }
84 }*/
61 85
62 specification.runCommand = createALSRunCommand => [ 86 specification.runCommand = createALSRunCommand => [
63 it.typeScopes+= createALSSigScope => [ 87 it.typeScopes+= createALSSigScope => [
@@ -65,41 +89,119 @@ class RunCommandMapper {
65 it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) 89 it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace)
66 it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) 90 it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements)
67 ] 91 ]
68 if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { 92
69 val integersUsed = specification.eAllContents.filter(ALSInt) 93 ]
70 if(integersUsed.empty) { 94
71 // If no integer scope is defined, but the problem has no integers 95 for(upperLimit : config.typeScopes.maxNewElementsByType.entrySet) {
72 // => scope can be empty 96 val type = upperLimit.key
73 it.typeScopes+= createALSIntScope => [ 97 val limit = upperLimit.value + getExistingCount(type)
74 it.number = 0 98 if(limit != LogicSolverConfiguration::Unlimited) {
75 ] 99 this.typeScopeMapping.addUpperMultiplicity(specification,type,limit,mapper,trace)
76 } else { 100 }
77 // If no integer scope is defined, and the problem has integers 101 }
78 // => error 102
79 throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') 103 for(lowerLimit : config.typeScopes.minNewElementsByType.entrySet) {
80 } 104 val type = lowerLimit.key
81 } else { 105 val limit = lowerLimit.value + getExistingCount(type)
82 it.typeScopes += createALSIntScope => [ 106 if(limit != 0) {
83 if(config.typeScopes.knownIntegers.empty) { 107 this.typeScopeMapping.addLowerMultiplicity(specification,type,limit,mapper,trace)
84 number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2)
85 } else {
86 var scope = Math.max(
87 Math.abs(config.typeScopes.knownIntegers.max),
88 Math.abs(config.typeScopes.knownIntegers.min))
89 if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) {
90 scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2
91 }
92 number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1
93 }
94 ]
95 } 108 }
96 if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { 109 }
97 throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') 110
111 setIntegerScope(specification,config,specification.runCommand)
112 setStringScope(specification,config,specification.runCommand)
113 }
114
115 private def getExistingCount(Type type) {
116 val existing = type.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet
117 existing.size
118 }
119
120 protected def Boolean setStringScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand it) {
121 if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) {
122 throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
123 } else {
124 if(config.typeScopes.maxNewStrings == 0) {
125 it.typeScopes += createALSStringScope => [it.number = 0]
98 } else { 126 } else {
99 if(config.typeScopes.maxNewStrings != 0) { 127 if(specification.eAllContents.filter(ALSString).empty) {
100 it.typeScopes += createALSStringScope => [it.number = 0] 128 it.typeScopes += createALSStringScope => [it.number = 0]
129 } else {
130 throw new UnsupportedOperationException('''A string scope have to be specified for Alloy!''')
101 } 131 }
102 } 132 }
103 ] 133 }
134 }
135
136 protected def setIntegerScope(ALSDocument specification, AlloySolverConfiguration config, ALSRunCommand command) {
137 //AlloySolverConfiguration config, ALSRunCommand it
138
139 // If the scope is unlimited ...
140 if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) {
141 val integersUsed = specification.eAllContents.filter(ALSInt)
142 if(integersUsed.empty) {
143 // ... but the problem has no integers => scope can be empty
144 command.typeScopes+= createALSIntScope => [ it.number = 0 ]
145 } else {
146 // If no integer scope is defined, and the problem has integers => error
147 throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''')
148 }
149 } else {
150 // If the scope is limited, collect the integers in the problem and the scope,...
151 //val maxIntScope = config.typeScopes.maxNewIntegers
152 //val minIntScope = config.typeScopes.minNewIntegers
153 val knownIntegers = config.typeScopes.knownIntegers
154 val minKnownInteger = if(knownIntegers.empty) { Integer.MAX_VALUE } else { knownIntegers.min }
155 val maxKnownInteger = if(knownIntegers.empty) { Integer.MIN_VALUE } else { knownIntegers.max }
156 val integersInProblem = specification.eAllContents.filter(ALSNumberLiteral).map[it.value].toList
157 val minIntegerInProblem = if(integersInProblem.empty) { Integer.MAX_VALUE } else { integersInProblem.min }
158 val maxIntegerInProblem = if(integersInProblem.empty) { Integer.MIN_VALUE } else { integersInProblem.max }
159 // And select the range of integers
160 val min = #[minKnownInteger,minIntegerInProblem].min
161 val max = #[maxKnownInteger,maxIntegerInProblem].max
162 //val abs = Math.max(Math.abs(min),Math.abs(max))
163
164
165 command.typeScopes += createALSIntScope => [
166 it.number = toBits(min, max)
167 ]
168 }
169
170// if(config.typeScopes.knownIntegers.empty) {
171// return Integer.SIZE-Integer.numberOfLeadingZeros((config.typeScopes.maxNewIntegers+1)/2)
172// } else {
173// var scope = Math.max(
174// Math.abs(config.typeScopes.knownIntegers.max),
175// Math.abs(config.typeScopes.knownIntegers.min))
176// if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) {
177// scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2
178// }
179// return Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1
180// }
181 }
182
183 private static def toBits(int min, int max) {
184 // 4 Int = {-8, ..., 7}
185 // x Int = {- (2^(x-1)) , ... , 2^(x-1)-1}
186 var int bits = 1
187 // range = 2^(x-1)
188 var int range = 1
189 while((!(-range <= min)) || (!(max <= range-1))) {
190 bits++
191 range*=2
192 }
193 return bits
104 } 194 }
195//
196// def static void main(String[] args) {
197// println('''0,0->«toBits(0,0)»''')
198// println('''1,1->«toBits(1,1)»''')
199// println('''-1,-1->«toBits(-1,-1)»''')
200// println('''5,6->«toBits(5,6)»''')
201// println('''0,6->«toBits(0,6)»''')
202// println('''-10,0->«toBits(-10,0)»''')
203// println('''-8,7->«toBits(-8,7)»''')
204// println('''-100,100->«toBits(-100,100)»''')
205// println('''-300,300->«toBits(-300,300)»''')
206// }
105} \ No newline at end of file 207} \ No newline at end of file
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-08 12:07:21 +0000