From 32a4f3392a7d0c44439c0c9b960ef1cfb5e3cc2f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 25 Oct 2019 04:15:39 -0400 Subject: VAMPIRE: post-submission push --- .../.classpath | 12 + .../.gitignore | 4 + .../.project | 40 ++ ...ry.patternlanguage.emf.EMFPatternLanguage.prefs | 29 ++ .../.settings/org.eclipse.jdt.core.prefs | 7 + ...ry.patternlanguage.emf.EMFPatternLanguage.prefs | 29 ++ .../META-INF/MANIFEST.MF | 26 ++ .../build.properties | 11 + .../lib/alloy4.2_2015-02-22.jar_GoesHere.txt | 1 + .../plugin.properties | 4 + .../plugin.xml | 17 + .../alloy/reasoner/queries/signatureQueries.vql | 17 + .../alloy/reasoner/queries/typeQueries.vql | 85 ++++ .../reasoner/AlloyAnalyzerConfiguration.xtend | 28 ++ .../dlsreasoner/alloy/reasoner/AlloySolver.xtend | 91 ++++ .../alloy/reasoner/builder/Alloy2LogicMapper.xtend | 66 +++ .../alloy/reasoner/builder/AlloyHandler.xtend | 228 ++++++++++ .../builder/AlloyModelInterpretation.xtend | 249 +++++++++++ ...loyModelInterpretation_TypeInterpretation.xtend | 21 + ...retation_TypeInterpretation_FilteredTypes.xtend | 72 +++ ...peInterpretation_InheritanceAndHorizontal.xtend | 20 + .../builder/Logic2AlloyLanguageMapper.xtend | 491 +++++++++++++++++++++ .../builder/Logic2AlloyLanguageMapperTrace.xtend | 56 +++ .../Logic2AlloyLanguageMapper_ConstantMapper.xtend | 43 ++ .../Logic2AlloyLanguageMapper_Containment.xtend | 260 +++++++++++ .../Logic2AlloyLanguageMapper_FunctionMapper.xtend | 87 ++++ .../Logic2AlloyLanguageMapper_RelationMapper.xtend | 199 +++++++++ .../Logic2AlloyLanguageMapper_Support.xtend | 207 +++++++++ .../Logic2AlloyLanguageMapper_TypeMapper.xtend | 18 + ...guageMapper_TypeMapperTrace_FilteredTypes.xtend | 15 + ..._TypeMapperTrace_InheritanceAndHorizontal.xtend | 15 + ...oyLanguageMapper_TypeMapper_FilteredTypes.xtend | 263 +++++++++++ ...apper_TypeMapper_InheritanceAndHorizontal.xtend | 122 +++++ .../alloy/reasoner/builder/RunCommandMapper.xtend | 105 +++++ .../unused/AlloyModelInterpretation.xtend_ | 212 +++++++++ .../unused/FunctionWithTimeout.xtend_ | 40 ++ .../unused/Logic2AlloyApiMapper.xtend_ | 345 +++++++++++++++ .../unused/oldTypes | 74 ++++ 38 files changed, 3609 insertions(+) create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/lib/alloy4.2_2015-02-22.jar_GoesHere.txt create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ create mode 100644 Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes (limited to 'Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner') diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath new file mode 100644 index 00000000..494c050c --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath @@ -0,0 +1,12 @@ + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore new file mode 100644 index 00000000..e42fe9ea --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore @@ -0,0 +1,4 @@ +/bin/ +/src-gen/ +/vql-gen/ +/xtend-gen/ \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project new file mode 100644 index 00000000..6f6a3130 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project @@ -0,0 +1,40 @@ + + + hu.bme.mit.inf.dlsreasoner.alloy.reasoner + + + + + + org.eclipse.viatra.query.tooling.core.projectbuilder + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + + org.eclipse.pde.PluginNature + org.eclipse.jdt.core.javanature + org.eclipse.xtext.ui.shared.xtextNature + org.eclipse.viatra.query.projectnature + + diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs new file mode 100644 index 00000000..1555fd84 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs @@ -0,0 +1,29 @@ +BuilderConfiguration.is_project_specific=true +autobuilding=true +eclipse.preferences.version=1 +generateGeneratedAnnotation=false +generateSuppressWarnings=true +generatedAnnotationComment= +includeDateInGenerated=false +outlet.DEFAULT_OUTPUT.cleanDirectory=false +outlet.DEFAULT_OUTPUT.cleanupDerived=true +outlet.DEFAULT_OUTPUT.createDirectory=true +outlet.DEFAULT_OUTPUT.derived=true +outlet.DEFAULT_OUTPUT.directory=./viatra-gen +outlet.DEFAULT_OUTPUT.hideLocalSyntheticVariables=true +outlet.DEFAULT_OUTPUT.installDslAsPrimarySource=false +outlet.DEFAULT_OUTPUT.keepLocalHistory=true +outlet.DEFAULT_OUTPUT.override=true +outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.queries.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.queries.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.src-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.src-gen.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.src.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.src.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.ignore= +outlet.DEFAULT_OUTPUT.userOutputPerSourceFolder= +targetJavaVersion=JAVA5 +useJavaCompilerCompliance=true diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..0c68a61d --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,7 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.8 diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs new file mode 100644 index 00000000..e346b3ed --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs @@ -0,0 +1,29 @@ +BuilderConfiguration.is_project_specific=true +autobuilding=true +eclipse.preferences.version=1 +generateGeneratedAnnotation=false +generateSuppressWarnings=true +generatedAnnotationComment= +includeDateInGenerated=false +outlet.DEFAULT_OUTPUT.cleanDirectory=true +outlet.DEFAULT_OUTPUT.cleanupDerived=true +outlet.DEFAULT_OUTPUT.createDirectory=true +outlet.DEFAULT_OUTPUT.derived=true +outlet.DEFAULT_OUTPUT.directory=./vql-gen +outlet.DEFAULT_OUTPUT.hideLocalSyntheticVariables=true +outlet.DEFAULT_OUTPUT.installDslAsPrimarySource=false +outlet.DEFAULT_OUTPUT.keepLocalHistory=true +outlet.DEFAULT_OUTPUT.override=true +outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.ecore-gen.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.queries.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.queries.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.src.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.src.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.viatra-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.viatra-gen.ignore= +outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.directory= +outlet.DEFAULT_OUTPUT.sourceFolder.xtend-gen.ignore= +outlet.DEFAULT_OUTPUT.userOutputPerSourceFolder= +targetJavaVersion=JAVA5 +useJavaCompilerCompliance=true diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF new file mode 100644 index 00000000..87ff7abc --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF @@ -0,0 +1,26 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: %pluginName +Bundle-SymbolicName: hu.bme.mit.inf.dlsreasoner.alloy.reasoner;singleton:=true +Bundle-Version: 1.0.0.qualifier +Bundle-ClassPath: lib/alloy4.2_2015-02-22.jar, + . +Bundle-Vendor: %providerName +Bundle-Localization: plugin +Export-Package: hu.bme.mit.inf.dlsreasoner.alloy.reasoner, + hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder, + hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries +Require-Bundle: com.google.guava, + org.eclipse.xtend.lib, + org.eclipse.xtext.xbase.lib, + org.eclipse.core.runtime, + org.eclipse.emf.ecore;visibility:=reexport, + hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, + hu.bme.mit.inf.dslreasoner.alloy.language;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.3.0", + hu.bme.mit.inf.dslreasoner.ecore2logic;bundle-version="1.0.0", + org.eclipse.viatra.query.runtime;bundle-version="2.0.0" +Import-Package: org.apache.log4j;version="1.2.15" +Automatic-Module-Name: hu.bme.mit.inf.dlsreasoner.alloy.reasoner +Bundle-ActivationPolicy: lazy +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties new file mode 100644 index 00000000..a406415f --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties @@ -0,0 +1,11 @@ +bin.includes = .,\ + META-INF/,\ + plugin.xml,\ + plugin.properties +jars.compile.order = . +source.. = src/,\ + queries/,\ + xtend-gen/,\ + vql-gen/,\ + src-gen/ +output.. = bin/ diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/lib/alloy4.2_2015-02-22.jar_GoesHere.txt b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/lib/alloy4.2_2015-02-22.jar_GoesHere.txt new file mode 100644 index 00000000..0df6fddc --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/lib/alloy4.2_2015-02-22.jar_GoesHere.txt @@ -0,0 +1 @@ +Download alloy4.2_2015-02-22.jar from http://alloy.mit.edu/alloy/downloads/alloy4.2_2015-02-22.jar and place here. \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties new file mode 100644 index 00000000..8a902309 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties @@ -0,0 +1,4 @@ +# + +pluginName = AlloyLanguage Model +providerName = www.example.org diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml new file mode 100644 index 00000000..e57b595a --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml @@ -0,0 +1,17 @@ + + + + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql new file mode 100644 index 00000000..5b04960e --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql @@ -0,0 +1,17 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries + +import epackage "http://www.bme.hu/mit/inf/dslreasoner/AlloyLanguage" + +pattern directSubset(x: ALSSignatureDeclaration, y: ALSSignatureDeclaration) { + ALSSignatureBody.declarations(b,y); + ALSSignatureBody.supertype(b,x); +} or { + ALSSignatureBody.declarations(b,y); + ALSSignatureBody.superset(b,x); +} + +pattern subset(x: ALSSignatureDeclaration, y: ALSSignatureDeclaration) { + x == y; +} or { + find directSubset+(x,y); +} diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql new file mode 100644 index 00000000..9847b60a --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql @@ -0,0 +1,85 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries + +import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" + +private pattern supertypeEdge(type1: Type, type2: Type) { + Type.supertypes(type1,type2); +} + +pattern supertype(type1: Type, type2: Type) { + type1 == type2; +} or { + find supertypeEdge+(type1,type2); +} + +private pattern commonSubtype(type1: Type, type2: Type, common: Type) { + find supertype(common,type1); + find supertype(common,type2); +} + +private pattern commonSupertype(type1: Type, type2: Type, common: Type) { + find supertype(common,type1); + find supertype(common,type2); +} + +private pattern hasHigherCommonSubtype(type1: Type, type2: Type, common: Type, higher: Type) { + find supertype(higher,type1); + find supertype(higher,type2); + Type.supertypes(common,higher); + higher != common; +} + +private pattern hasLowerCommonSupertype(type1: Type, type2: Type, common: Type, lower: Type) { + find supertype(type1,lower); + find supertype(type2,lower); + Type.supertypes(lower,common); + lower != common; +} + +pattern topmostCommonSubtypes(type1: Type, type2: Type, common: Type) { + find commonSubtype(type1, type2, common); + neg find hasHigherCommonSubtype(type1, type2, common, _); +} + +pattern lowermostCommonSupertype(type1: Type, type2: Type, common: Type) { + find commonSupertype(type1, type2, common); + neg find hasLowerCommonSupertype(type1, type2, common, _); +} +/*pattern topmostCommonSubtypesInObject(type1: Type, type2: Type, common: Type) { + find commonSubtype(type1, type2, common); + neg find supertypeEdge(type1,_); + neg find supertypeEdge(type2,_); + neg find hasHigherCommonSubtype(type1, type2, common, _); +} +pattern topmostCommonSubtypesInType(in: Type, type1: Type, type2: Type, common: Type) { + find commonSubtype(type1, type2, common); + find supertypeEdge(type1,in); + find supertypeEdge(type2,in); + neg find hasHigherCommonSubtype(type1, type2, common, _); +} + */ + +pattern lowestCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type) { + find typeContainsAllOccuranceOfElement(element,type); + neg find hasLowerCommonSupertypeOfAllOccuranceOfElement(element, type, _); +} + +private pattern hasLowerCommonSupertypeOfAllOccuranceOfElement(element: DefinedElement, type: Type, lower: Type) { + find typeContainsAllOccuranceOfElement(element, type); + find typeContainsAllOccuranceOfElement(element, lower); + find supertype(lower, type); + type != lower; +} + +private pattern typeContainsAllOccuranceOfElement(element: DefinedElement, type: Type) { + find supertype(containerType,type); + TypeDefinition.elements(containerType,element); + neg find typeDoesNotCoverElementOccurance(element,type,_); +} + +private pattern typeDoesNotCoverElementOccurance(element: DefinedElement, type: Type, uncoveredOccurance: TypeDefinition) { + find supertype(containerType,type); + TypeDefinition.elements(containerType,element); + TypeDefinition.elements(uncoveredOccurance,element); + neg find supertype(uncoveredOccurance,type); +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend new file mode 100644 index 00000000..b16ed27f --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend @@ -0,0 +1,28 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration + +class AlloySolverConfiguration extends LogicSolverConfiguration { + public var int symmetry = 20 // by default + public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J + public var TypeMappingTechnique typeMapping = TypeMappingTechnique.InheritanceAndHorizontal + public var randomise = 0 +} + +enum AlloyBackendSolver { + BerkMinPIPE, + SpearPIPE, + MiniSatJNI, + MiniSatProverJNI, + LingelingJNI, + PLingelingJNI, + GlucoseJNI, + CryptoMiniSatJNI, + SAT4J, + CNF, + KodKod +} + +enum TypeMappingTechnique { + FilteredTypes, InheritanceAndHorizontal +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend new file mode 100644 index 00000000..9cfa7391 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend @@ -0,0 +1,91 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner + +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Alloy2LogicMapper +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyHandler +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapperTrace +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes +import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage +import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace + +class AlloySolver extends LogicReasoner{ + + new() { + AlloyLanguagePackage.eINSTANCE.eClass + val x = new AlloyLanguageStandaloneSetupGenerated + x.createInjectorAndDoEMFRegistration + } + + val Logic2AlloyLanguageMapper forwardMapper = new Logic2AlloyLanguageMapper(new Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes) + val AlloyHandler handler = new AlloyHandler + val Alloy2LogicMapper backwardMapper = new Alloy2LogicMapper + + val fileName = "problem.als" + + override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { + val alloyConfig = configuration.asConfig + val writeFile = ( + configuration.documentationLevel===DocumentationLevel::NORMAL || + configuration.documentationLevel===DocumentationLevel::FULL) + + // Start: Logic -> Alloy mapping + val transformationStart = System.currentTimeMillis + val result = forwardMapper.transformProblem(problem,alloyConfig) + val alloyProblem = result.output + val forwardTrace = result.trace + + //var String fileURI = null; + var String alloyCode = workspace.writeModelToString(alloyProblem,fileName) + if(writeFile) { + workspace.writeModel(alloyProblem,fileName) + } + val transformationTime = System.currentTimeMillis - transformationStart + alloyConfig.progressMonitor.workedForwardTransformation + // Finish: Logic -> Alloy mapping + + // Start: Solving Alloy problem + //val solverStart = System.currentTimeMillis + val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,alloyCode) + alloyConfig.progressMonitor.workedSearchFinished + + val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) + alloyConfig.progressMonitor.workedBackwardTransformationFinished + //val solverFinish = System.currentTimeMillis-solverStart + // Finish: Solving Alloy problem + + //logicResult.statistics = + + return logicResult + } + + def asConfig(LogicSolverConfiguration configuration) { + if(configuration instanceof AlloySolverConfiguration) { + return configuration + } else { + throw new IllegalArgumentException('''The configuration has to be an «AlloySolverConfiguration.simpleName»!''') + } + } + + override getInterpretations(ModelResult modelResult) { + //val answers = (modelResult.representation as MonitoredAlloySolution).aswers.map[key] + val sols = modelResult.representation// as List + //val res = answers.map + sols.map[ + new AlloyModelInterpretation( + forwardMapper.typeMapper.typeInterpreter, + it as A4Solution, + forwardMapper, + modelResult.trace as Logic2AlloyLanguageMapperTrace + ) + ] + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend new file mode 100644 index 00000000..09b67599 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend @@ -0,0 +1,66 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory + +class Alloy2LogicMapper { + val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE + + public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, MonitoredAlloySolution monitoredAlloySolution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { + val models = monitoredAlloySolution.aswers.map[it.key].toList + + if(!monitoredAlloySolution.finishedBeforeTimeout) { + return createInsuficientResourcesResult => [ + it.problem = problem + it.representation += models + it.trace = trace + it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) + ] + } else { + if(models.last.satisfiable || requiredNumberOfSolution == -1) { + return createModelResult => [ + it.problem = problem + it.representation += models + it.trace = trace + it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) + ] + } else { + return createInconsistencyResult => [ + it.problem = problem + it.representation += models + it.trace = trace + it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) + ] + } + } + } + + def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { + createStatistics => [ + it.transformationTime = transformationTime as int + for(solutionIndex : 0.. [ + it.name = '''Answer«solutionIndex»Time''' + 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 ints) { + ints.reduce[p1, p2|p1+p2] + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend new file mode 100644 index 00000000..eee2d649 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend @@ -0,0 +1,228 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import edu.mit.csail.sdg.alloy4.A4Reporter +import edu.mit.csail.sdg.alloy4.Err +import edu.mit.csail.sdg.alloy4.ErrorWarning +import edu.mit.csail.sdg.alloy4compiler.ast.Command +import edu.mit.csail.sdg.alloy4compiler.parser.CompModule +import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil +import edu.mit.csail.sdg.alloy4compiler.translator.A4Options +import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.ArrayList +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +import java.util.concurrent.Callable +import java.util.concurrent.ExecutionException +import java.util.concurrent.ExecutorService +import java.util.concurrent.Executors +import java.util.concurrent.TimeUnit +import java.util.concurrent.TimeoutException +import org.eclipse.xtend.lib.annotations.Data + +class AlloySolverException extends Exception{ + new(String s) { super(s) } + new(String s, Exception e) { super(s,e) } + new(String s, List errors, Exception e) { + super(s + '\n' + errors.join('\n'), e) + } +} + +@Data class MonitoredAlloySolution{ + List warnings + List debugs + long kodkodTime + val List> aswers + val boolean finishedBeforeTimeout +} + +class AlloyHandler { + + //val fileName = "problem.als" + + def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration,String alloyCode) { + + //Prepare + val warnings = new LinkedList + val debugs = new LinkedList + val runtime = new ArrayList + val reporter = new A4Reporter() { + override debug(String message) { debugs += message } + override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } + override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } + override warning(ErrorWarning msg) { warnings += msg.message } + } + + val options = new A4Options() => [ + it.symmetry = configuration.symmetry + it.noOverflow = true + it.solver = getSolver(configuration.solver, configuration) + if(configuration.solver.externalSolver) { + it.solverDirectory = configuration.solverPath + } + //it.inferPartialInstance + //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString + ] + + // Transform + var Command command = null; + var CompModule compModule = null + + // Start: Alloy -> Kodkod + val kodkodTransformStart = System.currentTimeMillis(); + try { + compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) + if(compModule.allCommands.size != 1) + throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') + command = compModule.allCommands.head + } catch (Err e){ + throw new AlloySolverException(e.message,warnings,e) + } + val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart + // Finish: Alloy -> Kodkod + + val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) + var List> answers + var boolean finished + if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { + answers = callable.call + finished = true + } else { + val ExecutorService executor = Executors.newCachedThreadPool(); + val future = executor.submit(callable) + try{ + answers = future.get(configuration.runtimeLimit,TimeUnit.SECONDS) + finished = true + } catch (TimeoutException ex) { + // handle the timeout + } catch (InterruptedException e) { + // handle the interrupts + } catch (ExecutionException e) { + // handle other exceptions + } finally { + future.cancel(true); + + answers = callable.partialAnswers + finished = false + } + } + + new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) + } + + val static Map previousSolverConfigurations = new HashMap + def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { + val config = new SolverConfiguration(backedSolver,path,options) + if(previousSolverConfigurations.containsKey(config)) { + return previousSolverConfigurations.get(config) + } else { + val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' + val newSolver = A4Options.SatSolver.make(id,id,path,options) + previousSolverConfigurations.put(config,newSolver) + return newSolver + } + } + + def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { + switch(backedSolver){ + case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE + case SpearPIPE: return A4Options.SatSolver.SpearPIPE + case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI + case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI + case LingelingJNI: return A4Options.SatSolver.LingelingJNI + case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) + case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI + case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI + case SAT4J: return A4Options.SatSolver.SAT4J + case CNF: return A4Options.SatSolver.CNF + case KodKod: return A4Options.SatSolver.KK + } + } + + def isExternalSolver(AlloyBackendSolver backedSolver) { + return !(backedSolver == AlloyBackendSolver.SAT4J) + } +} + +class AlloyCallerWithTimeout implements Callable>>{ + + val List warnings + val List debugs + val A4Reporter reporter + val A4Options options + + val Command command + val CompModule compModule + val AlloySolverConfiguration configuration + + val List> answers = new LinkedList() + + new(List warnings, + List debugs, + A4Reporter reporter, + A4Options options, + Command command, + CompModule compModule, + AlloySolverConfiguration configuration) + { + this.warnings = warnings + this.debugs = debugs + this.reporter = reporter + this.options = options + this.command = command + this.compModule = compModule + this.configuration = configuration + } + + override call() throws Exception { + val startTime = System.currentTimeMillis + + // Start: Execute + var A4Solution lastAnswer = null + try { + if(!configuration.progressMonitor.isCancelled) { + do{ + if(lastAnswer == null) { + lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) + } else { + lastAnswer = lastAnswer.next + } + configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) + + val runtime = System.currentTimeMillis -startTime + synchronized(this) { + answers += (lastAnswer->runtime) + } + } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) + + } + }catch(Exception e) { + warnings +=e.message + } + // Finish: execute + return answers + } + + def hasEnoughSolution(List answers) { + if(configuration.solutionScope.numberOfRequiredSolution < 0) return false + else return answers.size() == configuration.solutionScope.numberOfRequiredSolution + } + + public def getPartialAnswers() { + return answers + } +} + +@Data class SolverConfiguration { + AlloyBackendSolver backedSolver + String path + String[] options +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend new file mode 100644 index 00000000..dcb4bb32 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend @@ -0,0 +1,249 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar +import edu.mit.csail.sdg.alloy4compiler.ast.Sig +import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import java.util.Arrays +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +import java.util.Set +import java.util.SortedSet +import java.util.TreeSet + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class AlloyModelInterpretation implements LogicModelInterpretation{ + + protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE + protected val AlloyModelInterpretation_TypeInterpretation typeInterpretator + + protected val Logic2AlloyLanguageMapper forwardMapper + protected val Logic2AlloyLanguageMapperTrace forwardTrace; + + private var ExprVar logicLanguage; + + private var String logicBooleanTrue; + private var String logicBooleanFalse; + private SortedSet integerAtoms = new TreeSet + private SortedSet stringAtoms = new TreeSet + + private val Map alloyAtom2LogicElement = new HashMap + private val Map> interpretationOfUndefinedType = new HashMap + + private val Map constant2Value + private val Map> function2Value + private val Map> relation2Value + + //private val int minInt + //private val int maxInt + + public new (AlloyModelInterpretation_TypeInterpretation typeInterpretator, A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { + this.typeInterpretator = typeInterpretator + this.forwardMapper = forwardMapper + this.forwardTrace = trace + + // Maps to trace language elements to the parsed problem. + val Map name2AlloySig = new HashMap + val Map name2AlloyField = new HashMap + // exploring signatures + for(sig:solution.allReachableSigs) { + name2AlloySig.put(sig.label,sig) + for(field : sig.fields) { + name2AlloyField.put(field.label,field) + } + } + val unknownAtoms = collectUnknownAndResolveKnownAtoms(solution) + this.typeInterpretator.resolveUnknownAtoms( + unknownAtoms, + solution, + forwardTrace, + name2AlloySig, + name2AlloyField, + alloyAtom2LogicElement, + interpretationOfUndefinedType) + + // eval consants + constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[ + solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term + ] + // eval functions + val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function | + newHashMap( + solution.eval(function.name.lookup(name2AlloyField)) + .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])] + + val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function | + val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField) + val paramIndexes = 1..(function.parameters.size) + return newHashMap( + solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t | + new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term]) + -> + t.atom(function.parameters.size + 1).atomLabel2Term + ])] + this.function2Value = Union(hostedfunction2Value,globalfunction2Value) + // eval relations + val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation | + solution.eval(relation.name.lookup(name2AlloyField)).map[ t | + new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet] + val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation | + solution.eval(relation.name.lookup(name2AlloyField)).map[ t | + new ParameterSubstitution((1.. collectUnknownAndResolveKnownAtoms(A4Solution solution) { + val Iterable allAtoms = solution.allAtoms + val List unknownAtoms = new LinkedList + + for(atom: allAtoms) { + val typeName = getName(atom.type) + val atomName = atom.name + println(atom.toString + " < - " + typeName) + if(typeName == forwardTrace.logicLanguage.name) { + this.logicLanguage = atom + } else if(typeName == "Int" || typeName == "seq/Int") { + val value = Integer.parseInt(atomName.join) + this.integerAtoms.add(value) + } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { + if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } + else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} + else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') + } else if(typeName == "String") { + val value = parseString(atomName.join) + this.stringAtoms.add(value) + } else { + unknownAtoms += atom + } + } + val integerSignature = solution.allReachableSigs.filter[it.label=="Int"].head + for(i : solution.eval(integerSignature)) { + val value = Integer.parseInt(i.atom(0)) + this.integerAtoms.add(value) + } + val stringSignature = solution.allReachableSigs.filter[it.label=="String"].head + for(i : solution.eval(stringSignature)) { + val value = parseString(i.atom(0)) + this.stringAtoms.add(value) + } + return unknownAtoms + } + + def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { + val name = type.toString + if(name.startsWith("{this/") && name.endsWith("}")) { + return type.toString.replaceFirst("\\{this\\/","").replace("}","") + } + else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') + } + def private getName(ExprVar atom) { atom.toString.split("\\$") } + + def print(Logic2AlloyLanguageMapperTrace trace) { + println('''Undefined-----''') + interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v.map[name]»''')] + //println('''Defined-----''') + //trace.type2ALSType.keySet.filter(TypeDefinition).forEach[println('''«it.name» -> «it.elements.map[name.join]»''')] + + println('''Constants-----''') + constant2Value.forEach[k, v|println('''«k.name» : «v»''')] + println('''Functions-----''') + function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]] + println('''Relations-----''') + relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]] + } + + override getElements(Type type) { getElementsDispatch(type) } + def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) } + def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } + + override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { + val transformedParams = new ParameterSubstitution(parameterSubstitution) + return transformedParams.lookup( + function.lookup(this.function2Value) + ) + } + + override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { + relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution)) + } + + override getInterpretation(ConstantDeclaration constant) { + constant.lookup(this.constant2Value) + } + + // Alloy term -> logic term + def private atomLabel2Term(String label) { + if(label.number) return Integer.parseInt(label) + else if(label == this.logicBooleanTrue) return true + else if(label == this.logicBooleanFalse) return false + else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) + else if(label.isString) return parseString(label) + else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') + } + def private isNumber(String s) { + try{ + Integer.parseInt(s) + return true + }catch(NumberFormatException e) { + return false + } + } + def private isString(String label) { + label.startsWith("\"") && label.endsWith("\"") + } + def private parseString(String label) { + label.substring(1,label.length-1) + } + + override getAllIntegersInStructure() { + this.integerAtoms + } + + override getAllRealsInStructure() { + new TreeSet + } + + override getAllStringsInStructure() { + this.stringAtoms + } +} + +/** + * Helper class for efficiently matching parameter substitutions for functions and relations. + */ +class ParameterSubstitution{ + val Object[] data; + + new(Object[] data) { this.data = data } + + override equals(Object obj) { + if(obj === this) return true + else if(obj == null) return false + if(obj instanceof ParameterSubstitution) { + return Arrays.equals(this.data,obj.data) + } + return false + } + + override hashCode() { + Arrays.hashCode(data) + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend new file mode 100644 index 00000000..7082c946 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend @@ -0,0 +1,21 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import edu.mit.csail.sdg.alloy4compiler.ast.Sig +import java.util.Map +import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import java.util.List + +interface AlloyModelInterpretation_TypeInterpretation { + def void resolveUnknownAtoms( + Iterable objectAtoms, + A4Solution solution, + Logic2AlloyLanguageMapperTrace forwardTrace, + Map name2AlloySig, + Map name2AlloyField, + Map expression2DefinedElement, + Map> interpretationOfUndefinedType) +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend new file mode 100644 index 00000000..d486649c --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend @@ -0,0 +1,72 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar +import edu.mit.csail.sdg.alloy4compiler.ast.Sig +import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import java.util.ArrayList +import java.util.List +import java.util.Map + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{ + protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE + + override resolveUnknownAtoms( + Iterable objectAtoms, + A4Solution solution, + Logic2AlloyLanguageMapperTrace forwardTrace, + Map name2AlloySig, + Map name2AlloyField, + Map expression2DefinedElement, + Map> interpretationOfUndefinedType) + { + /*val Map expression2DefinedElement = new HashMap() + val Map> interpretationOfUndefinedType = new HashMap;*/ + + val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes + + // 1. Evaluate the defined elements + for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { + val name = definedElementMappingEntry.value.name + val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) + val elementsOfSingletonSignature = solution.eval(matchingSig) + if(elementsOfSingletonSignature.size != 1) { + throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') + } else { + val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar + expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) + } + } + + // 2. evaluate the signatures and create new elements if necessary + for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { + val type = type2SingatureEntry.key + if(type instanceof TypeDeclaration) { + val name = type2SingatureEntry.value.name + val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) + val elementsOfSignature = solution.eval(matchingSig) + val elementList = new ArrayList(elementsOfSignature.size) + var newVariableIndex = 1; + for(elementOfSignature : elementsOfSignature) { + val expressionOfDefinedElement = elementOfSignature.atom(0) + if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { + elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) + } else { + val newElementName = '''newObject «newVariableIndex.toString»''' + val newRepresentation = createDefinedElement => [ + it.name = newElementName + ] + elementList += newRepresentation + expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) + } + } + interpretationOfUndefinedType.put(type,elementList) + } + } + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..249820b6 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend @@ -0,0 +1,20 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import java.util.Map +import edu.mit.csail.sdg.alloy4compiler.ast.Sig +import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory + +class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ + protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE + + override resolveUnknownAtoms(Iterable objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map name2AlloySig, Map name2AlloyField, Map expression2DefinedElement, Map> interpretationOfUndefinedType) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend new file mode 100644 index 00000000..65eaad47 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend @@ -0,0 +1,491 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Distinct +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.InstanceOf +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.StringTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import java.util.Collection +import java.util.Collections +import java.util.HashMap +import java.util.List +import java.util.Map +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import org.eclipse.viatra.query.runtime.emf.EMFScope +import org.eclipse.xtend.lib.annotations.Accessors + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2AlloyLanguageMapper { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + private val RunCommandMapper runCommandMapper + @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; + @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_ConstantMapper constantMapper = new Logic2AlloyLanguageMapper_ConstantMapper(this) + @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_FunctionMapper functionMapper = new Logic2AlloyLanguageMapper_FunctionMapper(this) + @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_RelationMapper relationMapper = new Logic2AlloyLanguageMapper_RelationMapper(this) + @Accessors(PUBLIC_GETTER) private val Logic2AlloyLanguageMapper_Containment containmentMapper = new Logic2AlloyLanguageMapper_Containment(this) + + public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { + this.typeMapper = typeMapper + this.runCommandMapper = new RunCommandMapper(typeMapper) + } + + public def TracedOutput transformProblem(LogicProblem problem, AlloySolverConfiguration config) { + val logicLanguage = createALSSignatureBody => [ + it.multiplicity = ALSMultiplicity.ONE + it.declarations += + createALSSignatureDeclaration => [ + it.name = support.toID(#["util", "language"]) ] + ] + + val specification = createALSDocument=>[ + it.signatureBodies+=logicLanguage + ] + val trace = new Logic2AlloyLanguageMapperTrace => [ + it.specification = specification + it.logicLanguage = logicLanguage.declarations.head + it.logicLanguageBody = logicLanguage + + it.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) + ] + specification.transformRandomisation(config.randomise) + + typeMapper.transformTypes(problem.types,problem.elements,this,trace) + + trace.constantDefinitions = problem.collectConstantDefinitions + trace.functionDefinitions = problem.collectFunctionDefinitions + trace.relationDefinitions = problem.collectRelationDefinitions + val calledInTransitiveClosure = problem.collectTransitiveRelationCalls + + problem.constants.forEach[this.constantMapper.transformConstant(it, trace)] + problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] + problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] + calledInTransitiveClosure.forEach[this.relationMapper.prepareTransitiveClosure(it, trace)] + + problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstantDefinitionSpecification(it,trace)] + problem.functions.filter(FunctionDefinition).forEach[this.functionMapper.transformFunctionDefinitionSpecification(it,trace)] + problem.relations.filter(RelationDefinition).forEach[this.relationMapper.transformRelationDefinitionSpecification(it,trace)] + + val containment = problem.getContainmentHierarchies.head + if(containment !== null) { + this.containmentMapper.transformContainmentHierarchy(containment,trace) + } + + //////////////////// + // Collect EMF-specific assertions + //////////////////// + val assertion2InverseRelation = problem.annotations.collectAnnotations(InverseRelationAssertion) + val assertion2UpperMultiplicityAssertion = problem.annotations.collectAnnotations(UpperMultiplicityAssertion) + val assertion2LowerMultiplicityAssertion = problem.annotations.collectAnnotations(LowerMultiplicityAssertion) + + //////////////////// + // Transform Assertions + //////////////////// + for(assertion : problem.assertions) { + if(assertion2InverseRelation.containsKey(assertion)) { + transformInverseAssertion(assertion.lookup(assertion2InverseRelation),trace) + } else if(assertion2UpperMultiplicityAssertion.containsKey(assertion)) { + transformUpperMultiplicityAssertion(assertion.lookup(assertion2UpperMultiplicityAssertion),trace) + } else if(assertion2LowerMultiplicityAssertion.containsKey(assertion)) { + transformLowerMultiplicityAssertion(assertion.lookup(assertion2LowerMultiplicityAssertion),trace) + } else { + transformAssertion(assertion,trace) + } + } + + runCommandMapper.transformRunCommand(this, specification, trace, config) + + return new TracedOutput(specification,trace) + } + + def transformRandomisation(ALSDocument document, int randomisation) { + if(randomisation !== 0) { + document.signatureBodies += createALSSignatureBody => [ + val declaration = createALSSignatureDeclaration => [ + it.name = support.toID(#["language","util","randomseed"]) + ] + it.declarations += declaration + it.multiplicity = ALSMultiplicity::ONE + for(i : 1..randomisation) { + it.fields+=createALSFieldDeclaration => [ + it.name = support.toID(#["language","util","randomseedField",i.toString]) + it.multiplicity = ALSMultiplicity::ONE + it.type = createALSReference => [referred = declaration] + ] + } + ] + } + } + + def transformInverseAssertion(InverseRelationAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { + val a = assertion.inverseA + val b = assertion.inverseB + if(a instanceof RelationDeclaration && b instanceof RelationDeclaration && + !trace.relationDefinitions.containsKey(a) && !trace.relationDefinitions.containsKey(b)) + { + val fact = createALSFactDeclaration => [ + it.name = support.toID(assertion.target.name) + it.term = createALSEquals => [ + it.leftOperand = relationMapper.transformRelationReference(a as RelationDeclaration, trace) + it.rightOperand = createALSInverseRelation => [it.operand = relationMapper.transformRelationReference(b as RelationDeclaration, trace) ] + ] + ] + trace.specification.factDeclarations += fact + } else { + return transformAssertion(assertion.target,trace) + } + } + + def transformUpperMultiplicityAssertion(UpperMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { + val x = assertion.relation + if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { + val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) + val type = relation.type + + if(type instanceof ALSDirectProduct) { + type.rightMultiplicit = type.rightMultiplicit.addUpper + } else { + relation.multiplicity = relation.multiplicity.addUpper + } + + if(assertion.upper === 1) { + return true + } else { + return transformAssertion(assertion.target,trace) + } + + } else { + return transformAssertion(assertion.target,trace) + } + } + + def transformLowerMultiplicityAssertion(LowerMultiplicityAssertion assertion, Logic2AlloyLanguageMapperTrace trace) { + val x = assertion.relation + if(x instanceof RelationDeclaration && !trace.relationDefinitions.containsKey(x)) { + val relation = relationMapper.getRelationReference((x as RelationDeclaration),trace) + val type = relation.type + + if(type instanceof ALSDirectProduct) { + type.rightMultiplicit = type.rightMultiplicit.addLower + } else { + relation.multiplicity = relation.multiplicity.addLower + } + + if(assertion.lower === 1) { + return true + } else { + return transformAssertion(assertion.target,trace) + } + + } else { + return transformAssertion(assertion.target,trace) + } + } + + private def addLower(ALSMultiplicity multiplicity) { + if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { + return ALSMultiplicity::SOME + } else if(multiplicity === ALSMultiplicity::LONE) { + return ALSMultiplicity::ONE + } else if(multiplicity == ALSMultiplicity::ONE) { + return ALSMultiplicity::ONE + } else { + throw new IllegalArgumentException('''Lower multiplicity is already set!''') + } + } + private def addUpper(ALSMultiplicity multiplicity) { + if(multiplicity === ALSMultiplicity::ALL) { + return ALSMultiplicity::LONE + } else if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { + return ALSMultiplicity::LONE + } else if(multiplicity === ALSMultiplicity::SOME) { + return ALSMultiplicity::ONE + } else if(multiplicity == ALSMultiplicity::ONE) { + return ALSMultiplicity::ONE + } else { + throw new IllegalArgumentException('''Upper multiplicity is already set!''') + } + } + + private def collectAnnotations(Collection collection, Class annotationKind) { + val res = new HashMap + collection.filter(annotationKind).forEach[res.put(it.target,it)] + return res + } + + private def collectConstantDefinitions(LogicProblem problem) { + val res = new HashMap + problem.constants.filter(ConstantDefinition).filter[it.defines!==null].forEach[ + res.put(it.defines,it) + ] + return res + } + private def collectFunctionDefinitions(LogicProblem problem) { + val res = new HashMap + problem.functions.filter(FunctionDefinition).filter[it.defines!==null].forEach[ + res.put(it.defines,it) + ] + return res + } + private def collectRelationDefinitions(LogicProblem problem) { + val res = new HashMap + problem.relations.filter(RelationDefinition).filter[it.defines!==null].forEach[ + res.put(it.defines,it) + ] + return res + } + private def collectTransitiveRelationCalls(LogicProblem problem) { + return problem.eAllContents.filter(TransitiveClosure).map[it.relation].toSet + } + + //////////////////// + // Type References + //////////////////// + def dispatch protected ALSTerm transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyLanguageMapperTrace trace) { + return createALSReference => [ it.referred = support.getBooleanType(trace) ] + } + def dispatch protected ALSTerm transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } + def dispatch protected ALSTerm transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSInt } + def dispatch protected ALSTerm transformTypeReference(StringTypeReference stringTypeReference, Logic2AlloyLanguageMapperTrace trace) { createALSString } + def dispatch protected ALSTerm transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapperTrace trace) { + val types = typeMapper.transformTypeReference(complexTypeReference.referred, this, trace) + return support.unfoldPlus(types.map[t|createALSReference=>[referred = t]]) + } + + ////////////// + // Assertions + Terms + ////////////// + + def protected transformAssertion(Assertion assertion, Logic2AlloyLanguageMapperTrace trace) { + val res = createALSFactDeclaration => [ + it.name = support.toID(assertion.name) + it.term = assertion.value.transformTerm(trace,Collections.EMPTY_MAP) + ] + trace.specification.factDeclarations += res + } + + def dispatch protected ALSTerm transformTerm(BoolLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map variables) { + var ALSEnumLiteral ref; + if(literal.value==true) {ref = support.getBooleanTrue(trace)} + else {ref = support.getBooleanFalse(trace)} + val refFinal = ref + + return support.booleanToLogicValue((createALSReference => [referred = refFinal]),trace) + } + def dispatch protected ALSTerm transformTerm(RealLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map variables) { + val v = literal.value.intValue + if(v>=0) { createALSNumberLiteral => [value = v]} + else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = v] ] } + } + def dispatch protected ALSTerm transformTerm(IntLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map variables) { + if(literal.value>=0) { createALSNumberLiteral => [value = literal.value]} + else {createALSUnaryMinus => [it.operand = createALSNumberLiteral => [value = literal.value] ] } + } + def dispatch protected ALSTerm transformTerm(StringLiteral literal, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSStringLiteral => [it.value = literal.value] + } + + def dispatch protected ALSTerm transformTerm(Not not, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSNot=>[operand = not.operand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(And and, Logic2AlloyLanguageMapperTrace trace, Map variables) { + support.unfoldAnd(and.operands.map[transformTerm(trace,variables)]) } + def dispatch protected ALSTerm transformTerm(Or or, Logic2AlloyLanguageMapperTrace trace, Map variables) { + support.unfoldOr(or.operands.map[transformTerm(trace,variables)],trace) } + def dispatch protected ALSTerm transformTerm(Impl impl, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSImpl => [leftOperand = impl.leftOperand.transformTerm(trace,variables) rightOperand = impl.rightOperand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(Iff iff, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSIff => [leftOperand = iff.leftOperand.transformTerm(trace,variables) rightOperand = iff.rightOperand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(MoreThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSMore => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(LessThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSLess => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(MoreOrEqualThan moreThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSMeq => [leftOperand = moreThan.leftOperand.transformTerm(trace,variables) rightOperand = moreThan.rightOperand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(LessOrEqualThan lessThan, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSLeq => [leftOperand = lessThan.leftOperand.transformTerm(trace,variables) rightOperand = lessThan.rightOperand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(Equals equals, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSEquals => [leftOperand = equals.leftOperand.transformTerm(trace,variables) rightOperand = equals.rightOperand.transformTerm(trace,variables)] } + def dispatch protected ALSTerm transformTerm(Distinct distinct, Logic2AlloyLanguageMapperTrace trace, Map variables) { + support.unfoldDistinctTerms(this,distinct.operands,trace,variables) } + + def dispatch protected ALSTerm transformTerm(Plus plus, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSFunctionCall => [it.params += plus.leftOperand.transformTerm(trace,variables) it.params += plus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.PLUS] } + def dispatch protected ALSTerm transformTerm(Minus minus, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSFunctionCall => [it.params += minus.leftOperand.transformTerm(trace,variables) it.params += minus.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.SUB] } + def dispatch protected ALSTerm transformTerm(Multiply multiply, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSFunctionCall => [it.params += multiply.leftOperand.transformTerm(trace,variables) it.params += multiply.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.MUL] } + def dispatch protected ALSTerm transformTerm(Divison div, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSFunctionCall => [it.params += div.leftOperand.transformTerm(trace,variables) it.params += div.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.DIV] } + def dispatch protected ALSTerm transformTerm(Mod mod, Logic2AlloyLanguageMapperTrace trace, Map variables) { + createALSFunctionCall => [it.params += mod.leftOperand.transformTerm(trace,variables) it.params += mod.rightOperand.transformTerm(trace,variables) it.referredNumericOperator = ALSNumericOperator.REM] } + + def dispatch protected ALSTerm transformTerm(Forall forall, Logic2AlloyLanguageMapperTrace trace, Map variables) { + support.createQuantifiedExpression(this,forall,ALSMultiplicity.ALL,trace,variables) } + def dispatch protected ALSTerm transformTerm(Exists exists, Logic2AlloyLanguageMapperTrace trace, Map variables) { + support.createQuantifiedExpression(this,exists,ALSMultiplicity.SOME,trace,variables) } + + def dispatch protected ALSTerm transformTerm(InstanceOf instanceOf, Logic2AlloyLanguageMapperTrace trace, Map variables) { + return createALSSubset => [ + it.leftOperand = instanceOf.value.transformTerm(trace,variables) + it.rightOperand = instanceOf.range.transformTypeReference(trace) + ] + } + + def dispatch protected ALSTerm transformTerm(TransitiveClosure tc, Logic2AlloyLanguageMapperTrace trace, Map variables) { + return this.relationMapper.transformTransitiveRelationReference( + tc.relation, + tc.leftOperand.transformTerm(trace,variables), + tc.rightOperand.transformTerm(trace,variables), + trace + ) + } + + def dispatch protected ALSTerm transformTerm(SymbolicValue symbolicValue, Logic2AlloyLanguageMapperTrace trace, Map variables) { + symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } + + def dispatch protected ALSTerm transformSymbolicReference(DefinedElement referred, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { + typeMapper.transformReference(referred,trace) + } + def dispatch protected ALSTerm transformSymbolicReference(ConstantDeclaration constant, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { + if(trace.constantDefinitions.containsKey(constant)) { + return this.transformSymbolicReference(constant.lookup(trace.constantDefinitions),parameterSubstitutions,trace,variables) + } else { + val res = createALSJoin=> [ + leftOperand = createALSReference => [ referred = trace.logicLanguage ] + rightOperand = createALSReference => [ referred = constant.lookup(trace.constantDeclaration2LanguageField) ] + ] + return support.postprocessResultOfSymbolicReference(constant.type,res,trace) + } + } + def dispatch protected ALSTerm transformSymbolicReference(ConstantDefinition constant, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { + val res = createALSFunctionCall => [ + it.referredDefinition = constant.lookup(trace.constantDefinition2Function) + ] + return support.postprocessResultOfSymbolicReference(constant.type,res,trace) + } + def dispatch protected ALSTerm transformSymbolicReference(Variable variable, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { + val res = createALSReference => [referred = variable.lookup(variables)] + return support.postprocessResultOfSymbolicReference(variable.range,res,trace) + } + def dispatch protected ALSTerm transformSymbolicReference(FunctionDeclaration function, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { + if(trace.functionDefinitions.containsKey(function)) { + return this.transformSymbolicReference(function.lookup(trace.functionDefinitions),parameterSubstitutions,trace,variables) + } else { + if(functionMapper.transformedToHostedField(function,trace)) { + val param = parameterSubstitutions.get(0).transformTerm(trace,variables) + val res = createALSJoin => [ + leftOperand = support.prepareParameterOfSymbolicReference(function.parameters.get(0),param,trace) + rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2HostedField)] + ] + return support.postprocessResultOfSymbolicReference(function.range,res,trace) + } else { + val functionExpression = createALSJoin=>[ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [referred = function.lookup(trace.functionDeclaration2LanguageField)] + ] + val res = support.unfoldDotJoin(this,parameterSubstitutions,functionExpression,trace,variables) + return support.postprocessResultOfSymbolicReference(function.range,res,trace) + } + } + } + def dispatch protected ALSTerm transformSymbolicReference(FunctionDefinition function, List parameterSubstitutions, Logic2AlloyLanguageMapperTrace trace, Map variables) { + val result = createALSFunctionCall => [ + it.referredDefinition = function.lookup(trace.functionDefinition2Function) + it.params += parameterSubstitutions.map[it.transformTerm(trace,variables)] + ] + return support.postprocessResultOfSymbolicReference(function.range,result,trace) + } + + def dispatch protected ALSTerm transformSymbolicReference(RelationDeclaration relation, List parameterSubstitutions, + Logic2AlloyLanguageMapperTrace trace, Map variables) { + if(trace.relationDefinitions.containsKey(relation)) { + this.transformSymbolicReference(relation.lookup(trace.relationDefinitions),parameterSubstitutions,trace,variables) + } else { + if(relationMapper.transformToHostedField(relation,trace)) { + val alsRelation = relation.lookup(trace.relationDeclaration2Field) + // R(a,b) => + // b in a.R + return createALSSubset => [ + it.leftOperand = parameterSubstitutions.get(1).transformTerm(trace,variables) + it.rightOperand = createALSJoin => [ + it.leftOperand = parameterSubstitutions.get(0).transformTerm(trace,variables) + it.rightOperand = createALSReference => [ it.referred = alsRelation ] + ] + ] + } else { + val target = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] + val source = support.unfoldTermDirectProduct(this,parameterSubstitutions,trace,variables) + + return createALSSubset => [ + leftOperand = source + rightOperand = target + ] + } + } + } + + + + def dispatch protected ALSTerm transformSymbolicReference(RelationDefinition relation, List parameterSubstitutions, + Logic2AlloyLanguageMapperTrace trace, Map variables) + { + return createALSFunctionCall => [ + it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) + it.params += parameterSubstitutions.map[p | p.transformTerm(trace,variables)] + ] + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend new file mode 100644 index 00000000..6aadb285 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend @@ -0,0 +1,56 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFieldDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFunctionDefinition +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDefinition +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import java.util.HashMap +import java.util.Map +import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation + +interface Logic2AlloyLanguageMapper_TypeMapperTrace {} + +class Logic2AlloyLanguageMapperTrace { + public var ViatraQueryEngine incqueryEngine; + + public var ALSDocument specification; + public var ALSSignatureDeclaration logicLanguage; + public var ALSSignatureBody logicLanguageBody; + public var ALSEnumDeclaration boolType; + public var ALSEnumLiteral boolTrue; + public var ALSEnumLiteral boolFalse; + + public var Logic2AlloyLanguageMapper_TypeMapperTrace typeMapperTrace + + public val Map constantDeclaration2LanguageField = new HashMap + public val Map constantDefinition2Function = new HashMap + + public val Map functionDeclaration2HostedField = new HashMap + public val Map functionDeclaration2LanguageField = new HashMap + public val Map functionDefinition2Function = new HashMap + + public val Map relationDeclaration2Global = new HashMap + public val Map relationDeclaration2Field = new HashMap + public val Map relationDefinition2Predicate = new HashMap + + public val Map transitiveClosureTarget2Global = new HashMap + public val Map transitiveClosureTarget2Field = new HashMap + + public var Map constantDefinitions + public var Map functionDefinitions + public var Map relationDefinitions + + public var Map relationInTransitiveToGlobalField = new HashMap + public var Map relationInTransitiveToHosterField = new HashMap +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend new file mode 100644 index 00000000..22650a92 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend @@ -0,0 +1,43 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2AlloyLanguageMapper_ConstantMapper { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper base; + public new(Logic2AlloyLanguageMapper base) { + this.base = base + } + + def protected dispatch transformConstant(ConstantDeclaration constant, Logic2AlloyLanguageMapperTrace trace) { + if(!trace.constantDefinitions.containsKey(constant)) { + val c = createALSFieldDeclaration=> [ + name = support.toID(constant.name) + it.type = base.transformTypeReference(constant.type,trace) + it.multiplicity = ALSMultiplicity.ONE + ] + trace.logicLanguageBody.fields+= c + trace.constantDeclaration2LanguageField.put(constant,c) + } + } + + def protected dispatch transformConstant(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) { + val c = createALSFunctionDefinition=> [ + name = support.toID(constant.name) + it.type = base.transformTypeReference(constant.type,trace) + // the value is set later + ] + trace.specification.functionDefinitions += c + trace.constantDefinition2Function.put(constant,c) + } + + def protected transformConstantDefinitionSpecification(ConstantDefinition constant, Logic2AlloyLanguageMapperTrace trace) { + val definition = constant.lookup(trace.constantDefinition2Function) + definition.value = base.transformTerm(constant.value, trace,emptyMap) + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend new file mode 100644 index 00000000..399a4eaf --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend @@ -0,0 +1,260 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy +import java.util.HashMap + +class Logic2AlloyLanguageMapper_Containment { + val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper base; + public new(Logic2AlloyLanguageMapper base) { + this.base = base + } + + def protected transformContainmentHierarchy(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { + // Single root + val rootField = createALSFieldDeclaration => [ + it.name= support.toID(#["util", "root"]) + it.multiplicity = ALSMultiplicity.ONE + it.type = typesOrderedInContainment(containment,trace) + ] + trace.logicLanguageBody.fields += rootField + + val contains = createALSFieldDeclaration => [ + it.name = support.toID(#["util", "contains"]) + //it.multiplicity = ALSMultiplicity::SET + it.type = createALSDirectProduct => [ + it.leftMultiplicit = ALSMultiplicity::LONE + it.rightMultiplicit = ALSMultiplicity::SET + it.leftOperand = typesOrderedInContainment(containment,trace) + it.rightOperand = typesOrderedInContainment(containment,trace) + ] + ] + trace.logicLanguageBody.fields += contains + + val containmentRelationDefinition = createALSFactDeclaration => [ + it.name = support.toID(#["util", "containmentDefinition"]) + ] + + if(containment.containmentRelations.forall[it instanceof RelationDeclaration]) { + val containmentRelations = containment.containmentRelations.filter(RelationDeclaration).map[relation| + base.relationMapper.transformRelationReference(relation,trace) + ].toList + + containmentRelationDefinition.term = createALSEquals => [ + leftOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ]] + rightOperand = support.unfoldPlus(containmentRelations) + ] + } else { + val parent = createALSVariableDeclaration => [ + it.name = "parent" + it.range = typesOrderedInContainment(containment, trace) + ] + val child = createALSVariableDeclaration => [ + it.name = "child" + it.range = typesOrderedInContainment(containment, trace) + ] + + val logicFactory = LogiclanguageFactory.eINSTANCE + val logicParentVariable = logicFactory.createVariable + val logicChildVariable = logicFactory.createVariable + val logicParent = logicFactory.createSymbolicValue => [it.symbolicReference = logicParentVariable] + val logicChild = logicFactory.createSymbolicValue => [it.symbolicReference = logicChildVariable] + val variableMap = new HashMap => [put(logicParentVariable,parent) put(logicChildVariable,child)] + val possibleRelations = containment.containmentRelations.map[relation | + base.transformSymbolicReference(relation,#[logicParent,logicChild],trace,variableMap) + ] + + containmentRelationDefinition.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity.ALL + it.variables += parent + it.variables += child + it.expression = createALSIff => [ + it.leftOperand = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = child] + it.rightOperand = createALSReference => [it.referred = parent] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + it.rightOperand = support.unfoldOr(possibleRelations,trace) + ] + ] + } + + trace.specification.factDeclarations += containmentRelationDefinition + + // With the exception of the root, every object has at least one parent + // No parent for root + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util", "noParentForRoot"]) + it.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::NO + val parent = createALSVariableDeclaration => [ + it.name = "parent" + it.range = typesOrderedInContainment(containment,trace) + ] + it.variables += parent + it.expression = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = parent] + it.rightOperand = createALSJoin => [ + it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] + it.rightOperand = createALSReference => [it.referred = rootField] + ] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + ] + ] + // Parent for nonroot + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util", "atLeastOneParent"]) + it.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::ALL + val child = createALSVariableDeclaration => [ + it.name = "child" + it.range = typesOrderedInContainment(containment,trace) + ] + it.variables += child + it.expression = createALSOr => [ + it.leftOperand = createALSEquals => [ + it.leftOperand = createALSReference => [it.referred = child] + it.rightOperand = createALSJoin => [ + it.leftOperand = createALSReference => [it.referred = trace.logicLanguage] + it.rightOperand = createALSReference => [it.referred = rootField] + ] + ] + it.rightOperand = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::SOME + val parent = createALSVariableDeclaration => [ + it.name = "parent" + it.range = typesOrderedInContainment(containment, trace) + ] + it.variables += parent + it.expression = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = parent] + it.rightOperand = createALSReference => [it.referred = child] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + ] + ] + ] + ] + + // Every object has at most one parent +// trace.specification.factDeclarations += createALSFactDeclaration => [ +// it.name = support.toID(#["util", "atMostOneParent"]) +// it.term = createALSQuantifiedEx => [ +// it.type = ALSMultiplicity::ALL +// val child = createALSVariableDeclaration => [ +// it.name = "child" +// it.range = typesOrderedInContainment(containment,trace) +// ] +// it.variables += child +// it.expression = createALSQuantifiedEx => [ +// it.type = ALSMultiplicity::LONE +// val parent = createALSVariableDeclaration => [ +// it.name = "parent" +// it.range = typesOrderedInContainment(containment, trace) +// ] +// it.variables += parent +// it.expression = createALSFunctionCall => [ +// it.referredDefinition = containmentRelation +// it.params += createALSReference => [ +// it.referred = parent +// it.referred = child +// ] +// ] +// ] +// ] +// ] + + // No circle in containment + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util", "noCircularContainment"]) + it.term = createALSQuantifiedEx => [ + it.type = ALSMultiplicity::NO + val variable = createALSVariableDeclaration => [ + it.name = "circle" + it.range = typesOrderedInContainment(containment,trace) + ] + it.variables += variable + it.expression = createALSSubset => [ + it.leftOperand = createALSDirectProduct => [ + it.leftOperand = createALSReference => [it.referred = variable] + it.rightOperand = createALSReference => [it.referred = variable] + ] + it.rightOperand = createAlSTransitiveClosure => [ + it.operand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = contains ] + ] + ] + ] + ] + ] + + } + + /*def protected calculateContainmentTypeCoveringSignatures(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { + val types = containment.typesOrderedInHierarchy + val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten.toList +// val uncoveredSignatures = new ArrayList(signaturesInContainment) +// val coveringSignatures = new LinkedList +// + val engine = ViatraQueryEngine.on(new EMFScope(trace.specification)) + //val directSubsetMatcher = DirectSubsetMatcher.on(engine) + // x <= y + val subsetMatcher = SubsetMatcher.on(engine) + + if() + }*/ + + /*def boolean coveringAllSignaturesInContainment(ALSSignatureDeclaration target, List signaturesInContainment, SubsetMatcher matcher) { + for(signatureInContainment : signaturesInContainment) { + if(!matcher.hasMatch(signatureInContainment,target)) { + return false + } + } + return true + }*/ + + /*def boolean coveringSignatureNotInContainment(ALSSignatureDeclaration target, List signaturesInContainment, SubsetMatcher matcher) { + val subtypes = matcher.getAllValuesOfx(target); + for(subType : subtypes) { + val isSubtypeOfASignatureInContainment = signaturesInContainment.exists[contained | + matcher.hasMatch(subType,contained) + ] + if(!isSubtypeOfASignatureInContainment) { + return false + } + } + return true + }*/ + + def protected typesOrderedInContainment(ContainmentHierarchy containment, Logic2AlloyLanguageMapperTrace trace) { + val types = containment.typesOrderedInHierarchy + val signaturesInContainment = types.map[base.typeMapper.transformTypeReference(it, base, trace)].flatten + // val allSignatures = trace.specification.signatureBodies.map[declarations].flatten + val typeReferences = signaturesInContainment.map[sig | createALSReference => [it.referred = sig]].toList + return support.unfoldPlus(typeReferences) + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend new file mode 100644 index 00000000..0915c306 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend @@ -0,0 +1,87 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import java.util.HashMap + +class Logic2AlloyLanguageMapper_FunctionMapper { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper base; + public new(Logic2AlloyLanguageMapper base) { + this.base = base + } + + def protected dispatch transformFunction(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) { + if(!trace.constantDefinitions.containsKey(f)) { + if(transformedToHostedField(f,trace)) transformFunctionToFieldOfSignature(f,trace) + else transformFunctionToGlobalRelation(f,trace) + } + } + + def protected transformedToHostedField(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) { + if(f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference) { + val head = f.parameters.head + if(head instanceof ComplexTypeReference) { + val types = base.typeMapper.transformTypeReference(head.referred,base,trace) + return types.size == 1 + } + } + return (f.parameters.size == 1 && f.parameters.head instanceof ComplexTypeReference) + } + def protected transformFunctionToFieldOfSignature(FunctionDeclaration f,Logic2AlloyLanguageMapperTrace trace) { + val param = (f.parameters.head as ComplexTypeReference) + val referred = param.referred + val field = createALSFieldDeclaration => [ + it.name = support.toID(f.getName) + it.multiplicity = ALSMultiplicity.ONE + it.type = base.transformTypeReference(f.range,trace) + ] + val host = base.typeMapper.transformTypeReference(referred,base,trace).get(0) + (host.eContainer as ALSSignatureBody).fields += field + trace.functionDeclaration2HostedField.put(f, field) + } + def protected transformFunctionToGlobalRelation(FunctionDeclaration f, Logic2AlloyLanguageMapperTrace trace) { + val field = createALSFieldDeclaration => [ + it.name = support.toID(f.name) + it.multiplicity = ALSMultiplicity.SET + it.type = createALSDirectProduct => [ + it.leftOperand = support.unfoldReferenceDirectProduct(base,f.parameters,trace) + it.rightMultiplicit = ALSMultiplicity.ONE + it.rightOperand = base.transformTypeReference(f.range,trace) + ] + ] + trace.logicLanguageBody.fields += field + trace.functionDeclaration2LanguageField.put(f, field) + } + + def protected dispatch transformFunction(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) { + val res = createALSFunctionDefinition => [ + name = support.toID(f.name) + // variables + specification later + ] + trace.specification.functionDefinitions+=res; + trace.functionDefinition2Function.put(f,res) + } + + def protected transformFunctionDefinitionSpecification(FunctionDefinition f, Logic2AlloyLanguageMapperTrace trace) { + val target = f.lookup(trace.functionDefinition2Function) + val variableMap = new HashMap + for(variable : f.variable) { + val v = createALSVariableDeclaration => [ + it.name = support.toID(variable.name) + it.range = base.transformTypeReference(variable.range,trace) + // specification later + ] + target.variables+=v + variableMap.put(variable,v) + } + target.value = base.transformTerm(f.value,trace,variableMap) + } + +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend new file mode 100644 index 00000000..d300a28b --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend @@ -0,0 +1,199 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition +import java.util.HashMap + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm + +class Logic2AlloyLanguageMapper_RelationMapper { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + val Logic2AlloyLanguageMapper base; + public new(Logic2AlloyLanguageMapper base) { + this.base = base + } + + def dispatch public void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { + if(!trace.relationDefinitions.containsKey(r)) { + if(r.transformToHostedField(trace)) { + transformRelationDeclarationToHostedField(r,trace) + } else { + transformRelationDeclarationToGlobalField(r,trace) + } + } + } + + def public createRelationDeclaration(String name, List paramTypes, Logic2AlloyLanguageMapperTrace trace) { + val field = createALSFieldDeclaration => [ + it.name = support.toID(name) + it.type = support.unfoldReferenceDirectProduct(base,paramTypes,trace) + ] + trace.logicLanguageBody.fields += field + return field + } + + def protected transformToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { + val first = r.parameters.get(0) + if(r.parameters.size == 2) { + if(first instanceof ComplexTypeReference) { + val types = base.typeMapper.transformTypeReference(first.referred,base,trace) + if(types.size == 1) { + return true + } + } + } + return false + } + + def protected transformRelationDeclarationToHostedField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { + val hostType = (r.parameters.head as ComplexTypeReference).referred + + val targetBody = base.typeMapper.transformTypeReference(hostType,base,trace).get(0).eContainer as ALSSignatureBody + val field = createALSFieldDeclaration => [ + it.name = support.toID(r.getName) + it.multiplicity = ALSMultiplicity.SET + it.type = base.transformTypeReference(r.parameters.get(1),trace) + ] + targetBody.fields += field + trace.relationDeclaration2Field.put(r,field) + + } + + def protected transformRelationDeclarationToGlobalField(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { + val field = createALSFieldDeclaration => [ + it.name = support.toID(r.name) + it.type = support.unfoldReferenceDirectProduct(base,r.parameters,trace) + ] + trace.logicLanguageBody.fields += field + trace.relationDeclaration2Global.put(r, field) + } + + def dispatch public void transformRelation(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { + val res = createALSRelationDefinition => [ + name = support.toID(r.name) + // fill the variables later + // fill the expression later + ] + + trace.relationDefinition2Predicate.put(r,res) + trace.specification.relationDefinitions+=res; + } + + def protected void transformRelationDefinitionSpecification(RelationDefinition r, Logic2AlloyLanguageMapperTrace trace) { + val predicate = r.lookup(trace.relationDefinition2Predicate) + if(predicate !== null) { + val variableMap = new HashMap + for(variable : r.variables) { + val v = createALSVariableDeclaration => [ + it.name = support.toID(variable.name) + it.range = base.transformTypeReference(variable.range,trace) + ] + predicate.variables+=v + variableMap.put(variable,v) + } + predicate.value = base.transformTerm(r.value,trace,variableMap) + } + } + + def public transformRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { + if(relation.transformToHostedField(trace)) { + return createALSReference => [it.referred = relation.lookup(trace.relationDeclaration2Field) ] + } else { + return createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = relation.lookup(trace.relationDeclaration2Global) ]] + } + } + + def public getRelationReference(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { + if(relation.transformToHostedField(trace)) { + return relation.lookup(trace.relationDeclaration2Field) + } else { + return relation.lookup(trace.relationDeclaration2Global) + } + } + + public def dispatch void prepareTransitiveClosure(RelationDeclaration relation, Logic2AlloyLanguageMapperTrace trace) { + // There is nothing to do, relation can be used in ^relation expressions + if(transformToHostedField(relation,trace)) { + trace.relationInTransitiveToHosterField.put(relation,relation.lookup(trace.relationDeclaration2Field)) + } else { + trace.relationInTransitiveToGlobalField.put(relation,relation.lookup(trace.relationDeclaration2Global)) + } + } + public def dispatch void prepareTransitiveClosure(RelationDefinition relation, Logic2AlloyLanguageMapperTrace trace) { + if(relation.parameters.size === 2) { + /** 1. Create a relation that can be used in ^relation expressions */ + val declaration = this.createRelationDeclaration('''AsDeclaration «relation.name»''',relation.parameters,trace) + trace.relationInTransitiveToHosterField.put(relation,declaration) + /** 2. Add fact that the declaration corresponds to the definition */ + val fact = createALSFactDeclaration => [ + it.name = '''EqualsAsDeclaration «relation.name»''' + it.term = createALSQuantifiedEx => [ + val a = createALSVariableDeclaration => [ + it.name = "a" + it.range = base.transformTypeReference(relation.parameters.get(0),trace) + ] + val b = createALSVariableDeclaration => [ + it.name = "b" + it.range = base.transformTypeReference(relation.parameters.get(1),trace) + ] + it.variables += a + it.variables += b + it.type = ALSMultiplicity::ALL + it.expression = createALSIff => [ + it.leftOperand = createALSFunctionCall => [ + it.referredDefinition = relation.lookup(trace.relationDefinition2Predicate) + it.params += createALSReference => [ it.referred = a ] + it.params += createALSReference => [ it.referred = b ] + ] + it.rightOperand = createALSSubset => [ + it.leftOperand = createALSJoin => [ + it.leftOperand = createALSReference => [ referred = a ] + it.rightOperand = createALSReference => [ referred = b ] + ] + it.rightOperand = createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred = declaration ] + ] + ] + ] + ] + ] + trace.specification.factDeclarations += fact + return + } else { + throw new AssertionError('''A non-binary relation "«relation.name»" is used in transitive clousure!''') + } + } + + def public transformTransitiveRelationReference(Relation relation, ALSTerm source, ALSTerm target, Logic2AlloyLanguageMapperTrace trace) { + val alsTargetRelation = if(trace.relationInTransitiveToGlobalField.containsKey(relation)) { + createALSJoin => [ + leftOperand = createALSReference => [referred = trace.logicLanguage] + rightOperand = createALSReference => [ referred =relation.lookup(trace.relationInTransitiveToGlobalField) ] + ] + } else if(trace.relationInTransitiveToHosterField.containsKey(relation)){ + createALSReference => [it.referred = relation.lookup(trace.relationInTransitiveToHosterField) ] + } else { + throw new AssertionError('''Relation «relation.name» is not prepared to transitive closure!''') + } + return createALSSubset => [ + it.leftOperand = createALSJoin => [ + it.leftOperand = source + it.rightOperand = target + ] + it.rightOperand = createAlSTransitiveClosure => [it.operand = alsTargetRelation] + + ] + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend new file mode 100644 index 00000000..0b8d2857 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend @@ -0,0 +1,207 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEquals +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.QuantifiedExpression +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import java.util.ArrayList +import java.util.HashMap +import java.util.List +import java.util.Map +import org.eclipse.emf.ecore.util.EcoreUtil + +class Logic2AlloyLanguageMapper_Support { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + + /// ID handling + def protected String toIDMultiple(String... ids) { + ids.map[it.split("\\s+").join("'")].join("'") + } + + def protected String toID(String ids) { + ids.split("\\s+").join("'") + } + def protected String toID(List ids) { + ids.map[it.split("\\s+").join("'")].join("'") + } + + /// Support functions + + def protected getBooleanType(Logic2AlloyLanguageMapperTrace trace) { + if(trace.boolType!=null) { + return trace.boolType + } else { + trace.boolType = createALSEnumDeclaration => [ + it.name = toID(#["util","boolean"]) + trace.boolTrue = createALSEnumLiteral =>[it.name=toID(#["util","boolean","true"])] + it.literal += trace.boolTrue + trace.boolFalse = createALSEnumLiteral =>[it.name=toID(#["util","boolean","false"])] + it.literal += trace.boolFalse + ] + trace.specification.enumDeclarations+=trace.boolType + return trace.boolType + } + } + def protected getBooleanTrue(Logic2AlloyLanguageMapperTrace trace) { + getBooleanType(trace) + return trace.boolTrue + } + def protected getBooleanFalse(Logic2AlloyLanguageMapperTrace trace) { + getBooleanType(trace) + return trace.boolFalse + } + + def protected booleanToLogicValue(ALSTerm boolReference, Logic2AlloyLanguageMapperTrace trace) { + //println((boolReference as ALSReference).referred) + createALSEquals => [ + leftOperand = EcoreUtil.copy(boolReference) + rightOperand = createALSReference => [referred = getBooleanTrue(trace)] + ] + } + def protected booleanToEnumValue(ALSTerm value, Logic2AlloyLanguageMapperTrace trace) { + if(value instanceof ALSEquals) { + val rightOperand = value.rightOperand + if(rightOperand instanceof ALSReference) { + if(rightOperand.referred == getBooleanTrue(trace)) { + return value.leftOperand + } + } + } + return value; + } + def protected prepareParameterOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) { + if(type instanceof BoolTypeReference) { + return booleanToEnumValue(term,trace) + } + else return term + } + def protected postprocessResultOfSymbolicReference(TypeReference type, ALSTerm term, Logic2AlloyLanguageMapperTrace trace) { + if(type instanceof BoolTypeReference) { + return booleanToLogicValue(term,trace) + } + else return term + } + + def protected ALSTerm unfoldAnd(List operands) { + if(operands.size == 1) { return operands.head } + else if(operands.size > 1) { return createALSAnd=>[ + leftOperand=operands.head + rightOperand=operands.subList(1,operands.size).unfoldAnd + ]} + else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + def protected ALSTerm unfoldOr(List operands, Logic2AlloyLanguageMapperTrace trace) { + if(operands.size == 0) { return unfoldTrueStatement(trace)} + else if(operands.size == 1) { return operands.head } + else if(operands.size > 1) { return createALSOr=>[ + leftOperand=operands.head + rightOperand=unfoldOr(operands.subList(1,operands.size),trace) + ]} + //else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + protected def unfoldTrueStatement(Logic2AlloyLanguageMapperTrace trace) { + createALSEquals => [ + it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)] + it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)] + ] + } + + protected def unfoldTFalseStatement(Logic2AlloyLanguageMapper m, Logic2AlloyLanguageMapperTrace trace) { + createALSEquals => [ + it.leftOperand = createALSReference => [it.referred = getBooleanTrue(trace)] + it.rightOperand = createALSReference => [it.referred = getBooleanTrue(trace)] + ] + } + + def protected ALSTerm unfoldPlus(List operands) { + if(operands.size == 1) { return operands.head } + else if(operands.size > 1) { return createALSPlus=>[ + leftOperand=operands.head + rightOperand=operands.subList(1,operands.size).unfoldPlus + ]} + else return createALSNone + } + + def protected ALSTerm unfoldIntersection(List operands) { + if(operands.size == 1) { return operands.head } + else if(operands.size > 1) { return createALSIntersection=>[ + leftOperand=operands.head + rightOperand=operands.subList(1,operands.size).unfoldIntersection + ]} + else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + def protected ALSTerm unfoldDistinctTerms(Logic2AlloyLanguageMapper m, List operands, Logic2AlloyLanguageMapperTrace trace, Map variables) { + if(operands.size == 1) { return m.transformTerm(operands.head,trace,variables) } + else if(operands.size > 1) { + val notEquals = new ArrayList(operands.size*operands.size/2) + for(i:0..[ + leftOperand = m.transformTerm(operands.get(i),trace,variables) + rightOperand = m.transformTerm(operands.get(j),trace,variables) + ] + } + } + return notEquals.unfoldAnd + } + else throw new UnsupportedOperationException('''Logic operator with 0 operands!''') + } + + def protected ALSTerm unfoldReferenceDirectProduct(Logic2AlloyLanguageMapper m, List references,Logic2AlloyLanguageMapperTrace trace) { + if(references.size == 1) return m.transformTypeReference(references.head,trace) + else if(references.size > 1) return createALSDirectProduct => [ + it.leftOperand = m.transformTypeReference(references.head,trace) + it.rightOperand = unfoldReferenceDirectProduct(m,references.subList(1,references.size),trace) + ] + else throw new UnsupportedOperationException + } + + def protected ALSTerm unfoldDotJoin(Logic2AlloyLanguageMapper m, List elements, ALSTerm target, Logic2AlloyLanguageMapperTrace trace, + Map variables) { + if (elements.size == 1) { + return createALSJoin => [ + it.leftOperand = m.transformTerm(elements.head,trace, variables) + it.rightOperand = target + ] + } else if (elements.size > 1) { + return createALSJoin => [ + it.leftOperand = m.transformTerm(elements.last,trace, variables) + it.rightOperand = m.unfoldDotJoin(elements.subList(0, elements.size - 1), target, trace, variables) + ] + } else + throw new UnsupportedOperationException + } + + def protected ALSTerm unfoldTermDirectProduct(Logic2AlloyLanguageMapper m, List references,Logic2AlloyLanguageMapperTrace trace,Map variables) { + if(references.size == 1) return m.transformTerm(references.head,trace,variables) + else if(references.size > 1) return createALSDirectProduct => [ + it.leftOperand = m.transformTerm(references.head,trace,variables) + it.rightOperand = unfoldTermDirectProduct(m,references.subList(1,references.size),trace, variables) + ] + else throw new UnsupportedOperationException + } + + def protected createQuantifiedExpression(Logic2AlloyLanguageMapper m, QuantifiedExpression q, ALSMultiplicity multiplicity, Logic2AlloyLanguageMapperTrace trace, Map variables) { + val variableMap = q.quantifiedVariables.toInvertedMap[v | createALSVariableDeclaration=> [ + it.name = toID(v.name) + it.range = m.transformTypeReference(v.range,trace) ]] + + createALSQuantifiedEx=>[ + it.type = multiplicity + it.variables += variableMap.values + it.expression = m.transformTerm(q.expression,trace,variables.withAddition(variableMap)) + ] + } + + def protected withAddition(Map v1, Map v2) { new HashMap(v1) => [putAll(v2)] } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend new file mode 100644 index 00000000..c998de1f --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend @@ -0,0 +1,18 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.Collection +import java.util.List + +interface Logic2AlloyLanguageMapper_TypeMapper { + def void transformTypes(Collection types, Collection elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace); + def List transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) + def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) + def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace) + def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace) + + def AlloyModelInterpretation_TypeInterpretation getTypeInterpreter() +} diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend new file mode 100644 index 00000000..17b1a87b --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend @@ -0,0 +1,15 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.HashMap +import java.util.Map + +class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes + implements Logic2AlloyLanguageMapper_TypeMapperTrace +{ + public var ALSSignatureDeclaration objectSupperClass; + public val Map type2ALSType = new HashMap; + public val Map definedElement2Declaration = new HashMap +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..1b04a877 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend @@ -0,0 +1,15 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import java.util.HashMap +import java.util.List +import java.util.Map + +class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { + public var ALSSignatureDeclaration objectSupperClass; + public val Map type2ALSType = new HashMap; + public val Map definedElement2Declaration = new HashMap + public val Map> typeSelection = new HashMap +} diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..9e548ab6 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend @@ -0,0 +1,263 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.TypeQueries +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import java.util.ArrayList +import java.util.Collection +import java.util.HashMap +import java.util.List + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +/** + * Each object is an element of an Object set, and types are subsets of the objects. + */ +class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyLanguageMapper_TypeMapper{ + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + + new() { + // Initialize package + LogicproblemPackage.eINSTANCE.class + } + + override transformTypes(Collection types, Collection elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes + trace.typeMapperTrace = typeTrace + + // 1. A global type for Objects is created + val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] + val objectBody = createALSSignatureBody => [ + it.declarations += objectSig + it.abstract = true + ] + typeTrace.objectSupperClass = objectSig + trace.specification.signatureBodies += objectBody + + // 2. Each type is mapped to a unique sig + for(type : types) { + val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] + val body = createALSSignatureBody => [it.declarations += sig] + trace.specification.signatureBodies += body + typeTrace.type2ALSType.put(type,sig) + } + + // 3. The elements of a defined type is mapped to singleton signatures + // 3.1 Collect the elements + val elementMatcher = TypeQueries.instance.getLowestCommonSupertypeOfAllOccuranceOfElement(trace.incqueryEngine) + val topmostType2Elements = new HashMap> + for(element : elements) { + val topmostTypes = elementMatcher.getAllValuesOftype(element) + var ALSSignatureDeclaration selectedTopmostType; + if(topmostTypes.empty) { + selectedTopmostType = objectSig + } else{ + selectedTopmostType = topmostTypes.head.lookup(typeTrace.type2ALSType) + } + topmostType2Elements.putOrAddToList(selectedTopmostType,element) + } + + // 4. For each topmost types several singleton classes are generated, which represents the elements. + // For the sake of clarity, common bodies are used. + for(topmostEntry : topmostType2Elements.entrySet) { + + for(element : topmostEntry.value) { + val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] + typeTrace.definedElement2Declaration.put(element,signature) + } + + val body = createALSSignatureBody => [ + it.multiplicity = ALSMultiplicity.ONE + it.declarations += topmostEntry.value.map[it.lookup(typeTrace.definedElement2Declaration)] + ] + + val containerLogicType = topmostEntry.key + body.superset += containerLogicType + + trace.specification.signatureBodies+=body + } + + // 5.1 Each Defined Type is specified as the union of its elements + for(definedType : types.filter(TypeDefinition)) { + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toIDMultiple("typedefinition",definedType.name) + it.term = createALSEquals => [ + it.leftOperand = createALSReference => [ it.referred = definedType.lookup(typeTrace.type2ALSType) ] + it.rightOperand = support.unfoldPlus(definedType.elements.map[e| + createALSReference => [it.referred = e.lookup(typeTrace.definedElement2Declaration)]]) + ] + ] + } + // 5.2 Each Defined Element is unique + for(definedType : types.filter(TypeDefinition)) { + val allElementsIncludingSubtypes = + definedType.transitiveClosureStar[it.subtypes].filter(TypeDefinition) + .map[elements].flatten.toSet.toList + if(allElementsIncludingSubtypes.size>=2) { + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toIDMultiple("typeElementsUnique",definedType.name) + it.term = unfoldDistinctElements(allElementsIncludingSubtypes,trace) + ] + } + } + + // 6. Each inheritance is modeled by subset operator 'in' + for(type : types) { + val sigBody = type.lookup(typeTrace.type2ALSType).eContainer as ALSSignatureBody + if(type.supertypes.empty) { + sigBody.superset += typeTrace.objectSupperClass + } else { + sigBody.superset += type.supertypes.map[lookup(typeTrace.type2ALSType)] + } + } + + + // 7. Each type is in the intersection of the supertypes + for(type : types.filter[it.supertypes.size>=2]) { + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toIDMultiple("abstract",type.name) + it.term = createALSEquals => [ + it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] + it.rightOperand = support.unfoldIntersection(type.supertypes.map[e| + createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) + ] + ] + } + + // 8. Each abstract type is equal to the union of the subtypes + for(type : types.filter[isIsAbstract]) { + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toIDMultiple("abstract",type.name) + it.term = createALSEquals => [ + it.leftOperand = createALSReference => [ it.referred = type.lookup(typeTrace.type2ALSType) ] + it.rightOperand = support.unfoldPlus(type.subtypes.map[e| + createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) + ] + ] + } + // 8.1 The object type is the union of the root types. + val rootTypes = types.filter[it.supertypes.empty].toList + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toIDMultiple(#["ObjectTypeDefinition"]) + it.term = createALSEquals => [ + it.leftOperand = createALSReference => [ it.referred = typeTrace.objectSupperClass ] + it.rightOperand = support.unfoldPlus(rootTypes.map[e| + createALSReference => [it.referred = e.lookup(typeTrace.type2ALSType)]]) + ] + ] + + // 9. For each type X (including Object) + // only the common subtypes are in the intersection + // of the two subtype. + // 9.1. for the object + { + val rootTypeList = types.filter[it.supertypes.empty].toList + for(type1Index: 0..=2) { + for(type1Index: 0.. [ + it.name = support.toIDMultiple("common","types",t1.name,t2.name) + it.term = createALSEquals => [ + it.leftOperand = createALSIntersection => [ + it.leftOperand = createALSReference => [it.referred = t1.lookup(trace.typeTrace.type2ALSType)] + it.rightOperand = createALSReference => [it.referred = t2.lookup(trace.typeTrace.type2ALSType)] + ] + it.rightOperand = support.unfoldPlus(allTopmostCommon.map[t|createALSReference => [it.referred = t.lookup(trace.typeTrace.type2ALSType)]]) + ] + ] + } + + def private unfoldDistinctElements( + List operands, + Logic2AlloyLanguageMapperTrace trace + ) { + if(operands.size == 1 || operands.size == 0) {support.unfoldTrueStatement(trace);} + else { + val notEquals = new ArrayList(operands.size*operands.size/2) + for(i:0..[ + leftOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(i)) ] + rightOperand = createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(operands.get(j)) ] + ] + } + } + return support.unfoldAnd(notEquals) + } + } + + override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + return #[trace.typeTrace.type2ALSType.get(referred)] + } + + override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { + trace.typeTrace.objectSupperClass + } + + override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { + createALSReference => [it.referred = referred.lookup(trace.typeTrace.definedElement2Declaration)] + } + + override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { + if(undefinedScope == Integer.MAX_VALUE) return undefinedScope else return undefinedScope + trace.typeTrace.definedElement2Declaration.size + } + + override getTypeInterpreter() { + return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..7d90b2b0 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend @@ -0,0 +1,122 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage +import java.util.Collection +import java.util.LinkedList + +class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + + new() { + LogicproblemPackage.eINSTANCE.class + } + + override transformTypes(Collection types, Collection elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal + trace.typeMapperTrace = typeTrace + + // 1. A global type for Objects is created + val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])] + val objectBody = createALSSignatureBody => [ + it.declarations += objectSig + it.abstract = true + ] + typeTrace.objectSupperClass = objectSig + trace.specification.signatureBodies += objectBody + + // 2. Each type is mapped to a unique sig + for(type : types) { + val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)] + val body = createALSSignatureBody => [it.declarations += sig] + body.abstract = type.isIsAbstract || (type instanceof TypeDefinition) + + trace.specification.signatureBodies += body + typeTrace.type2ALSType.put(type,sig) + + typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)]) + } + + for(element : elements) { + val mostSpecificTypes = element.definedInType.filter[it.subtypes.empty] + if(mostSpecificTypes.size== 1) { + val mostSpecificSubtype = mostSpecificTypes.head + val elementContainer = createALSSignatureBody => [ + it.multiplicity = ALSMultiplicity::ONE + it.supertype =typeTrace.type2ALSType.get(mostSpecificSubtype) + ] + val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)] + elementContainer.declarations += signature + typeTrace.definedElement2Declaration.put(element,signature) + trace.specification.signatureBodies += elementContainer + } else { + throw new UnsupportedOperationException + } + } + + // 6. Each inheritance is modeled by extend keyword + for(type : types) { + if(type.supertypes.size == 0) { + (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = typeTrace.objectSupperClass + }if(type.supertypes.size == 1) { + val alsType = typeTrace.type2ALSType.get(type.supertypes.head) + (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsType + + } else if(type.supertypes.size > 1){ + val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head) + (typeTrace.type2ALSType.get(type).eContainer as ALSSignatureBody).supertype = alsMainType + for(otherType : type.supertypes.filter[it != alsMainType]) { + typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(type)) + } + } + } + } + + private def boolean hasDefinedSupertype(Type type) { + if(type instanceof TypeDefinition) { + return true + } else { + if(type.supertypes.empty) return false + else return type.supertypes.exists[it.hasDefinedSupertype] + } + } + + def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { + val res = trace.typeMapperTrace + if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal) { + return res + } else { + throw new IllegalArgumentException(''' + Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name», + but found «res.class.name»''') + } + } + + override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + trace.typeTrace.typeSelection.get(referred) + } + + override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { + trace.typeTrace.objectSupperClass + } + + override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { + val r = trace.typeTrace.definedElement2Declaration.get(referred) + return createALSReference => [it.referred =r] + } + + override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { + return undefinedScope + trace.typeTrace.definedElement2Declaration.size + } + + override getTypeInterpreter() { + return new AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal + } + +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend new file mode 100644 index 00000000..fdc35412 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/RunCommandMapper.xtend @@ -0,0 +1,105 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSInt +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import java.util.LinkedList +import java.util.List + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class RunCommandMapper { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + private val Logic2AlloyLanguageMapper_TypeMapper typeMapper; + + public new(Logic2AlloyLanguageMapper_TypeMapper typeMapper) { + this.typeMapper = typeMapper + } + + def public transformRunCommand(Logic2AlloyLanguageMapper mapper, ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) + { + //val knownStringNumber = specification.eAllContents.filter(ALSStringLiteral).map[it.value].toSet.size + + // add fact to ensure the existence of all literals in the scope + if(!config.typeScopes.knownStrings.empty) { + specification.factDeclarations += createALSFactDeclaration => [ + it.name = "EnsureAllStrings" + val List equals = config.typeScopes.knownStrings.map[x|createALSEquals => [ + it.leftOperand =createALSStringLiteral => [it.value = x] + it.rightOperand =createALSStringLiteral => [it.value = x] + ]].toList + it.term = support.unfoldAnd(equals) + ] + } + val typeScopes = new LinkedList + for(definedScope : config.typeScopes.maxNewElementsByType.entrySet) { + val key = definedScope.key + val amount = definedScope.value + val exactly = config.typeScopes.minNewElementsByType.containsKey(key) && config.typeScopes.minNewElementsByType.get(key) === amount + + val existing = key.transitiveClosureStar[it.subtypes].filter(TypeDefinition).map[elements].flatten.toSet + if(amount == 0 && exactly) { + specification.factDeclarations += createALSFactDeclaration => [ + it.term = createALSEquals => [ + it.leftOperand = support.unfoldPlus(typeMapper.transformTypeReference(key,mapper,trace).map[t|createALSReference => [it.referred = t]].toList) + it.rightOperand = support.unfoldPlus( existing.map[typeMapper.transformReference(it,trace)].toList ) + ] + ] + } + val int n = existing.size-amount + typeScopes += createALSSigScope => [ + it.type = typeMapper.transformTypeReference(key,mapper,trace).head + it.number = n + it.exactly =exactly + ] + } + + specification.runCommand = createALSRunCommand => [ + it.typeScopes+= createALSSigScope => [ + it.type= typeMapper.getUndefinedSupertype(trace) + it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) + it.exactly = (config.typeScopes.maxNewElements == config.typeScopes.minNewElements) + ] + if(config.typeScopes.maxNewIntegers == LogicSolverConfiguration::Unlimited) { + val integersUsed = specification.eAllContents.filter(ALSInt) + if(integersUsed.empty) { + // If no integer scope is defined, but the problem has no integers + // => scope can be empty + it.typeScopes+= createALSIntScope => [ + it.number = 0 + ] + } else { + // If no integer scope is defined, and the problem has integers + // => error + throw new UnsupportedOperationException('''An integer scope have to be specified for Alloy!''') + } + } else { + it.typeScopes += createALSIntScope => [ + if(config.typeScopes.knownIntegers.empty) { + number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxNewIntegers+1/2) + } else { + var scope = Math.max( + Math.abs(config.typeScopes.knownIntegers.max), + Math.abs(config.typeScopes.knownIntegers.min)) + if(scope*2+1 < config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) { + scope += ((config.typeScopes.knownIntegers.size + config.typeScopes.maxNewIntegers) - (scope*2))/2 + } + number = Integer.SIZE-Integer.numberOfLeadingZeros(scope)+1 + } + ] + } + if(config.typeScopes.maxNewStrings === LogicSolverConfiguration::Unlimited) { + throw new UnsupportedOperationException('''An string scope have to be specified for Alloy!''') + } else { + if(config.typeScopes.maxNewStrings != 0) { + it.typeScopes += createALSStringScope => [it.number = 0] + } + } + ] + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ new file mode 100644 index 00000000..264e3ff8 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ @@ -0,0 +1,212 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar +import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field +import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import java.util.Arrays +import java.util.HashMap +import java.util.LinkedList +import java.util.List +import java.util.Map +import java.util.Set + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class AlloyModelInterpretation implements LogicModelInterpretation{ + + protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE + //protected val extension LogicProblemBuilder builder = new LogicProblemBuilder + + protected val Logic2AlloyLanguageMapper forwardMapper + protected val Logic2AlloyLanguageMapperTrace forwardTrace; + + private var ExprVar logicLanguage; + private var String logicBooleanTrue; + private var String logicBooleanFalse; + + val Map alloyAtom2LogicElement = new HashMap + private val Map> interpretationOfUndefinedType = new HashMap + + private val Map constant2Value + private val Map> function2Value + private val Map> relation2Value + + private val int minInt + private val int maxInt + + public new (A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { + + this.forwardMapper = forwardMapper + this.forwardTrace = trace + + //TMP sig maps to identify alloy signatures by their names + val Map sigName2LogicType = + forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name] + val Map elementNameNamel2DefinedElement = + forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name] + + // Fill the interpretation map with empty lists + forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)] + + // exporing individuals + for(atom: solution.allAtoms) { + val typeName = getName(atom.type) + val atomName = atom.name + //println(atom.toString + " < - " + typeName) + if(typeName == forwardTrace.logicLanguage.name) { + this.logicLanguage = atom + } else if(typeName == "Int" || typeName == "seq/Int") { + // do nothing + } else if(sigName2LogicType.containsKey(typeName) && typeName.lookup(sigName2LogicType) instanceof TypeDefinition) { + val element = elementNameNamel2DefinedElement.get(atomName.head) + alloyAtom2LogicElement.put(atom.label,element) + } else if(sigName2LogicType.containsKey(typeName)) { + val type = sigName2LogicType.get(typeName) + val elementsOfType = interpretationOfUndefinedType.get(type) + val element = createDefinedElement => [ + it.name += type.name + it.name += (elementsOfType.size+1).toString + ] + alloyAtom2LogicElement.put(atom.label,element) + elementsOfType+=element + } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { + if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } + else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} + else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') + } + else throw new UnsupportedOperationException('''Unknown atom: «atom»''') + } + + //TMP field maps + val Map name2AlloyField = new HashMap + // exploring signatures + for(sig:solution.allReachableSigs) { + for(field : sig.fields) { + name2AlloyField.put(field.label,field) + } + } + + // eval consants + constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[ + solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term + ] + // eval functions + val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function | + newHashMap( + solution.eval(function.name.lookup(name2AlloyField)) + .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])] + + val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function | + val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField) + val paramIndexes = 1..(function.parameters.size) + return newHashMap( + solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t | + new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term]) + -> + t.atom(function.parameters.size + 1).atomLabel2Term + ])] + this.function2Value = Union(hostedfunction2Value,globalfunction2Value) + // eval relations + val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation | + solution.eval(relation.name.lookup(name2AlloyField)).map[ t | + new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet] + val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation | + solution.eval(relation.name.lookup(name2AlloyField)).map[ t | + new ParameterSubstitution((1.. «v»''')] + + println('''Constants-----''') + constant2Value.forEach[k, v|println('''«k.name» : «v»''')] + println('''Functions-----''') + function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]] + println('''Relations-----''') + relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]] + } + + def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { + val name = type.toString + if(name.startsWith("{this/") && name.endsWith("}")) { + return type.toString.replaceFirst("\\{this\\/","").replace("}","") + } + else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') + } + def private getName(ExprVar atom) { atom.toString.split("\\$") } + + override getElements(Type type) { getElementsDispatch(type) } + def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) } + def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } + + override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { + val transformedParams = new ParameterSubstitution(parameterSubstitution) + return transformedParams.lookup( + function.lookup(this.function2Value) + ) + } + + override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { + relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution)) + } + + override getInterpretation(ConstantDeclaration constant) { + constant.lookup(this.constant2Value) + } + + override getMinimalInteger() { this.minInt } + override getMaximalInteger() { this.maxInt } + + // Alloy term -> logic term + def private atomLabel2Term(String label) { + if(label.number) return Integer.parseInt(label) + else if(label == this.logicBooleanTrue) return true + else if(label == this.logicBooleanFalse) return false + else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) + else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') + } + def isNumber(String s) { + try{ + Integer.parseInt(s) + return true + }catch(NumberFormatException e) { + return false + } + } +} + +class ParameterSubstitution{ + val Object[] data; + + new(Object[] data) { this.data = data } + + override equals(Object obj) { + if(obj === this) return true + else if(obj == null) return false + if(obj instanceof ParameterSubstitution) { + return Arrays.equals(this.data,obj.data) + } + return false + } + + override hashCode() { + Arrays.hashCode(data) + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ new file mode 100644 index 00000000..4f001c72 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ @@ -0,0 +1,40 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import org.eclipse.xtext.xbase.lib.Functions.Function0 +import java.util.concurrent.Executors +import java.util.concurrent.Callable +import java.util.concurrent.TimeUnit +import java.util.concurrent.TimeoutException +import java.util.concurrent.ExecutionException + +class FunctionWithTimeout { + val Function0 function; + + new(Function0 function) { + this.function = function + } + + def execute(long millisecs) { + if(millisecs>0) { + val executor = Executors.newCachedThreadPool(); + val task = new Callable() { + override Type call() { function.apply } + }; + val future = executor.submit(task); + try { + val result = future.get(millisecs, TimeUnit.MILLISECONDS); + return result + } catch (TimeoutException ex) { + // handle the timeout + } catch (InterruptedException e) { + // handle the interrupts + } catch (ExecutionException e) { + // handle other exceptions + } finally { + future.cancel(true); // may or may not desire this + } + return null + } + else return function.apply + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ new file mode 100644 index 00000000..48ec4fd4 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ @@ -0,0 +1,345 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import java.util.Map +import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant +import edu.mit.csail.sdg.alloy4compiler.ast.Expr +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall +import java.util.HashMap +import edu.mit.csail.sdg.alloy4compiler.ast.Decl +import java.util.ArrayList +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement +import edu.mit.csail.sdg.alloy4compiler.ast.Attr +import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import javax.naming.OperationNotSupportedException +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type + +class AlloyInput{ + public val List typeDeclarations=new ArrayList + public val List functionDeclarations=new ArrayList + public val List assertions=new ArrayList + public val List multiplicityConstraints=new ArrayList + public val List inverseConstraints=new ArrayList +} + +class Logic2AlloyApiMapperTrace { + val Map typeMap + val Map elementMap + //val Map functionMap + val Map relationMap + //val Map constantMap + + new () { + this.typeMap = new HashMap + this.elementMap = new HashMap + //this.functionMap = new HashMap + this.relationMap = new HashMap + //this.constantMap = new HashMap + } + new (Map typeMap, + Map elementMap, + //Map functionMap, + Map relationMap/*, + Map constantMap*/) + { + this.typeMap = typeMap + this.elementMap = elementMap + //this.functionMap = functionMap + this.relationMap = relationMap + //this.constantMap = constantMap + } + + def types() { typeMap } + def elements() { elementMap } + //def functions() { functionMap } + def relations() { relationMap } + //def constants() { constantMap } +} + +class Logic2AlloyApiMapper{ + //TODO output + public def TracedOutput, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) { + val documentInput = new AlloyInput() + //createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand] + //val document = createSMTDocument => [input = documentInput] + val List document=new ArrayList + val trace = new Logic2AlloyApiMapperTrace + + // Trafo + documentInput.typeDeclarations += problem.types.map[transformType(trace)] + //documentInput.functionDeclarations += problem.functions.map[transformFunction(trace)] + documentInput.functionDeclarations += problem.relations.map[transformRelation(trace)] + //documentInput.functionDeclarations += problem.constants.map[transformConstant(trace)] + documentInput.assertions += problem.assertions.map[transformAssertion(trace)] + + + val alloySpecification = problem.specifications.filter(AlloySpecification).head + + for(mult: alloySpecification.multiplicities){ + if(mult.min>0){ + documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace) + } + if(mult.max!=-1){ + documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace) + } + } + + for(inv: alloySpecification.inverses){ + documentInput.inverseConstraints += inv.transformInverse(trace) + } + // End trafo + + return new TracedOutput(document,trace) + } + + def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){ + + val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl + return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable) + + } + + def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){ + + val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl + return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable) + + } + + def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){ + return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose) + } + + private def toID(List names) {names.join("!") } + + def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) { + val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT) + trace.types.put(declaration,result) + return result + } + + def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) { + val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE) + trace.elements.put(element,result) + return result + } + + def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) { + //TODO �r�kles, absztrakt + val result = new PrimSig(declaration.name.toID) + trace.types.put(declaration,result) + return result + } + + def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) { + throw new UnsupportedOperationException("BoolTypeReference is not supported.") + } + def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) { + return PrimSig.SIGINT + } + def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) { + throw new UnsupportedOperationException("RealTypeReference is not supported.") + } + def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) { + return trace.types.get(complexTypeReference.referred) + } + + /*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) { + val functionDeclaration = createSMTFunctionDeclaration => [ + name = declaration.name.toID + range = declaration.range.transformTypeReference(trace) + parameters+= declaration.parameters.map[transformTypeReference(trace)] + ] + trace.functions.put(declaration,functionDeclaration) + return functionDeclaration + }*/ + + def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) { + if(relation.parameters.size==2){ + trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf)) + } else{ + throw new OperationNotSupportedException("More parameters are not supported.") + } + } + + /*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) { + val smtConstant = createSMTFunctionDeclaration => [ + name = constant.name.toID + range = transformTypeReference(constant.type, trace) + ] + trace.constants.put(constant,smtConstant) + return smtConstant + }*/ + + def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) { + + return assertion.value.transformTerm(trace,emptyMap) + } + + def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map variables) { + throw new UnsupportedOperationException("Bool is not supported") + //open util/boolean, autoPay: Bool + //https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142 + } + def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map variables) { + return ExprConstant.makeNUMBER(literal.value) + } + def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map variables) { + throw new UnsupportedOperationException("Real number is not supported") + } + def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map variables) { + return not.operand.transformTerm(trace,variables).not} + def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map variables) { + val List operands= and.operands.map[transformTerm(trace,variables)] + var andTerm=operands.get(0) + for(Integer i: 1..(operands.size-1)){ + andTerm=andTerm.and(operands.get(i)) + } + return andTerm + } + def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map variables) { + val List operands= or.operands.map[transformTerm(trace,variables)] + var orTerm=operands.get(0) + for(Integer i: 1..(operands.size-1)){ + orTerm=orTerm.or(operands.get(i)) + } + return orTerm + } + def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map variables) { + return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map variables) { + return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map variables) { + return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map variables) { + return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables)) + } + /*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map variables) { + createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/ + def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map variables) { + return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map variables) { + return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map variables) { + return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map variables) { + return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables)) + } + def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map variables) { + throw new UnsupportedOperationException("Modulo is not supported.") + } + def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map variables) { + return configureForall(forall,trace,variables) + } + def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map variables) { + return configureExists(exists,trace,variables) + } + def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map variables) { + symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } + + def private configureForall( + Forall quantifiedExpression, + Logic2AlloyApiMapperTrace trace, Map variables) + { + val allVariables = new HashMap(variables) + val newAlloyVariables = new ArrayList(quantifiedExpression.quantifiedVariables.size) + + for(logicVariable: quantifiedExpression.quantifiedVariables) { + val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl + allVariables.put(logicVariable, newAlloyVariable) + newAlloyVariables += newAlloyVariable + } + val variable0=newAlloyVariables.get(0) + newAlloyVariables.remove(0) + return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables) + } + + def private configureExists( + Exists quantifiedExpression, + Logic2AlloyApiMapperTrace trace, Map variables) + { + val allVariables = new HashMap(variables) + val newAlloyVariables = new ArrayList(quantifiedExpression.quantifiedVariables.size) + + for(logicVariable: quantifiedExpression.quantifiedVariables) { + val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl + allVariables.put(logicVariable, newAlloyVariable) + newAlloyVariables += newAlloyVariable + } + val variable0=newAlloyVariables.get(0) + newAlloyVariables.remove(0) + return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables) + } + + def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + return trace.elements.get(referred) + } + def dispatch protected Expr transformSymbolicReference(Variable variable, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + return variables.get(variable).get + } + /*def dispatch protected Expr transformSymbolicReference(Function function, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + val result = createSMTSymbolicValue => [sv | sv.symbolicReference = trace.functions.get(function)] + for(paramSubstitution : parameterSubstitutions) { + result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables)) + } + return result + }*/ + def dispatch protected Expr transformSymbolicReference(Relation relation, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + return trace.relations.get(relation) + } + def dispatch protected Expr transformSymbolicReference(Constant constant, List parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map variables) { + //createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)] + throw new UnsupportedOperationException("Constant is not supported") + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes new file mode 100644 index 00000000..f5f5a9b6 --- /dev/null +++ b/Solvers/Alloy-Solver2/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes @@ -0,0 +1,74 @@ +/*def dispatch boolean hasDeclaredElement(TypeDefinition type) { return false; } + def dispatch boolean hasDeclaredElement(TypeDeclaration type) { + if(type.isAbstract) { + type.subtypes.exists[it.hasDeclaredElement] + } else return true; + } + + def dispatch List allEnumSubtypes(TypeDefinition type) { return #[type] } + def dispatch List allEnumSubtypes(TypeDeclaration type) { + return type.subtypes.map[it.allEnumSubtypes].flatten.toList + } + + def protected transformTypes(List types, Logic2AlloyLanguageMapperTrace trace) { + val Map signatureTrace = new HashMap; + + // Creating the root type + val objectType = createALSSignatureDeclaration => [ name=#["util","object"].toID it.abstract = true ] + trace.objectSupperClass = objectType + trace.specification.typeDeclarations += objectType + + // Creating the images of the types + for(type : types) { + if(type instanceof TypeDefinition) { + if(type.elements.empty) { + trace.type2ALSType.put(type,#[]); + } else { + val e = createALSEnumDeclaration => [ + it.name = type.name.toID + it.literal += type.elements.map[transformDefinedElement(trace)] + ] + trace.type2ALSType.put(type,#[e]) + trace.specification.typeDeclarations += e + } + } + else if(type instanceof TypeDeclaration) { + if(hasDeclaredElement(type)) { + val s = createALSSignatureDeclaration => [ + name=type.name.toID + it.abstract = type.isIsAbstract + ] + trace.type2ALSType.put(type,new LinkedList=>[add(s)]) + signatureTrace.put(type, s) + trace.specification.typeDeclarations += s + } + else { + signatureTrace.put(type, null) + trace.type2ALSType.put(type,new LinkedList);// empty + } + } + else throw new IllegalArgumentException('''Unknown type «type.class.name»''') + } + + + for(type: types.filter(TypeDeclaration)) { + // Adding inheritance + val s = type.lookup(signatureTrace) + if(s!=null) { + for(supertype : type.supertypes) { + s.supertype += (supertype as TypeDeclaration).lookup(signatureTrace) + } + if(type.supertypes.empty) { + s.supertype += objectType + } + } + // Adding enum subtypes + type.lookup(trace.type2ALSType)+=type.allEnumSubtypes.map[it.lookup(trace.type2ALSType)].flatten + } + } + + def protected transformDefinedElement(DefinedElement element, Logic2AlloyLanguageMapperTrace trace) { + val result = createALSEnumLiteral => [name = element.name.toID] + trace.definedElement2EnumProperty.put(element,result) + return result + }*/ \ No newline at end of file -- cgit v1.2.3-70-g09d2