From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../.classpath | 11 + .../.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 | 10 + .../plugin.properties | 4 + .../plugin.xml | 21 + .../alloy/reasoner/queries/signatureQueries.vql | 17 + .../alloy/reasoner/queries/typeQueries.vql | 85 ++++ .../reasoner/AlloyAnalyzerConfiguration.xtend | 32 ++ .../dlsreasoner/alloy/reasoner/AlloySolver.xtend | 72 ++++ .../alloy/reasoner/builder/Alloy2LogicMapper.xtend | 48 +++ .../alloy/reasoner/builder/AlloyHandler.xtend | 145 +++++++ .../builder/AlloyModelInterpretation.xtend | 331 +++++++++++++++ .../builder/Logic2AlloyLanguageMapper.xtend | 467 +++++++++++++++++++++ .../builder/Logic2AlloyLanguageMapperTrace.xtend | 49 +++ .../Logic2AlloyLanguageMapper_ConstantMapper.xtend | 43 ++ .../Logic2AlloyLanguageMapper_Containment.xtend | 260 ++++++++++++ .../Logic2AlloyLanguageMapper_FunctionMapper.xtend | 87 ++++ .../Logic2AlloyLanguageMapper_RelationMapper.xtend | 111 +++++ .../Logic2AlloyLanguageMapper_Support.xtend | 207 +++++++++ .../Logic2AlloyLanguageMapper_TypeMapper.xtend | 16 + ...oyLanguageMapper_TypeMapper_FilteredTypes.xtend | 268 ++++++++++++ ...yLanguageMapper_TypeMapper_Horizontal.xtend_old | 428 +++++++++++++++++++ ...apper_TypeMapper_InheritanceAndHorizontal.xtend | 50 +++ .../unused/AlloyModelInterpretation.xtend_ | 212 ++++++++++ .../unused/FunctionWithTimeout.xtend_ | 40 ++ .../unused/Logic2AlloyApiMapper.xtend_ | 345 +++++++++++++++ .../unused/oldTypes | 74 ++++ .../.classpath | 9 + .../.gitignore | 4 + .../.project | 34 ++ .../.settings/org.eclipse.core.resources.prefs | 2 + .../.settings/org.eclipse.jdt.core.prefs | 7 + .../META-INF/MANIFEST.MF | 27 ++ .../build.properties | 6 + .../plugin.xml | 398 ++++++++++++++++++ .../plugin.xml_gen | 425 +++++++++++++++++++ .../inf/dslreasoner/ui/AlloyLanguageUiModule.java | 15 + .../AlloyLanguageProposalProvider.xtend | 12 + .../AlloyLanguageDescriptionLabelProvider.xtend | 24 ++ .../ui/labeling/AlloyLanguageLabelProvider.xtend | 29 ++ .../outline/AlloyLanguageOutlineTreeProvider.xtend | 13 + .../quickfix/AlloyLanguageQuickfixProvider.xtend | 26 ++ .../.classpath | 9 + .../.gitignore | 4 + ....bme.mit.inf.dslreasoner.alloy.language).launch | 18 + .../.project | 34 ++ .../.settings/org.eclipse.core.resources.prefs | 2 + .../.settings/org.eclipse.jdt.core.prefs | 12 + .../META-INF/MANIFEST.MF | 37 ++ .../build.properties | 7 + .../model/generated/AlloyLanguage.ecore | 267 ++++++++++++ .../model/generated/AlloyLanguage.genmodel | 206 +++++++++ .../plugin.xml | 16 + .../plugin.xml_gen | 16 + .../hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext | 149 +++++++ .../dslreasoner/AlloyLanguageRuntimeModule.java | 11 + .../dslreasoner/AlloyLanguageStandaloneSetup.java | 16 + .../mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 | 133 ++++++ .../formatting/AlloyLanguageFormatter.xtend | 96 +++++ .../generator/AlloyLanguageGenerator.xtend | 24 ++ .../scoping/AlloyLanguageScopeProvider.xtend | 81 ++++ .../validation/AlloyLanguageValidator.xtend | 24 ++ 67 files changed, 5761 insertions(+) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend create mode 100644 Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old create mode 100644 Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.classpath create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.gitignore create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.project create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.settings/org.eclipse.core.resources.prefs create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/META-INF/MANIFEST.MF create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/build.properties create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml_gen create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/AlloyLanguageUiModule.java create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/AlloyLanguageProposalProvider.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageDescriptionLabelProvider.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageLabelProvider.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/AlloyLanguageOutlineTreeProvider.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/AlloyLanguageQuickfixProvider.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.classpath create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.gitignore create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.project create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.core.resources.prefs create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.jdt.core.prefs create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/META-INF/MANIFEST.MF create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/build.properties create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.ecore create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.genmodel create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml_gen create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend (limited to 'Solvers/Alloy-Solver') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath new file mode 100644 index 00000000..de68b5f7 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.classpath @@ -0,0 +1,11 @@ + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.gitignore new file mode 100644 index 00000000..e42fe9ea --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.project new file mode 100644 index 00000000..a1c16519 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.incquery.patternlanguage.emf.EMFPatternLanguage.prefs new file mode 100644 index 00000000..7d03706a --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..295926d9 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/.settings/org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguage.prefs new file mode 100644 index 00000000..c6f56e64 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/META-INF/MANIFEST.MF new file mode 100644 index 00000000..13ad2d10 --- /dev/null +++ b/Solvers/Alloy-Solver/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, + hu.bme.mit.inf.dlsreasoner.alloy.reasoner.queries.util +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;bundle-version="[1.2.0,2.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" +Bundle-RequiredExecutionEnvironment: JavaSE-1.8 +Bundle-ActivationPolicy: lazy +Import-Package: org.apache.log4j;version="1.2.15" diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties new file mode 100644 index 00000000..bb9e5d4d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/build.properties @@ -0,0 +1,10 @@ +bin.includes = .,\ + model/,\ + META-INF/,\ + plugin.xml,\ + plugin.properties +jars.compile.order = . +source.. = ecore-gen/,\ + src/,\ + src-gen/ +output.. = bin/ diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.properties new file mode 100644 index 00000000..14541a0a --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml new file mode 100644 index 00000000..23c55a4d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/plugin.xml @@ -0,0 +1,21 @@ + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/signatureQueries.vql new file mode 100644 index 00000000..a020953c --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/queries/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/queries/typeQueries.vql new file mode 100644 index 00000000..8d93cafb --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend new file mode 100644 index 00000000..cdf21174 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend @@ -0,0 +1,32 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner + +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration + +class AlloySolverConfiguration extends LogicSolverConfiguration { + /*public var boolean createCommonSupertype + public var int intScope = 1 // 5 by default + public def setIntScopeFor(int max) { + intScope = 31 - Integer.numberOfLeadingZeros(max) + 1 + }*/ + public var int symmetry = 0 // by default + public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J + public var boolean writeToFile = false +} + +enum AlloyBackendSolver { + BerkMinPIPE, + SpearPIPE, + MiniSatJNI, + MiniSatProverJNI, + LingelingJNI, + PLingelingJNI, + GlucoseJNI, + CryptoMiniSatJNI, + SAT4J, + CNF, + KodKod +} + +enum TypeMappingTechnique { + FilteredTypes +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend new file mode 100644 index 00000000..7dfc3161 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloySolver.xtend @@ -0,0 +1,72 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner + +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.MonitoredAlloySolution +import hu.bme.mit.inf.dslreasoner.AlloyLanguageStandaloneSetupGenerated +import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguagePackage +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 +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder.AlloyModelInterpretation_TypeInterpretation_FilteredTypes +import org.eclipse.emf.common.util.URI + +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 { + if(configuration instanceof AlloySolverConfiguration) { + val transformationStart = System.currentTimeMillis + val result = forwardMapper.transformProblem(problem,configuration) + val alloyProblem = result.output + + /*val x = alloyProblem.eAllContents.filter(ALSFunctionCall).filter[it.referredDefinition == null].toList + println(x)*/ + val forwardTrace = result.trace + + var String fileURI = null; + var String alloyCode = null; + if(configuration.writeToFile) { + fileURI = workspace.writeModel(alloyProblem,fileName).toFileString + } else { + alloyCode = workspace.writeModelToString(alloyProblem,fileName) + } + + //val alloyCode = workspace.readText(fileName) + //val FunctionWithTimeout call = new FunctionWithTimeout[] + + val transformationTime = System.currentTimeMillis - transformationStart + val result2 = handler.callSolver(alloyProblem,workspace,configuration,fileURI,alloyCode) + workspace.deactivateModel(fileName) + val logicResult = backwardMapper.transformOutput(problem,result2,forwardTrace,transformationTime) + return logicResult + } else throw new IllegalArgumentException('''The configuration have to be an «AlloySolverConfiguration.simpleName»!''') + } + + override getInterpretation(ModelResult modelResult) { + return new AlloyModelInterpretation( + new AlloyModelInterpretation_TypeInterpretation_FilteredTypes, + (modelResult.representation as MonitoredAlloySolution).solution, + forwardMapper, + modelResult.trace as Logic2AlloyLanguageMapperTrace + ); + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend new file mode 100644 index 00000000..637752b0 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Alloy2LogicMapper.xtend @@ -0,0 +1,48 @@ +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, MonitoredAlloySolution solution, Logic2AlloyLanguageMapperTrace trace, long transformationTime) { + if(solution == null) { + return createInsuficientResourcesResult => [ + it.problem = problem + it.statistics = transformStatistics(solution,transformationTime) + ] + } else { + val logicResult = solution.solution + if(logicResult.satisfiable) { + return createModelResult => [ + it.problem = problem + it.representation += solution + it.maxInteger = logicResult.max + it.minInteger = logicResult.min + it.trace = trace + it.statistics = transformStatistics(solution,transformationTime) + ] + } else { + return createInconsistencyResult => [ + it.problem = problem + //trace? + it.statistics = transformStatistics(solution,transformationTime) + ] + } + } + } + + def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { + createStatistics => [ + it.transformationTime = transformationTime as int + if(solution != null) { + it.solverTime = solution.runtimeTime as int + it.entries += LogicresultFactory.eINSTANCE.createIntStatisticEntry => [ + it.name = "KoodkodToCNFTransformationTime" + it.value = solution.getKodkodTime as int + ] + } + ] + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend new file mode 100644 index 00000000..6bac4130 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyHandler.xtend @@ -0,0 +1,145 @@ +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.A4Solution +import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod +import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace +import java.util.LinkedList +import java.util.List +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloyBackendSolver +import org.eclipse.xtend.lib.annotations.Data +import java.util.Map +import java.util.HashMap +import edu.mit.csail.sdg.alloy4compiler.translator.A4Options.SatSolver +import org.eclipse.emf.common.CommonPlugin +import java.util.ArrayList +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration + +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 + long runtimeTime + + A4Solution solution +} + +class AlloyHandler { + + //val fileName = "problem.als" + + public def callSolver(ALSDocument problem, ReasonerWorkspace workspace, AlloySolverConfiguration configuration, String path, 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.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString + ] + + // Transform + var Command command = null; + var CompModule compModule = null + + val kodkodTransformStart = System.currentTimeMillis(); + + try { + if(configuration.writeToFile) { + compModule = CompUtil.parseEverything_fromFile(reporter,null,path) + } else { + 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 + + //Execute + var A4Solution answer = null; + try { + answer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) + }catch(Exception e) { + warnings +=e.message + } + + var long runtimeFromAnswer; + if(runtime.empty) { + runtimeFromAnswer = System.currentTimeMillis - (kodkodTransformStart + kodkodTransformFinish) + } else { + runtimeFromAnswer = runtime.head + } + + return new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,runtimeFromAnswer,answer) + } + + 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) + } +} + +@Data class SolverConfiguration { + AlloyBackendSolver backedSolver + String path + String[] options +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend new file mode 100644 index 00000000..d00291e0 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend @@ -0,0 +1,331 @@ +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.* +import edu.mit.csail.sdg.alloy4compiler.ast.Sig +import java.util.ArrayList + +interface AlloyModelInterpretation_TypeInterpretation { + def void resolveUnknownAtoms( + Iterable objectAtoms, + A4Solution solution, + Logic2AlloyLanguageMapperTrace forwardTrace, + Map name2AlloySig, + Map name2AlloyField, + Map expression2DefinedElement, + Map> interpretationOfUndefinedType) +} + +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) + } + } + } +} +/* +class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{ + protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE + + override resolveUnknownAtoms(Iterable objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map alloyAtom2LogicElement) { + val Map> interpretationOfUndefinedType = new HashMap; + + //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: objectAtoms) { + val typeName = getName(atom.type) + //val atomName = atom.name + + 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 throw new UnsupportedOperationException('''Unknown atom: «atom»''') + } + + return interpretationOfUndefinedType + } + + 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("\\$") } +}*/ + +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 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.allAtoms) + 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(Iterable 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") { + // do nothing, integers will be parsed from the string + } 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 unknownAtoms += atom + } + + 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) + } + + 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 private isNumber(String s) { + try{ + Integer.parseInt(s) + return true + }catch(NumberFormatException e) { + return false + } + } +} + +/** + * 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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend new file mode 100644 index 00000000..23b9027f --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend @@ -0,0 +1,467 @@ +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.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.logic.model.builder.LogicSolverConfiguration +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.SymbolicValue +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +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.* +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation +import java.util.Collection +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct + +class Logic2AlloyLanguageMapper { + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + @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 + } + + 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)) + ] + + typeMapper.transformTypes(problem.types,problem.elements,this,trace) + + trace.constantDefinitions = problem.collectConstantDefinitions + trace.functionDefinitions = problem.collectFunctionDefinitions + trace.relationDefinitions = problem.collectRelationDefinitions + + problem.constants.forEach[this.constantMapper.transformConstant(it,trace)] + problem.functions.forEach[this.functionMapper.transformFunction(it, trace)] + problem.relations.forEach[this.relationMapper.transformRelation(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) + } + } + + transformRunCommand(specification, trace, config) + + return new TracedOutput(specification,trace) + } + + 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 { + throw new IllegalArgumentException('''Lower multiplicity is already set!''') + } + } + private def addUpper(ALSMultiplicity multiplicity) { + if(multiplicity === ALSMultiplicity::SET || multiplicity === null) { + return ALSMultiplicity::LONE + } else if(multiplicity === ALSMultiplicity::SOME) { + 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 + } + + //////////////////// + // 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) {throw new UnsupportedOperationException('''Real types are not supported in Alloy.''')} + 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]]) + } + + ////////////// + // Scopes + ////////////// + + def transformRunCommand(ALSDocument specification, Logic2AlloyLanguageMapperTrace trace, AlloySolverConfiguration config) { + specification.runCommand = createALSRunCommand => [ + it.typeScopes+= createALSSigScope => [ + it.type= typeMapper.getUndefinedSupertype(trace) + it.number = typeMapper.getUndefinedSupertypeScope(config.typeScopes.maxNewElements,trace) + //it.exactly = (config.typeScopes.maxElements == config.typeScopes.minElements) + ] + if(config.typeScopes.maxIntScope == LogicSolverConfiguration::Unlimited) throw new UnsupportedOperationException( + '''An integer scope have to be specified for Alloy!''') + it.typeScopes += createALSIntScope => [ + number = Integer.SIZE-Integer.numberOfLeadingZeros(config.typeScopes.maxIntScope) + ] +// for(definedScope : config.typeScopes.allDefinedScope) { +// it.typeScopes += createALSSigScope => [ +// it.type = definedScope.type.lookup(trace.type2ALSType) +// it.number = definedScope.upperLimit +// it.exactly = (definedScope.upperLimit == definedScope.lowerLimit) +// ] +// } + ] + } + + + ////////////// + // 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) { + throw new UnsupportedOperationException("RealLiteral is not supported") + } + 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(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(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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend new file mode 100644 index 00000000..22f49c98 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapperTrace.xtend @@ -0,0 +1,49 @@ +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 + +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 var Map constantDefinitions + public var Map functionDefinitions + public var Map relationDefinitions +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_ConstantMapper.xtend b/Solvers/Alloy-Solver/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..401c2ec2 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Containment.xtend b/Solvers/Alloy-Solver/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..fd519c1e --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_FunctionMapper.xtend b/Solvers/Alloy-Solver/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..ff18ef80 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend new file mode 100644 index 00000000..9dd4da2f --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_RelationMapper.xtend @@ -0,0 +1,111 @@ +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.* + +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 protected void transformRelation(RelationDeclaration r, Logic2AlloyLanguageMapperTrace trace) { + if(!trace.relationDefinitions.containsKey(r)) { + if(r.transformToHostedField(trace)) { + transformRelationDeclarationToHostedField(r,trace) + } else { + transformRelationDeclarationToGlobalField(r,trace) + } + } + } + + 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 protected 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) + } + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_Support.xtend b/Solvers/Alloy-Solver/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..39896c27 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver/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..9927f1cc --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend @@ -0,0 +1,16 @@ +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) +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend new file mode 100644 index 00000000..ade9860b --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend @@ -0,0 +1,268 @@ +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 java.util.Map + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes + implements Logic2AlloyLanguageMapper_TypeMapperTrace +{ + public var ALSSignatureDeclaration objectSupperClass; + public val Map type2ALSType = new HashMap; + public val Map definedElement2Declaration = new HashMap +} +/** + * 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) { + return undefinedScope + trace.typeTrace.definedElement2Declaration.size + } + +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old new file mode 100644 index 00000000..7383904d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old @@ -0,0 +1,428 @@ +package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity +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.ComplexTypeReference +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.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher +import java.util.HashMap +import java.util.LinkedHashSet +import java.util.LinkedList +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.Data + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* + +class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal + implements Logic2AlloyLanguageMapper_TypeMapperTrace { + public var ALSSignatureDeclaration declaredSupertype + public var ALSSignatureDeclaration definedSupertype + public val Map definedElement2Declaration = new HashMap + + public val Map definition2definition = new HashMap + public val Map declaration2definition = new HashMap + public val Map undefined2definition = new HashMap + public val Map new2declaration = new HashMap + + def getAllDefinedTypes() { + return (definition2definition.values) + + (declaration2definition.values) + + (undefined2definition.values) + } + def getAllDeclaredTypes() { + return new2declaration.values + } + + public val Map> type2AllSignatures = new HashMap; +} + +@Data +class DynamicTypeConstraints { + List> positiveCNF + LinkedHashSet negative + public new() { + this.positiveCNF = new LinkedList + this.negative = new LinkedHashSet + } + def public void addPositiveTypeOptions(List typeDisjunction) { + this.positiveCNF.add(typeDisjunction) + } + def public void addNegativeTypes(Iterable negativeTypes) { + this.negative.addAll(negativeTypes) + } +} + +/** + * Dynamic types are represented by disjoint sets, and + * static types are represented by the union of the dynamic type sets. + * + * Definition Declaration + * | / \ + * | W/DefinedSuper Wo/DefinedSuper + * | | / \ + * | | undefined2declaration new2declaration + * definition2definition definition2declaration + * +----------------------------------------------------+ +-------------+ + * Defined Declared + */ +class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{ + private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support; + private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE + + override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + // 0. Creating the traces + val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal + trace.typeMapperTrace = typeTrace + /** + * Static type -> list of possible dynamic type map + */ + val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace) + + + + // 1. Transforming the types + + // There are two kind of types: + // A: one with defined supertypes (including itself), that only has defined elements + // Those types can have instances only from the defined elements, ie they are subset of problem.elements + // B: one without defined supertypes + // Those types can have instances from two sources + // B.1 from elements that dont have definitions + // B.2 from newly created elements + val allConcreteTypes = problem.types.filter[!it.isAbstract] + val definitions = allConcreteTypes.filter(TypeDefinition).toList + val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList + val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList + + // 2. If there are defined elements + if(trace.typeTrace.definedSupertype != null) { + // 3 mapping the elements + problem.elements.transformDefinedSupertype(trace) + // 4. if there are elements that are added to types, then it have to be mapped to defined parts + if(problem.elements.exists[!it.definedInType.empty]) { + definitions.forEach[it.transformDefinition2Definition(trace)] + declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)] + } + // 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions + if(problem.elements.exists[it.definedInType.empty]) { + declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)] + } + + definedConcreteTypesAreFull(trace) + definedConcreteTypesAreDisjoint(trace) + problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace) + } + + // Transforming the declared and defined concrete types + problem.elements.transformDefinedSupertype(trace) + if(trace.typeTrace.definedSupertype != null) { + problem.elements.transformDefinedElements(trace) + declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)] + } + + // 2: Caching the types by filling type2AllSignatures + for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) { + val type = typeToConcreteSubtypesEntry.key + val List signatures = new LinkedList + + } + } + + def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) { + val res = trace.typeMapperTrace + if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) { + return res + } else { + throw new IllegalArgumentException(''' + Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name», + but found «res.class.name»''') + } + } + + 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] + } + } + + private def transformDefinedSupertype(List elements, Logic2AlloyLanguageMapperTrace trace) { + trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [ + it.name = support.toID(#["util","defined","Object"]) + ] + trace.specification.signatureBodies += createALSSignatureBody => [ + it.abstract = true + it.declarations += trace.typeTrace.definedSupertype + ] + } + + private def transformDefinedElements(List elements, + Logic2AlloyLanguageMapperTrace trace){ + if(trace.typeTrace.definedSupertype != null) { + // 2. Create elements as singleton signatures subtype of definedSupertype + val elementBodies = createALSSignatureBody => [ + it.multiplicity = ALSMultiplicity::ONE + it.supertype = trace.typeTrace.definedSupertype + ] + trace.specification.signatureBodies += elementBodies + for(element : elements) { + val elementDeclaration = createALSSignatureDeclaration => [ + it.name = support.toIDMultiple(#["element"],element.name) + ] + elementBodies.declarations += elementDeclaration + trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration) + } + // 3. Specify that definedSupertype is equal to the union of specified + /*trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util","typehierarchy","definitionOfElements"]) + it.term = createALSEquals => [ + it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype] + it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[ + it.referred = element.lookup(trace.typeTrace.definedElement2Declaration) + ]]) + ] + ]*/ + } + } + + ///// Type definitions + + protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) { + val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)] + val body = createALSSignatureBody => [ + it.declarations += sig + it.superset += trace.typeTrace.definedSupertype + ] + trace.specification.signatureBodies += body + trace.typeTrace.definition2definition.put(type,sig) + } + protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { + val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)] + val body = createALSSignatureBody => [ + it.declarations += sig + it.superset += trace.typeTrace.definedSupertype + ] + trace.specification.signatureBodies += body + trace.typeTrace.declaration2definition.put(type,sig) + } + protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { + val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)] + val body = createALSSignatureBody => [ + it.declarations += sig + it.supertype = trace.typeTrace.definedSupertype + ] + trace.specification.signatureBodies += body + trace.typeTrace.undefined2definition.put(type,sig) + } + protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) { + val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)] + val body = createALSSignatureBody => [ + it.declarations += sig + it.supertype = trace.typeTrace.declaredSupertype + ] + trace.specification.signatureBodies += body + trace.typeTrace.new2declaration.put(type,sig) + } + + /** + * The dynamic types cover each concrete types + */ + protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) { + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util","typehierarchy","elementFull"]) + it.term = createALSEquals => [ + it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype] + it.rightOperand = support.unfoldPlus( + trace.typeTrace.allDefinedTypes.map[type| + createALSReference=>[referred = type] + ].toList + ) + ] + ] + + } + /** + * The dynamic types are disjoint + */ + protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) { + val types = trace.getTypeTrace.allDefinedTypes.toList + if (types.size >= 2) { + trace.specification.factDeclarations += createALSFactDeclaration => [ + it.name = support.toID(#["util", "typehierarchy", "elementFull"]) + it.term = types.disjointSets + ] + } + } + /** + * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not + */ + protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) { + val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes) + for(constraintOnElement : constraintOnElements.entrySet) { + val element = constraintOnElement.key + val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration) + val constraint = constraintOnElement.value + + var ALSTerm negativeConstraints; + if(constraint.negative.isEmpty) { + negativeConstraints = null + } else { + negativeConstraints = support.unfoldAnd(constraint.negative.map[type| + createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ] + ].toList) + } + + var ALSTerm positiveTypeConstraints + if(constraint.positiveCNF.isEmpty) { + positiveTypeConstraints = null + } else { + positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition | + support.unfoldOr(typeConstraintFromDefinition.map[type | + elementInDefinedType(elementSignature,type,trace) + ].toList,trace) + ]) + } + + var ALSTerm typeConstraint + if(negativeConstraints != null && positiveTypeConstraints == null) { + typeConstraint = negativeConstraints + } else if (negativeConstraints == null && positiveTypeConstraints != null) { + typeConstraint = positiveTypeConstraints + } else if (negativeConstraints != null && positiveTypeConstraints != null) { + val and = createALSAnd + and.leftOperand = positiveTypeConstraints + and.rightOperand = negativeConstraints + typeConstraint = and + } else { + typeConstraint = null + } + + if(typeConstraint != null) { + val fact = createALSFactDeclaration => [ + name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name) + ] + fact.term = typeConstraint + trace.specification.factDeclarations +=fact + } + // otherwise there is no type constraint on element + } + } + + private def elementInDefinedType( + ALSSignatureDeclaration elementSignature, + Type type, + Logic2AlloyLanguageMapperTrace trace) + { + var ALSSignatureDeclaration signature + if(type instanceof TypeDeclaration) { + if(trace.typeTrace.declaration2definition.containsKey(type)) { + signature = type.lookup(trace.typeTrace.declaration2definition) + } else if(trace.typeTrace.undefined2definition.containsKey(type)) { + signature = type.lookup(trace.typeTrace.undefined2definition) + } else { + return null + } + } else if(type instanceof TypeDefinition) { + if(trace.typeTrace.definition2definition.containsKey(type)) { + signature = type.lookup(trace.typeTrace.definition2definition) + } else { + return null + } + } else throw new IllegalArgumentException('''Unknownt type «type.class.name»''') + + val finalSignature = signature + return createALSSubset => [ + leftOperand = createALSReference => [ + referred = elementSignature + ] + rightOperand = createALSReference => [ + referred = finalSignature + ] + ] + } + + def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) { + if(trace.incqueryEngine == null) { + trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem)) + } + val matcher = SupertypeStarMatcher.on(trace.incqueryEngine) + val Map> typeToConcreteSubtypes = new HashMap + for(supertype : problem.types) { + typeToConcreteSubtypes.put( + supertype, + matcher.getAllValuesOfsubtype(supertype) + .filter[!it.isIsAbstract].toList) + } + return typeToConcreteSubtypes + } + + /** + * Gives type constraints in a form of CNF + */ + def private Map typeConstraints(List elements, Map> typeToConcreteSubtypes) { + val Map constraints = new HashMap + elements.forEach[constraints.put(it,new DynamicTypeConstraints)] + + for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) { + val subtypes = type.lookup(typeToConcreteSubtypes) + for(elementInType:type.elements) { + elementInType.lookup(constraints).addPositiveTypeOptions(subtypes) + } + for(elementNotInType:elements.filter[!type.elements.contains(it)]) { + elementNotInType.lookup(constraints).addNegativeTypes(subtypes) + } + } + + return constraints + } + + private def ALSTerm disjointSets(List signatures) { + if(signatures.size >= 2){ + val top = createALSEquals => [ + it.leftOperand = signatures.intersectionOfTypes + it.rightOperand = createALSNone + ] + if(signatures.size > 2) { + return createALSAnd => [ + it.leftOperand = top + it.rightOperand = signatures.subList(1,signatures.size).disjointSets + ] + } else{ + return top + } + } else { + throw new UnsupportedOperationException() + } + } + + private def ALSIntersection intersectionOfTypes(List signatures) { + if(signatures.size == 2) { + return createALSIntersection => [ + leftOperand = createALSReference => [it.referred = signatures.get(0)] + rightOperand = createALSReference => [it.referred = signatures.get(1)] + ] + } else if(signatures.size > 2) { + return createALSIntersection => [ + leftOperand = createALSReference => [it.referred = signatures.get(0)] + rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes + ] + } else throw new UnsupportedOperationException() + } + + + override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + //trace.typeTrace. + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/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..6533ad36 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend @@ -0,0 +1,50 @@ +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 hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem +import java.util.HashMap +import java.util.Map +import java.util.Collection + +class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { + val Map newElementTypes = new HashMap + val Map definedElementTypes = new HashMap + var ALSSignatureDeclaration undefinedSupertype + var ALSSignatureDeclaration definedSupertype +} + +class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ + + override transformTypes(Collection types, Collection elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + 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] + } + } + + override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } + + override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { + throw new UnsupportedOperationException("TODO: auto-generated method stub") + } +} \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ new file mode 100644 index 00000000..05b97b0c --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ new file mode 100644 index 00000000..8c03af6e --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ new file mode 100644 index 00000000..29acd681 --- /dev/null +++ b/Solvers/Alloy-Solver/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-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes new file mode 100644 index 00000000..5e349ac8 --- /dev/null +++ b/Solvers/Alloy-Solver/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 diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.classpath b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.classpath new file mode 100644 index 00000000..f5ffadb8 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.classpath @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.gitignore b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.gitignore new file mode 100644 index 00000000..8ae4e44d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.gitignore @@ -0,0 +1,4 @@ +/bin/ +/src-gen/ +/vql-gen/ +/xtend-gen/ diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.project b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.project new file mode 100644 index 00000000..25768d12 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.project @@ -0,0 +1,34 @@ + + + hu.bme.mit.inf.dslreasoner.alloy.language.ui + + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + + org.eclipse.jdt.core.javanature + org.eclipse.pde.PluginNature + org.eclipse.xtext.ui.shared.xtextNature + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.settings/org.eclipse.core.resources.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 00000000..4824b802 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/=UTF-8 diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.settings/org.eclipse.jdt.core.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..11f6e462 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/.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.7 +org.eclipse.jdt.core.compiler.compliance=1.7 +org.eclipse.jdt.core.compiler.problem.assertIdentifier=error +org.eclipse.jdt.core.compiler.problem.enumIdentifier=error +org.eclipse.jdt.core.compiler.source=1.7 diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/META-INF/MANIFEST.MF new file mode 100644 index 00000000..a6ff6ade --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/META-INF/MANIFEST.MF @@ -0,0 +1,27 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: hu.bme.mit.inf.dslreasoner.alloy.language.ui +Bundle-Vendor: My Company +Bundle-Version: 1.0.0.qualifier +Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.alloy.language.ui; singleton:=true +Bundle-ActivationPolicy: lazy +Require-Bundle: hu.bme.mit.inf.dslreasoner.alloy.language;visibility:=reexport, + org.eclipse.xtext.ui, + org.eclipse.ui.editors;bundle-version="3.5.0", + org.eclipse.ui.ide;bundle-version="3.5.0", + org.eclipse.xtext.ui.shared, + org.eclipse.ui, + org.eclipse.xtext.builder, + org.eclipse.xtext.xbase.lib, + org.antlr.runtime, + org.eclipse.xtext.common.types.ui, + org.eclipse.xtext.ui.codetemplates.ui, + org.eclipse.compare +Import-Package: org.apache.log4j +Bundle-RequiredExecutionEnvironment: JavaSE-1.7 +Export-Package: hu.bme.mit.inf.dslreasoner.ui.quickfix, + hu.bme.mit.inf.dslreasoner.ui.contentassist, + hu.bme.mit.inf.dslreasoner.ui.contentassist.antlr, + hu.bme.mit.inf.dslreasoner.ui.internal, + hu.bme.mit.inf.dslreasoner.ui.contentassist.antlr.internal +Bundle-Activator: hu.bme.mit.inf.dslreasoner.ui.internal.AlloyLanguageActivator diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/build.properties b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/build.properties new file mode 100644 index 00000000..31255ed0 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/build.properties @@ -0,0 +1,6 @@ +source.. = src/,\ + src-gen/,\ + xtend-gen/ +bin.includes = META-INF/,\ + .,\ + plugin.xml \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml new file mode 100644 index 00000000..962a70ce --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml @@ -0,0 +1,398 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml_gen b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml_gen new file mode 100644 index 00000000..634f234b --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/plugin.xml_gen @@ -0,0 +1,425 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/AlloyLanguageUiModule.java b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/AlloyLanguageUiModule.java new file mode 100644 index 00000000..20d083e6 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/AlloyLanguageUiModule.java @@ -0,0 +1,15 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.ui; + +import org.eclipse.ui.plugin.AbstractUIPlugin; + +/** + * Use this class to register components to be used within the IDE. + */ +public class AlloyLanguageUiModule extends hu.bme.mit.inf.dslreasoner.ui.AbstractAlloyLanguageUiModule { + public AlloyLanguageUiModule(AbstractUIPlugin plugin) { + super(plugin); + } +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/AlloyLanguageProposalProvider.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/AlloyLanguageProposalProvider.xtend new file mode 100644 index 00000000..cf8d33f8 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/contentassist/AlloyLanguageProposalProvider.xtend @@ -0,0 +1,12 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.ui.contentassist + +import hu.bme.mit.inf.dslreasoner.ui.contentassist.AbstractAlloyLanguageProposalProvider + +/** + * see http://www.eclipse.org/Xtext/documentation.html#contentAssist on how to customize content assistant + */ +class AlloyLanguageProposalProvider extends AbstractAlloyLanguageProposalProvider { +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageDescriptionLabelProvider.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageDescriptionLabelProvider.xtend new file mode 100644 index 00000000..89bb0f87 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageDescriptionLabelProvider.xtend @@ -0,0 +1,24 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.labeling + +//import org.eclipse.xtext.resource.IEObjectDescription + +/** + * Provides labels for a IEObjectDescriptions and IResourceDescriptions. + * + * see http://www.eclipse.org/Xtext/documentation.html#labelProvider + */ +class AlloyLanguageDescriptionLabelProvider extends org.eclipse.xtext.ui.label.DefaultDescriptionLabelProvider { + + // Labels and icons can be computed like this: + +// override text(IEObjectDescription ele) { +// ele.name.toString +// } +// +// override image(IEObjectDescription ele) { +// ele.EClass.name + '.gif' +// } +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageLabelProvider.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageLabelProvider.xtend new file mode 100644 index 00000000..6f002921 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/labeling/AlloyLanguageLabelProvider.xtend @@ -0,0 +1,29 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.labeling + +import com.google.inject.Inject + +/** + * Provides labels for a EObjects. + * + * see http://www.eclipse.org/Xtext/documentation.html#labelProvider + */ +class AlloyLanguageLabelProvider extends org.eclipse.xtext.ui.label.DefaultEObjectLabelProvider { + + @Inject + new(org.eclipse.emf.edit.ui.provider.AdapterFactoryLabelProvider delegate) { + super(delegate); + } + + // Labels and icons can be computed like this: + +// def text(Greeting ele) { +// 'A greeting to ' + ele.name +// } +// +// def image(Greeting ele) { +// 'Greeting.gif' +// } +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/AlloyLanguageOutlineTreeProvider.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/AlloyLanguageOutlineTreeProvider.xtend new file mode 100644 index 00000000..fe3fef9d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/outline/AlloyLanguageOutlineTreeProvider.xtend @@ -0,0 +1,13 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.outline + +/** + * Customization of the default outline structure. + * + * see http://www.eclipse.org/Xtext/documentation.html#outline + */ +class AlloyLanguageOutlineTreeProvider extends org.eclipse.xtext.ui.editor.outline.impl.DefaultOutlineTreeProvider { + +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/AlloyLanguageQuickfixProvider.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/AlloyLanguageQuickfixProvider.xtend new file mode 100644 index 00000000..3e329e62 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language.ui/src/hu/bme/mit/inf/dslreasoner/ui/quickfix/AlloyLanguageQuickfixProvider.xtend @@ -0,0 +1,26 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner.ui.quickfix + +//import org.eclipse.xtext.ui.editor.quickfix.Fix +//import org.eclipse.xtext.ui.editor.quickfix.IssueResolutionAcceptor +//import org.eclipse.xtext.validation.Issue + +/** + * Custom quickfixes. + * + * see http://www.eclipse.org/Xtext/documentation.html#quickfixes + */ +class AlloyLanguageQuickfixProvider extends org.eclipse.xtext.ui.editor.quickfix.DefaultQuickfixProvider { + +// @Fix(MyDslValidator::INVALID_NAME) +// def capitalizeName(Issue issue, IssueResolutionAcceptor acceptor) { +// acceptor.accept(issue, 'Capitalize name', 'Capitalize the name.', 'upcase.png') [ +// context | +// val xtextDocument = context.xtextDocument +// val firstLetter = xtextDocument.get(issue.offset, 1) +// xtextDocument.replace(issue.offset, 1, firstLetter.toUpperCase) +// ] +// } +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.classpath b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.classpath new file mode 100644 index 00000000..5c568755 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.classpath @@ -0,0 +1,9 @@ + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.gitignore b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.gitignore new file mode 100644 index 00000000..8ae4e44d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.gitignore @@ -0,0 +1,4 @@ +/bin/ +/src-gen/ +/vql-gen/ +/xtend-gen/ diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch new file mode 100644 index 00000000..77031bf1 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.launch/Generate Language Infrastructure (hu.bme.mit.inf.dslreasoner.alloy.language).launch @@ -0,0 +1,18 @@ + + + + + + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.project b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.project new file mode 100644 index 00000000..d33a2394 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.project @@ -0,0 +1,34 @@ + + + hu.bme.mit.inf.dslreasoner.alloy.language + + + + + + org.eclipse.jdt.core.javabuilder + + + + + org.eclipse.pde.ManifestBuilder + + + + + org.eclipse.pde.SchemaBuilder + + + + + org.eclipse.xtext.ui.shared.xtextBuilder + + + + + + org.eclipse.jdt.core.javanature + org.eclipse.pde.PluginNature + org.eclipse.xtext.ui.shared.xtextNature + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.core.resources.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.core.resources.prefs new file mode 100644 index 00000000..4824b802 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.core.resources.prefs @@ -0,0 +1,2 @@ +eclipse.preferences.version=1 +encoding/=UTF-8 diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.jdt.core.prefs b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.jdt.core.prefs new file mode 100644 index 00000000..ace45cee --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/.settings/org.eclipse.jdt.core.prefs @@ -0,0 +1,12 @@ +eclipse.preferences.version=1 +org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled +org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate +org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8 +org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve +org.eclipse.jdt.core.compiler.compliance=1.8 +org.eclipse.jdt.core.compiler.debug.lineNumber=generate +org.eclipse.jdt.core.compiler.debug.localVariable=generate +org.eclipse.jdt.core.compiler.debug.sourceFile=generate +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-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/META-INF/MANIFEST.MF b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/META-INF/MANIFEST.MF new file mode 100644 index 00000000..1de8b744 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/META-INF/MANIFEST.MF @@ -0,0 +1,37 @@ +Manifest-Version: 1.0 +Bundle-ManifestVersion: 2 +Bundle-Name: hu.bme.mit.inf.dslreasoner.alloy.language +Bundle-Vendor: My Company +Bundle-Version: 1.0.0.qualifier +Bundle-SymbolicName: hu.bme.mit.inf.dslreasoner.alloy.language; singleton:=true +Bundle-ActivationPolicy: lazy +Require-Bundle: org.eclipse.xtext;visibility:=reexport, + org.eclipse.xtext.xbase;resolution:=optional;visibility:=reexport, + org.eclipse.xtext.generator;resolution:=optional, + org.apache.commons.logging;bundle-version="1.0.4";resolution:=optional, + org.eclipse.emf.codegen.ecore;resolution:=optional, + org.eclipse.emf.mwe.utils;resolution:=optional, + org.eclipse.emf.mwe2.launch;resolution:=optional, + org.eclipse.xtext.util, + org.eclipse.emf.ecore, + org.eclipse.emf.common, + org.eclipse.xtext.xbase.lib, + org.antlr.runtime, + org.eclipse.xtext.common.types, + org.objectweb.asm;bundle-version="[5.0.1,6.0.0)";resolution:=optional, + org.eclipse.equinox.common;bundle-version="3.7.0" +Import-Package: org.apache.log4j +Bundle-RequiredExecutionEnvironment: JavaSE-1.7 +Export-Package: hu.bme.mit.inf.dslreasoner, + hu.bme.mit.inf.dslreasoner.services, + hu.bme.mit.inf.dslreasoner.alloyLanguage, + hu.bme.mit.inf.dslreasoner.alloyLanguage.impl, + hu.bme.mit.inf.dslreasoner.alloyLanguage.util, + hu.bme.mit.inf.dslreasoner.serializer, + hu.bme.mit.inf.dslreasoner.parser.antlr, + hu.bme.mit.inf.dslreasoner.parser.antlr.internal, + hu.bme.mit.inf.dslreasoner.validation, + hu.bme.mit.inf.dslreasoner.scoping, + hu.bme.mit.inf.dslreasoner.generator, + hu.bme.mit.inf.dslreasoner.formatting + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/build.properties b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/build.properties new file mode 100644 index 00000000..07a42688 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/build.properties @@ -0,0 +1,7 @@ +source.. = src/,\ + src-gen/,\ + xtend-gen/ +bin.includes = model/,\ + META-INF/,\ + .,\ + plugin.xml \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.ecore b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.ecore new file mode 100644 index 00000000..a825966e --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.ecore @@ -0,0 +1,267 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.genmodel b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.genmodel new file mode 100644 index 00000000..dd1d46d2 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/model/generated/AlloyLanguage.genmodel @@ -0,0 +1,206 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml new file mode 100644 index 00000000..7567279d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml @@ -0,0 +1,16 @@ + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml_gen b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml_gen new file mode 100644 index 00000000..7567279d --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/plugin.xml_gen @@ -0,0 +1,16 @@ + + + + + + + + + + + + + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext new file mode 100644 index 00000000..6d5fcf58 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext @@ -0,0 +1,149 @@ +grammar hu.bme.mit.inf.dslreasoner.AlloyLanguage with org.eclipse.xtext.common.Terminals + +generate alloyLanguage "http://www.bme.hu/mit/inf/dslreasoner/AlloyLanguage" + +ALSDocument: + ( enumDeclarations += ALSEnumDeclaration | + signatureBodies += ALSSignatureBody | + functionDefinitions += ALSFunctionDefinition | + relationDefinitions += ALSRelationDefinition | + factDeclarations += ALSFactDeclaration)+ + runCommand = ALSRunCommand +; + +////////////////////////////////// +// ALS terminals +////////////////////////////////// + +terminal ID: ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|"'"|'"'|'0'..'9')*; +ALSID: ID; + +enum ALSMultiplicity: all | no | some | lone | one | set; + + +////////////////////////////////// +// ALS types +////////////////////////////////// + +ALSRelationDeclaration: ALSTypeDeclaration | ALSEnumLiteral | ALSFieldDeclaration | ALSVariableDeclaration; + +ALSTypeDeclaration: + ALSEnumDeclaration | ALSSignatureDeclaration +; + +ALSEnumDeclaration: + 'enum' name=ALSID '{' + literal+=ALSEnumLiteral ("," literal+=ALSEnumLiteral)* + '}'; +ALSEnumLiteral: name = ALSID; + +ALSSignatureDeclaration: name = ALSID; + +ALSSignatureBody: + ((multiplicity = ALSMultiplicity?) & (abstract ?= 'abstract')?) + 'sig' + declarations += ALSSignatureDeclaration (',' declarations += ALSSignatureDeclaration)* + (('extends' supertype = [ALSSignatureDeclaration]) + | + ('in' superset += [ALSSignatureDeclaration] ('+' superset += [ALSSignatureDeclaration])*) )? + '{' (fields+=ALSFieldDeclaration ("," fields+=ALSFieldDeclaration)*)? '}' +; + +ALSFieldDeclaration: + name = ALSID ':' (multiplicity = ALSMultiplicity)? type = ALSTerm +; + +ALSDefinition : ALSFunctionDefinition | ALSRelationDefinition; + +ALSFunctionDefinition: + "fun" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" ":" type = ALSTerm + "{" value = ALSTerm "}" +; +ALSRelationDefinition: + "pred" name = ALSID "[" variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* "]" + "{" value = ALSTerm "}" +; + +ALSFactDeclaration: {ALSFactDeclaration} 'fact' (name=ALSID)? '{' (term = ALSTerm) '}' ; + +////////////////////////////////// +// ALS terms +////////////////////////////////// +ALSTerm: ALSQuantified; + +ALSQuantified returns ALSTerm: ({ALSQuantifiedEx} type = ALSMultiplicity + (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}') | ALSOr; + +ALSOr returns ALSTerm: ALSIff ({ALSOr.leftOperand = current} ( "||" | "or" ) rightOperand = ALSIff)?; +ALSIff returns ALSTerm: ALSImpl ({ALSIff.leftOperand = current} ("<=>" | "iff") rightOperand = ALSImpl)?; +ALSImpl returns ALSTerm: ALSAnd ({ALSImpl.leftOperand = current} ("=>" | "implies") rightOperand = ALSAnd ('else' elseOperand = ALSAnd)?)?; +ALSAnd returns ALSTerm: ALSComparison ({ALSAnd.leftOperand = current} ( "&&" | "and" ) rightOperand = ALSComparison)?; + +ALSComparison returns ALSTerm: + ALSOverride + (({ALSEquals.leftOperand = current} "=" | + {ALSNotEquals.leftOperand = current} "!=" | + {ALSSubset.leftOperand = current} "in" | + {ALSLess.leftOperand = current} ">" | + {ALSLeq.leftOperand = current} ">=" | + {ALSMore.leftOperand = current} "<" | + {ALSMeq.leftOperand = current} "<=") + rightOperand = ALSOverride)?; + +ALSOverride returns ALSTerm: ALSRangeRestrictionRight ({ALSOverride.leftOperand = current} '++' rightOperand = ALSRangeRestrictionRight)?; + +ALSRangeRestrictionRight returns ALSTerm: ALSRangeRestrictionLeft ({ALSRangeRestrictionRight.relation = current} ':>' filter = ALSRangeRestrictionLeft)?; +ALSRangeRestrictionLeft returns ALSTerm: ALSJoin ({ALSRangeRestrictionLeft.filter = current} '<:' relation = ALSJoin)?; +ALSJoin returns ALSTerm: ALSMinus ({ALSJoin.leftOperand = current} '.' rightOperand = ALSMinus )*; + +ALSMinus returns ALSTerm: ALSPlus ({ALSMinus.leftOperand = current} '-' rightOperand = ALSPlus)*; +ALSPlus returns ALSTerm: ALSIntersection ({ALSPlus.leftOperand = current} '+' rightOperand = ALSIntersection)*; +ALSIntersection returns ALSTerm: ALSDirectProduct ({ALSIntersection.leftOperand = current} '&' rightOperand = ALSDirectProduct)*; +//ALSMultiply returns ALSTerm: ALSDirectProduct ({ALSMultiply.leftOperand = current} '*' rightOperand = ALSDirectProduct)*; + +ALSDirectProduct returns ALSTerm: + ALSPreficed + ({ALSDirectProduct.leftOperand = current} (leftMultiplicit = ALSMultiplicity)? + '->' + (rightMultiplicit = ALSMultiplicity)? + rightOperand = ALSPreficed)? +; + +ALSPreficed returns ALSTerm: + {ALSNot}=>("!"|'not') operand = ALSBasicRelationTerm | + {ALSInverseRelation}=>"~" operand = ALSBasicRelationTerm | + {AlSTransitiveClosure} "^" operand = ALSBasicRelationTerm | + {ALSReflectiveTransitiveClosure} "*" operand = ALSBasicRelationTerm | + {ALSCardinality} '#' operand = ALSBasicRelationTerm | + {ALSUnaryMinus} =>'-' operand = ALSBasicRelationTerm | + {ALSSum} 'sum' variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | +// {ALSQuantifiedEx} type = ALSMultiplicity +// (disj?='disj')? variables+=ALSVariableDeclaration (',' variables+=ALSVariableDeclaration)* '{' expression = ALSTerm '}' | + {ALSFunctionCall} (referredDefinition=[ALSDefinition]|referredNumericOperator=ALSNumericOperator) '['params+=ALSTerm (',' params+=ALSTerm)*']' | + ALSBasicRelationTerm; + +enum ALSNumericOperator: plus|sub|mul|rem|div; + +//ALSVariable: name = ALSID; +ALSVariableDeclaration: name=ALSID ':' range = ALSTerm; + +ALSBasicRelationTerm returns ALSTerm: + {ALSNone} 'none'| + {ALSIden} 'iden'| + {ALSUniv} 'univ'| + {ALSInt} 'Int' | + {ALSReference} referred = [ALSRelationDeclaration] | + {ALSNumberLiteral} value = INT| + '(' ALSTerm ')' +; + +////////////////////////////////// +// ALS Commands and scopes +////////////////////////////////// +ALSRunCommand: + {ALSRunCommand} 'run' '{' '}' ('for' typeScopes+=ALSTypeScope (',' typeScopes+=ALSTypeScope)*)?; + +ALSTypeScope: ALSSigScope | ALSIntScope; + +ALSSigScope: (exactly?='exactly')? number = INT type = [ALSSignatureDeclaration]; +ALSIntScope: number = INT 'Int'; \ No newline at end of file diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java new file mode 100644 index 00000000..b78c88c2 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageRuntimeModule.java @@ -0,0 +1,11 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner; + +/** + * Use this class to register components to be used at runtime / without the Equinox extension registry. + */ +public class AlloyLanguageRuntimeModule extends hu.bme.mit.inf.dslreasoner.AbstractAlloyLanguageRuntimeModule { + +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java new file mode 100644 index 00000000..bb1447eb --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/AlloyLanguageStandaloneSetup.java @@ -0,0 +1,16 @@ +/* +* generated by Xtext +*/ +package hu.bme.mit.inf.dslreasoner; + +/** + * Initialization support for running Xtext languages + * without equinox extension registry + */ +public class AlloyLanguageStandaloneSetup extends AlloyLanguageStandaloneSetupGenerated{ + + public static void doSetup() { + new AlloyLanguageStandaloneSetup().createInjectorAndDoEMFRegistration(); + } +} + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 new file mode 100644 index 00000000..fa57e2de --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/GenerateAlloyLanguage.mwe2 @@ -0,0 +1,133 @@ +module hu.bme.mit.inf.dslreasoner.GenerateAlloyLanguage + +import org.eclipse.emf.mwe.utils.* +import org.eclipse.xtext.generator.* +import org.eclipse.xtext.ui.generator.* + +var grammarURI = "classpath:/hu/bme/mit/inf/dslreasoner/AlloyLanguage.xtext" +var fileExtensions = "als" +var projectName = "hu.bme.mit.inf.dslreasoner.alloy.language" +var runtimeProject = "../${projectName}" +var generateXtendStub = true +var encoding = "UTF-8" + +Workflow { + bean = StandaloneSetup { + scanClassPath = true + platformUri = "${runtimeProject}/.." + // The following two lines can be removed, if Xbase is not used. + registerGeneratedEPackage = "org.eclipse.xtext.xbase.XbasePackage" + registerGenModelFile = "platform:/resource/org.eclipse.xtext.xbase/model/Xbase.genmodel" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/src-gen" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}/model/generated" + } + + component = DirectoryCleaner { + directory = "${runtimeProject}.ui/src-gen" + } + +// component = DirectoryCleaner { +// directory = "${runtimeProject}.tests/src-gen" +// } + + component = Generator { + pathRtProject = runtimeProject + pathUiProject = "${runtimeProject}.ui" + //pathTestProject = "${runtimeProject}.tests" + projectNameRt = projectName + projectNameUi = "${projectName}.ui" + encoding = encoding + language = auto-inject { + uri = grammarURI + + // Java API to access grammar elements (required by several other fragments) + fragment = grammarAccess.GrammarAccessFragment auto-inject {} + + // generates Java API for the generated EPackages + fragment = ecore.EMFGeneratorFragment auto-inject {} + + // the old serialization component + // fragment = parseTreeConstructor.ParseTreeConstructorFragment auto-inject {} + + // serializer 2.0 + fragment = serializer.SerializerFragment auto-inject { + generateStub = false + } + + // a custom ResourceFactory for use with EMF + fragment = resourceFactory.ResourceFactoryFragment auto-inject {} + + // The antlr parser generator fragment. + fragment = parser.antlr.XtextAntlrGeneratorFragment auto-inject { + // options = { + // backtrack = true + // } + } + + // Xtend-based API for validation + fragment = validation.ValidatorFragment auto-inject { + // composedCheck = "org.eclipse.xtext.validation.ImportUriValidator" + // composedCheck = "org.eclipse.xtext.validation.NamesAreUniqueValidator" + } + + // old scoping and exporting API + // fragment = scoping.ImportURIScopingFragment auto-inject {} + // fragment = exporting.SimpleNamesFragment auto-inject {} + + // scoping and exporting API + fragment = scoping.ImportNamespacesScopingFragment auto-inject {} + fragment = exporting.QualifiedNamesFragment auto-inject {} + fragment = builder.BuilderIntegrationFragment auto-inject {} + + // generator API + fragment = generator.GeneratorFragment auto-inject {} + + // formatter API + fragment = formatting.FormatterFragment auto-inject {} + + // labeling API + fragment = labeling.LabelProviderFragment auto-inject {} + + // outline API + fragment = outline.OutlineTreeProviderFragment auto-inject {} + fragment = outline.QuickOutlineFragment auto-inject {} + + // quickfix API + fragment = quickfix.QuickfixProviderFragment auto-inject {} + + // content assist API + fragment = contentAssist.ContentAssistFragment auto-inject {} + + // generates a more lightweight Antlr parser and lexer tailored for content assist + fragment = parser.antlr.XtextAntlrUiGeneratorFragment auto-inject {} + + // generates junit test support classes into Generator#pathTestProject + fragment = junit.Junit4Fragment auto-inject {} + + // rename refactoring + fragment = refactoring.RefactorElementNameFragment auto-inject {} + + // provides the necessary bindings for java types integration + fragment = types.TypesGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xbase + fragment = xbase.XbaseGeneratorFragment auto-inject {} + + // generates the required bindings only if the grammar inherits from Xtype + fragment = xbase.XtypeGeneratorFragment auto-inject {} + + // provides a preference page for template proposals + fragment = templates.CodetemplatesGeneratorFragment auto-inject {} + + // provides a compare view + fragment = compare.CompareFragment auto-inject {} + } + } +} + diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend new file mode 100644 index 00000000..28797bc4 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/formatting/AlloyLanguageFormatter.xtend @@ -0,0 +1,96 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.formatting + +import com.google.inject.Inject +import hu.bme.mit.inf.dslreasoner.services.AlloyLanguageGrammarAccess +import org.eclipse.xtext.formatting.impl.AbstractDeclarativeFormatter +import org.eclipse.xtext.formatting.impl.FormattingConfig + +/** + * This class contains custom formatting description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#formatting + * on how and when to use it + * + * Also see {@link org.eclipse.xtext.xtext.XtextFormattingTokenSerializer} as an example + */ +class AlloyLanguageFormatter extends AbstractDeclarativeFormatter { + + @Inject extension AlloyLanguageGrammarAccess + + override protected void configureFormatting(FormattingConfig c) { + // It's usually a good idea to activate the following three statements. + // They will add and preserve newlines around comments + c.setLinewrap(0, 1, 2).before(SL_COMMENTRule) + c.setLinewrap(0, 1, 2).before(ML_COMMENTRule) + c.setLinewrap(0, 1, 1).after(ML_COMMENTRule) + + c.setAutoLinewrap(100000); + + //Signatures + c.setIndentationIncrement.after(ALSSignatureBodyAccess.leftCurlyBracketKeyword_5); + c.setLinewrap.after(ALSSignatureBodyAccess.leftCurlyBracketKeyword_5) + c.setIndentationDecrement.before(ALSSignatureBodyAccess.rightCurlyBracketKeyword_7); + c.setLinewrap.after(ALSSignatureBodyAccess.rightCurlyBracketKeyword_7) + c.setLinewrap.before(ALSSignatureBodyAccess.rightCurlyBracketKeyword_7) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_3_0) + c.setLinewrap.after(ALSSignatureBodyAccess.commaKeyword_3_0) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_3_0) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_6_1_0) + c.setLinewrap.after(ALSSignatureBodyAccess.commaKeyword_6_1_0) + c.setNoSpace.before(ALSSignatureBodyAccess.commaKeyword_6_1_0) + //c.setLinewrap(0,1,2).between(ALSSignatureDeclarationRule,ALSSignatureDeclarationRule) + + //Enums + c.setIndentationIncrement.after(ALSEnumDeclarationAccess.leftCurlyBracketKeyword_2) + c.setLinewrap.after(ALSEnumDeclarationAccess.leftCurlyBracketKeyword_2) + c.setIndentationDecrement.before(ALSEnumDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.before(ALSEnumDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.after(ALSEnumDeclarationAccess.rightCurlyBracketKeyword_5) + c.setNoSpace.before(ALSEnumDeclarationAccess.commaKeyword_4_0) + + + //facts + c.setIndentationIncrement.after(ALSFactDeclarationAccess.leftCurlyBracketKeyword_3) + c.setLinewrap.after(ALSFactDeclarationAccess.leftCurlyBracketKeyword_3) + c.setIndentationDecrement.before(ALSFactDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.before(ALSFactDeclarationAccess.rightCurlyBracketKeyword_5) + c.setLinewrap.after(ALSFactDeclarationAccess.rightCurlyBracketKeyword_5) + + //predicates + c.setIndentationIncrement.after(ALSRelationDefinitionAccess.leftCurlyBracketKeyword_6) + c.setLinewrap.after(ALSRelationDefinitionAccess.leftCurlyBracketKeyword_6) + c.setIndentationDecrement.before(ALSRelationDefinitionAccess.rightCurlyBracketKeyword_8) + c.setLinewrap.before(ALSRelationDefinitionAccess.rightCurlyBracketKeyword_8) + c.setLinewrap.after(ALSRelationDefinitionAccess.rightCurlyBracketKeyword_8) + c.setNoSpace.after(ALSRelationDefinitionAccess.leftSquareBracketKeyword_2) + c.setNoSpace.before(ALSRelationDefinitionAccess.rightSquareBracketKeyword_5) + c.setNoSpace.before(ALSRelationDefinitionAccess.commaKeyword_4_0) + + // terms + //c.setNoSpace.before(ALSJoinAccess.rightSquareBracketKeyword_1_2_1_3) + c.setNoSpace.before(ALSJoinAccess.fullStopKeyword_1_1) + c.setNoSpace.after(ALSJoinAccess.fullStopKeyword_1_1) + + c.setNoSpace.before(ALSDirectProductAccess.hyphenMinusGreaterThanSignKeyword_1_2) + c.setNoSpace.after(ALSDirectProductAccess.hyphenMinusGreaterThanSignKeyword_1_2) + + c.setNoSpace.before(ALSVariableDeclarationAccess.colonKeyword_1) +// c.setNoSpace.before(ALSPreficedAccess.commaKeyword_5_3_0) +// c.setNoSpace.before(ALSPreficedAccess.commaKeyword_6_4_0) +// +// c.setIndentationIncrement.after(ALSPreficedAccess.leftCurlyBracketKeyword_5_4) +// c.setLinewrap.after(ALSPreficedAccess.leftCurlyBracketKeyword_5_4) +// c.setLinewrap.before(ALSPreficedAccess.rightCurlyBracketKeyword_5_6) +// c.setIndentationDecrement.before(ALSPreficedAccess.rightCurlyBracketKeyword_5_6) + + c.setNoSpace.after(ALSBasicRelationTermAccess.leftParenthesisKeyword_6_0) + c.setNoSpace.before(ALSBasicRelationTermAccess.rightParenthesisKeyword_6_2) + + // Quantified expression + c.setNoSpace.before(ALSQuantifiedAccess.commaKeyword_0_4_0) + + } +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend new file mode 100644 index 00000000..9afcc300 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/generator/AlloyLanguageGenerator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.generator + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.xtext.generator.IGenerator +import org.eclipse.xtext.generator.IFileSystemAccess + +/** + * Generates code from your model files on save. + * + * see http://www.eclipse.org/Xtext/documentation.html#TutorialCodeGeneration + */ +class AlloyLanguageGenerator implements IGenerator { + + override void doGenerate(Resource resource, IFileSystemAccess fsa) { +// fsa.generateFile('greetings.txt', 'People to greet: ' + +// resource.allContents +// .filter(typeof(Greeting)) +// .map[name] +// .join(', ')) + } +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend new file mode 100644 index 00000000..6e095f3c --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/scoping/AlloyLanguageScopeProvider.xtend @@ -0,0 +1,81 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.scoping + +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDefinition +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSFunctionCall +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSQuantifiedEx +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSReference +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDeclaration +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSRelationDefinition +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody +import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSum +import java.util.ArrayList +import java.util.Collections +import java.util.HashSet +import java.util.LinkedList +import java.util.List +import java.util.Set +import org.eclipse.emf.ecore.EObject +import org.eclipse.emf.ecore.EReference +import org.eclipse.xtext.scoping.IScope +import org.eclipse.xtext.scoping.Scopes +import org.eclipse.xtext.scoping.impl.AbstractDeclarativeScopeProvider + +/** + * This class contains custom scoping description. + * + * see : http://www.eclipse.org/Xtext/documentation.html#scoping + * on how and when to use it + * + */ +class AlloyLanguageScopeProvider extends AbstractDeclarativeScopeProvider { + + def public IScope scope_ALSReference_referred(ALSReference alsReferecnce, EReference ref) { + val Set declarations = new HashSet + + val parent = alsReferecnce.getAllParents(ALSDocument).head as ALSDocument + val signatures = parent.signatureBodies.map[ALSSignatureBody x|x.declarations].flatten + declarations+=parent.enumDeclarations + declarations+=signatures + declarations+=parent.enumDeclarations.map[ALSEnumDeclaration x | x.literal].flatten + declarations+=parent.signatureBodies.map[ALSSignatureBody x|x.fields].flatten + + declarations+=alsReferecnce.getAllParents(ALSQuantifiedEx).map[ALSQuantifiedEx x | x.variables].flatten + declarations+=alsReferecnce.getAllParents(ALSSum).map[ALSSum x | x.variables].flatten + declarations+=alsReferecnce.getAllParents(ALSRelationDefinition).map[ALSRelationDefinition x | x.variables].flatten + +// println("---") +// println(declarations.map[it.name].join(", ")) + + return Scopes.scopeFor(declarations) + } + //{ALSFunctionCall} (/*functionName=ALSID |*/ referredDefinition=[ALSDefinition]) + def public IScope scope_ALSFunctionCall_referredDefinition(ALSFunctionCall call, EReference ref) { + val parent = call.getAllParents(ALSDocument).head as ALSDocument + val list = new LinkedList + list += parent.relationDefinitions + list += parent.functionDefinitions + //list.forEach[println(it.name + " " + it.eContainer)] + return Scopes.scopeFor(list) + } + + def List getAllParents(EObject object, Class type) { + if(object.eContainer == null) { + return Collections.EMPTY_LIST + } else { + val container = object.eContainer; + val previousParents = container.getAllParents(type) + if(type.isInstance(container)){ + val res = new ArrayList(previousParents) + res+= container as X + return res + } + else return previousParents + + } + } +} diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend new file mode 100644 index 00000000..8e1efc99 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dslreasoner.alloy.language/src/hu/bme/mit/inf/dslreasoner/validation/AlloyLanguageValidator.xtend @@ -0,0 +1,24 @@ +/* + * generated by Xtext + */ +package hu.bme.mit.inf.dslreasoner.validation +//import org.eclipse.xtext.validation.Check + +/** + * Custom validation rules. + * + * see http://www.eclipse.org/Xtext/documentation.html#validation + */ +class AlloyLanguageValidator extends AbstractAlloyLanguageValidator { + +// public static val INVALID_NAME = 'invalidName' +// +// @Check +// def checkGreetingStartsWithCapital(Greeting greeting) { +// if (!Character.isUpperCase(greeting.name.charAt(0))) { +// warning('Name should start with a capital', +// MyDslPackage.Literals.GREETING__NAME, +// INVALID_NAME) +// } +// } +} -- cgit v1.2.3-70-g09d2