diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test')
20 files changed, 409 insertions, 343 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF index 2ea274a4..9e50006e 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF | |||
@@ -1,11 +1,21 @@ | |||
1 | Manifest-Version: 1.0 | 1 | Manifest-Version: 1.0 |
2 | Bundle-ManifestVersion: 2 | 2 | Bundle-ManifestVersion: 2 |
3 | Bundle-Name: Test | 3 | Bundle-Name: %pluginName |
4 | Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true | 4 | Bundle-SymbolicName: ca.mcgill.ecse.dslreasoner.vampire.test;singleton:=true |
5 | Bundle-Version: 1.0.0.qualifier | 5 | Bundle-Version: 1.0.0.qualifier |
6 | Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries | 6 | Bundle-ClassPath: . |
7 | Bundle-Vendor: %providerName | ||
8 | Bundle-Localization: plugin | ||
9 | Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries, | ||
10 | yakindumm, | ||
11 | yakindumm.impl, | ||
12 | yakindumm.util, | ||
13 | yakindumm.yakindumm, | ||
14 | yakindumm.yakindumm.impl, | ||
15 | yakindumm.yakindumm.util | ||
7 | Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, | 16 | Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, |
8 | org.eclipse.emf.ecore, | 17 | org.eclipse.core.runtime, |
18 | org.eclipse.emf.ecore;visibility:=reexport, | ||
9 | org.eclipse.viatra.query.runtime.rete, | 19 | org.eclipse.viatra.query.runtime.rete, |
10 | org.eclipse.viatra.query.runtime.localsearch, | 20 | org.eclipse.viatra.query.runtime.localsearch, |
11 | com.google.guava, | 21 | com.google.guava, |
@@ -32,6 +42,7 @@ Require-Bundle: org.eclipse.viatra.addon.querybasedfeatures.runtime, | |||
32 | org.eclipse.collections;bundle-version="9.2.0", | 42 | org.eclipse.collections;bundle-version="9.2.0", |
33 | hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", | 43 | hu.bme.mit.inf.dslreasoner.application.FAMTest;bundle-version="1.0.0", |
34 | ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0" | 44 | ca.mcgill.ecse.dslreasoner.standalone.test;bundle-version="1.0.0" |
35 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | ||
36 | Import-Package: org.apache.log4j | 45 | Import-Package: org.apache.log4j |
37 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test | 46 | Automatic-Module-Name: ca.mcgill.ecse.dslreasoner.vampire.test |
47 | Bundle-ActivationPolicy: lazy | ||
48 | Bundle-RequiredExecutionEnvironment: JavaSE-1.8 | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/Yakindu.xmi index 49b1f89d..49b1f89d 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/Yakindu.xmi +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/Yakindu.xmi | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore deleted file mode 100644 index 0c944db8..00000000 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/initialModels/yakindu/yakindu.ecore +++ /dev/null | |||
@@ -1,26 +0,0 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?> | ||
2 | <ecore:EPackage xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="yakindu" nsURI="YakinduMetamodel" nsPrefix="yakindu"> | ||
3 | <eClassifiers xsi:type="ecore:EClass" name="Pseudostate" abstract="true" eSuperTypes="//Vertex"/> | ||
4 | <eClassifiers xsi:type="ecore:EClass" name="Vertex" abstract="true"> | ||
5 | <eStructuralFeatures xsi:type="ecore:EReference" name="incomingTransitions" ordered="false" upperBound="-1" eType="//Transition" eOpposite="//Transition/target"/> | ||
6 | <eStructuralFeatures xsi:type="ecore:EReference" name="outgoingTransitions" ordered="false" upperBound="-1" eType="//Transition" containment="true" eOpposite="//Transition/source"/> | ||
7 | </eClassifiers> | ||
8 | <eClassifiers xsi:type="ecore:EClass" name="Region"> | ||
9 | <eStructuralFeatures xsi:type="ecore:EReference" name="vertices" ordered="false" upperBound="-1" eType="//Vertex" containment="true"/> | ||
10 | </eClassifiers> | ||
11 | <eClassifiers xsi:type="ecore:EClass" name="Transition"> | ||
12 | <eStructuralFeatures xsi:type="ecore:EReference" name="target" ordered="false" lowerBound="1" eType="//Vertex" eOpposite="//Vertex/incomingTransitions"/> | ||
13 | <eStructuralFeatures xsi:type="ecore:EReference" name="source" ordered="false" eType="//Vertex" eOpposite="//Vertex/outgoingTransitions"/> | ||
14 | </eClassifiers> | ||
15 | <eClassifiers xsi:type="ecore:EClass" name="Statechart" eSuperTypes="//CompositeElement"/> | ||
16 | <eClassifiers xsi:type="ecore:EClass" name="Entry" eSuperTypes="//Pseudostate"/> | ||
17 | <eClassifiers xsi:type="ecore:EClass" name="Synchronization" eSuperTypes="//Pseudostate"/> | ||
18 | <eClassifiers xsi:type="ecore:EClass" name="State" eSuperTypes="//RegularState //CompositeElement"/> | ||
19 | <eClassifiers xsi:type="ecore:EClass" name="RegularState" abstract="true" eSuperTypes="//Vertex"/> | ||
20 | <eClassifiers xsi:type="ecore:EClass" name="CompositeElement" abstract="true"> | ||
21 | <eStructuralFeatures xsi:type="ecore:EReference" name="regions" upperBound="-1" eType="//Region" containment="true"/> | ||
22 | </eClassifiers> | ||
23 | <eClassifiers xsi:type="ecore:EClass" name="Choice" eSuperTypes="//Pseudostate"/> | ||
24 | <eClassifiers xsi:type="ecore:EClass" name="Exit" eSuperTypes="//Pseudostate"/> | ||
25 | <eClassifiers xsi:type="ecore:EClass" name="FinalState" eSuperTypes="//RegularState"/> | ||
26 | </ecore:EPackage> | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem index 226150e8..f86a2f3c 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | |||
@@ -1,5 +1,5 @@ | |||
1 | <?xml version="1.0" encoding="ASCII"?> | 1 | <?xml version="1.0" encoding="ASCII"?> |
2 | <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" xmlns:viatra2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/viatra2logicannotation"> | 2 | <language:LogicProblem xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:ecore2logicannotations="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language/ecore2logicannotation" xmlns:language="http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" xmlns:language_1="http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"> |
3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> | 3 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalElement class" subtypes="//@types.2" isAbstract="true"/> |
4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class" subtypes="//@types.10 //@types.11" isAbstract="true"/> | 4 | <types xsi:type="language_1:TypeDeclaration" name="FunctionalArchitectureModel class" subtypes="//@types.10 //@types.11" isAbstract="true"/> |
5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> | 5 | <types xsi:type="language_1:TypeDeclaration" name="Function class" supertypes="//@types.0"/> |
@@ -496,22 +496,6 @@ | |||
496 | </expression> | 496 | </expression> |
497 | </value> | 497 | </value> |
498 | </assertions> | 498 | </assertions> |
499 | <assertions name="errorpattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.24"> | ||
500 | <value xsi:type="language_1:Forall"> | ||
501 | <quantifiedVariables name="p0"> | ||
502 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
503 | </quantifiedVariables> | ||
504 | <quantifiedVariables name="p1"> | ||
505 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
506 | </quantifiedVariables> | ||
507 | <expression xsi:type="language_1:Not"> | ||
508 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17"> | ||
509 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/> | ||
510 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/> | ||
511 | </operand> | ||
512 | </expression> | ||
513 | </value> | ||
514 | </assertions> | ||
515 | <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement"> | 499 | <relations xsi:type="language_1:RelationDeclaration" name="interface reference FunctionalElement"> |
516 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | 500 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> |
517 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/> | 501 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.5"/> |
@@ -572,197 +556,6 @@ | |||
572 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | 556 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
573 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | 557 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> |
574 | </relations> | 558 | </relations> |
575 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam rootElements" annotations="//@annotations.19"> | ||
576 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
577 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
578 | <variables name="parameter Model"> | ||
579 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
580 | </variables> | ||
581 | <variables name="parameter Root"> | ||
582 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
583 | </variables> | ||
584 | <value xsi:type="language_1:Or"> | ||
585 | <operands xsi:type="language_1:And"> | ||
586 | <operands xsi:type="language_1:InstanceOf"> | ||
587 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
588 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
589 | </operands> | ||
590 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.3"> | ||
591 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
592 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
593 | </operands> | ||
594 | </operands> | ||
595 | </value> | ||
596 | </relations> | ||
597 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam model" annotations="//@annotations.20"> | ||
598 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
599 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
600 | <variables name="parameter This"> | ||
601 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
602 | </variables> | ||
603 | <variables name="parameter Target"> | ||
604 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
605 | </variables> | ||
606 | <value xsi:type="language_1:Or"> | ||
607 | <operands xsi:type="language_1:And"> | ||
608 | <operands xsi:type="language_1:InstanceOf"> | ||
609 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/> | ||
610 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
611 | </operands> | ||
612 | <operands xsi:type="language_1:InstanceOf"> | ||
613 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.1"/> | ||
614 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
615 | </operands> | ||
616 | </operands> | ||
617 | </value> | ||
618 | </relations> | ||
619 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.21"> | ||
620 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
621 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
622 | <variables name="parameter T"> | ||
623 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | ||
624 | </variables> | ||
625 | <variables name="parameter I"> | ||
626 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | ||
627 | </variables> | ||
628 | <value xsi:type="language_1:Or"> | ||
629 | <operands xsi:type="language_1:Exists"> | ||
630 | <quantifiedVariables name="variable Out"> | ||
631 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.7"/> | ||
632 | </quantifiedVariables> | ||
633 | <expression xsi:type="language_1:And"> | ||
634 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> | ||
635 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/> | ||
636 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.1"/> | ||
637 | </operands> | ||
638 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
639 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/> | ||
640 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> | ||
641 | </operands> | ||
642 | </expression> | ||
643 | </operands> | ||
644 | <operands xsi:type="language_1:Exists"> | ||
645 | <quantifiedVariables name="variable In"> | ||
646 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/> | ||
647 | </quantifiedVariables> | ||
648 | <expression xsi:type="language_1:And"> | ||
649 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> | ||
650 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.1"/> | ||
651 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.1/@quantifiedVariables.0"/> | ||
652 | </operands> | ||
653 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
654 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.1/@quantifiedVariables.0"/> | ||
655 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> | ||
656 | </operands> | ||
657 | </expression> | ||
658 | </operands> | ||
659 | </value> | ||
660 | </relations> | ||
661 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam parent" annotations="//@annotations.22"> | ||
662 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
663 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
664 | <variables name="parameter Func"> | ||
665 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
666 | </variables> | ||
667 | <variables name="parameter Par"> | ||
668 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
669 | </variables> | ||
670 | <value xsi:type="language_1:Or"> | ||
671 | <operands xsi:type="language_1:And"> | ||
672 | <operands xsi:type="language_1:InstanceOf"> | ||
673 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/> | ||
674 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
675 | </operands> | ||
676 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.2"> | ||
677 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/> | ||
678 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/> | ||
679 | </operands> | ||
680 | <operands xsi:type="language_1:InstanceOf"> | ||
681 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/> | ||
682 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
683 | </operands> | ||
684 | </operands> | ||
685 | </value> | ||
686 | </relations> | ||
687 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam type" annotations="//@annotations.23"> | ||
688 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
689 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
690 | <variables name="parameter This"> | ||
691 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
692 | </variables> | ||
693 | <variables name="parameter Target"> | ||
694 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
695 | </variables> | ||
696 | <value xsi:type="language_1:Or"> | ||
697 | <operands xsi:type="language_1:Exists"> | ||
698 | <quantifiedVariables name="variable Model"> | ||
699 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
700 | </quantifiedVariables> | ||
701 | <expression xsi:type="language_1:And"> | ||
702 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
703 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.0/@quantifiedVariables.0"/> | ||
704 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
705 | </operands> | ||
706 | <operands xsi:type="language_1:Equals"> | ||
707 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
708 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.0"/> | ||
709 | </operands> | ||
710 | </expression> | ||
711 | </operands> | ||
712 | <operands xsi:type="language_1:Forall"> | ||
713 | <quantifiedVariables name="variable Child"> | ||
714 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
715 | </quantifiedVariables> | ||
716 | <quantifiedVariables name="variable Model"> | ||
717 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
718 | </quantifiedVariables> | ||
719 | <expression xsi:type="language_1:And"> | ||
720 | <operands xsi:type="language_1:InstanceOf"> | ||
721 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
722 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
723 | </operands> | ||
724 | <operands xsi:type="language_1:Not"> | ||
725 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> | ||
726 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.1/@quantifiedVariables.0"/> | ||
727 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
728 | </operand> | ||
729 | </operands> | ||
730 | <operands xsi:type="language_1:Not"> | ||
731 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
732 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.1/@quantifiedVariables.1"/> | ||
733 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
734 | </operand> | ||
735 | </operands> | ||
736 | <operands xsi:type="language_1:Equals"> | ||
737 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
738 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.2"/> | ||
739 | </operands> | ||
740 | </expression> | ||
741 | </operands> | ||
742 | <operands xsi:type="language_1:Exists"> | ||
743 | <quantifiedVariables name="variable Par"> | ||
744 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
745 | </quantifiedVariables> | ||
746 | <quantifiedVariables name="variable Child"> | ||
747 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
748 | </quantifiedVariables> | ||
749 | <expression xsi:type="language_1:And"> | ||
750 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> | ||
751 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
752 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.2/@quantifiedVariables.0"/> | ||
753 | </operands> | ||
754 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> | ||
755 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.2/@quantifiedVariables.1"/> | ||
756 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
757 | </operands> | ||
758 | <operands xsi:type="language_1:Equals"> | ||
759 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
760 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.1"/> | ||
761 | </operands> | ||
762 | </expression> | ||
763 | </operands> | ||
764 | </value> | ||
765 | </relations> | ||
766 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> | 559 | <elements name="Root literal FunctionType" definedInType="//@types.9"/> |
767 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> | 560 | <elements name="Intermediate literal FunctionType" definedInType="//@types.9"/> |
768 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> | 561 | <elements name="Leaf literal FunctionType" definedInType="//@types.9"/> |
@@ -787,10 +580,4 @@ | |||
787 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> | 580 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> |
788 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> | 581 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> |
789 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> | 582 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> |
790 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.rootElements"/> | ||
791 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.16" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/> | ||
792 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.17" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/> | ||
793 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.18" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.parent"/> | ||
794 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.19" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/> | ||
795 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.21"/> | ||
796 | </language:LogicProblem> | 583 | </language:LogicProblem> |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.properties b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.properties new file mode 100644 index 00000000..6021c31d --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.properties | |||
@@ -0,0 +1,4 @@ | |||
1 | # | ||
2 | |||
3 | pluginName = Test | ||
4 | providerName = www.example.org | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml index b0735f37..6a9aee5e 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml | |||
@@ -1,10 +1,15 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?><plugin> | 1 | <?xml version="1.0" encoding="UTF-8"?><plugin> |
2 | <extension point="org.eclipse.emf.ecore.generated_package"> | ||
3 | <!-- @generated yakindu_simplified --> | ||
4 | <package class="yakindumm.YakindummPackage" genModel="initialModels/yakindu/yakindu_simplified.genmodel" uri="hu.bme.mit.inf.yakindumm"/> | ||
5 | </extension> | ||
6 | <extension point="org.eclipse.emf.ecore.generated_package"> | ||
7 | <!-- @generated yakindu_simplified --> | ||
8 | <package class="yakindumm.yakindumm.YakindummPackage" genModel="initialModels/yakindu/yakindu_simplified.genmodel" uri="hu.bme.mit.inf.yakindumm"/> | ||
9 | </extension> | ||
2 | <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" point="org.eclipse.viatra.query.runtime.queryspecification"> | 10 | <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" point="org.eclipse.viatra.query.runtime.queryspecification"> |
3 | <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns"> | 11 | <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns"> |
4 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/> | 12 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/> |
5 | </group> | 13 | </group> |
6 | </extension> | 14 | </extension> |
7 | <extension id="extension.derived.ca.mcgill.ecse.dslreasoner.vampire.queries.live" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features"> | ||
8 | <wellbehaving-derived-feature classifier-name="FileSystem" feature-name="live" package-nsUri="FileSystemMetamodel"/> | ||
9 | </extension> | ||
10 | </plugin> | 15 | </plugin> |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend index 70ded02d..35b76350 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend | |||
@@ -50,7 +50,7 @@ class EcoreTest { | |||
50 | it.documentationLevel = DocumentationLevel::FULL | 50 | it.documentationLevel = DocumentationLevel::FULL |
51 | ] | 51 | ] |
52 | 52 | ||
53 | solution = reasoner.solve(logicProblem, vampireConfig, workspace, "ECO") | 53 | solution = reasoner.solve(logicProblem, vampireConfig, workspace) |
54 | 54 | ||
55 | println("Problem solved") | 55 | println("Problem solved") |
56 | 56 | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend index 5143641b..a7da818c 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend | |||
@@ -2,12 +2,13 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse | |||
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
5 | import functionalarchitecture.FAMTerminator | ||
5 | import functionalarchitecture.Function | 6 | import functionalarchitecture.Function |
6 | import functionalarchitecture.FunctionalArchitectureModel | 7 | import functionalarchitecture.FunctionalArchitectureModel |
7 | import functionalarchitecture.FunctionalInterface | 8 | import functionalarchitecture.FunctionalInterface |
8 | import functionalarchitecture.FunctionalOutput | 9 | import functionalarchitecture.FunctionalOutput |
9 | import functionalarchitecture.FunctionalarchitecturePackage | 10 | import functionalarchitecture.FunctionalarchitecturePackage |
10 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns | 11 | //import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns |
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
@@ -22,7 +23,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | |||
22 | import java.util.HashMap | 23 | import java.util.HashMap |
23 | import org.eclipse.emf.ecore.resource.Resource | 24 | import org.eclipse.emf.ecore.resource.Resource |
24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 25 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
25 | import functionalarchitecture.FAMTerminator | ||
26 | 26 | ||
27 | class FAMTest { | 27 | class FAMTest { |
28 | def static void main(String[] args) { | 28 | def static void main(String[] args) { |
@@ -47,15 +47,15 @@ class FAMTest { | |||
47 | // Load DSL | 47 | // Load DSL |
48 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) | 48 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) |
49 | val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") | 49 | val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") |
50 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | 50 | // val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) |
51 | // val queries = null | 51 | val queries = null |
52 | 52 | ||
53 | println("DSL loaded") | 53 | println("DSL loaded") |
54 | 54 | ||
55 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | 55 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) |
56 | var problem = modelGenerationProblem.output | 56 | var problem = modelGenerationProblem.output |
57 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | 57 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output |
58 | problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | 58 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output |
59 | workspace.writeModel(problem, "Fam.logicproblem") | 59 | workspace.writeModel(problem, "Fam.logicproblem") |
60 | 60 | ||
61 | println("Problem created") | 61 | println("Problem created") |
@@ -94,14 +94,15 @@ class FAMTest { | |||
94 | 94 | ||
95 | it.typeScopes.minNewElements = 8//24 | 95 | it.typeScopes.minNewElements = 8//24 |
96 | it.typeScopes.maxNewElements = 10//25 | 96 | it.typeScopes.maxNewElements = 10//25 |
97 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 97 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
98 | // if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 98 | // if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
99 | it.contCycleLevel = 5 | 99 | it.contCycleLevel = 5 |
100 | it.uniquenessDuplicates = false | 100 | it.uniquenessDuplicates = false |
101 | ] | 101 | ] |
102 | 102 | ||
103 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) | 103 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) |
104 | 104 | ||
105 | println("Problem solved") | ||
105 | // visualisation, see | 106 | // visualisation, see |
106 | var interpretations = reasoner.getInterpretations(solution as ModelResult) | 107 | var interpretations = reasoner.getInterpretations(solution as ModelResult) |
107 | // interpretations.get(0) as VampireModelInterpretation | 108 | // interpretations.get(0) as VampireModelInterpretation |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index fb1bdb59..057bcf12 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | |||
@@ -1,25 +1,27 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage | 3 | import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
7 | import functionalarchitecture.FunctionalarchitecturePackage | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | ||
11 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
12 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | 15 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic |
13 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 16 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
14 | import java.util.HashMap | 17 | import java.io.PrintWriter |
15 | import org.eclipse.emf.ecore.resource.Resource | 18 | import org.eclipse.emf.ecore.resource.Resource |
16 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
17 | 20 | ||
18 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.* | ||
19 | |||
20 | class YakinduTest { | 21 | class YakinduTest { |
21 | def static void main(String[] args) { | 22 | def static void main(String[] args) { |
22 | val Ecore2Logic ecore2Logic = new Ecore2Logic | 23 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
24 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | ||
23 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | 25 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) |
24 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | 26 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic |
25 | 27 | ||
@@ -35,76 +37,166 @@ class YakinduTest { | |||
35 | 37 | ||
36 | println("Input and output workspaces are created") | 38 | println("Input and output workspaces are created") |
37 | 39 | ||
38 | val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE) | 40 | // val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE) |
39 | val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi") | 41 | val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) |
40 | // val queries = GeneralTest.loadQueries(metamodel, yakinduPatterns.instance) | 42 | // val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi") |
41 | val queries = null | 43 | val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") |
42 | 44 | // val queries = GeneralTest.loadQueries(metamodel, YakinduPatterns.instance) | |
45 | val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) | ||
46 | // val queries = null | ||
43 | println("DSL loaded") | 47 | println("DSL loaded") |
44 | 48 | ||
45 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | 49 | var MAX = 150 |
46 | var problem = modelGenerationProblem.output | 50 | var START = 10 |
47 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | 51 | var INC = 20 |
52 | var REPS = 1 | ||
53 | |||
54 | val EXACT = -1 | ||
55 | if (EXACT!= -1) { | ||
56 | MAX = EXACT | ||
57 | START = EXACT | ||
58 | INC = 1 | ||
59 | REPS = 5 | ||
60 | } | ||
61 | |||
62 | var writer = new PrintWriter(workspace.workspaceURI + "//yakinduStats.csv") | ||
63 | writer.append("size,") | ||
64 | for (var x = 0; x < REPS; x++) { | ||
65 | writer.append("t" + x + ",") | ||
66 | } | ||
67 | writer.append("avg\n") | ||
68 | var totalTime = 0.0 | ||
69 | var totFound = 0.0 | ||
70 | var modelFound = true | ||
71 | var LogicResult solution = null | ||
72 | for (var i = START; i <= MAX; i += INC) { | ||
73 | val num = (i - START) / INC | ||
74 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") | ||
75 | writer.append(i + ",") | ||
76 | totalTime = 0.0 | ||
77 | totFound = 0.0 | ||
78 | modelFound = true | ||
79 | for (var j = 0; j < REPS; j++) { | ||
80 | |||
81 | print(j) | ||
82 | |||
83 | val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) | ||
84 | var problem = modelGenerationProblem.output | ||
85 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output | ||
48 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output | 86 | // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output |
49 | workspace.writeModel(problem, "Yakindu.logicproblem") | 87 | workspace.writeModel(problem, "Yakindu.logicproblem") |
50 | 88 | ||
51 | println("Problem created") | 89 | // println("Problem created") |
52 | 90 | // Start Time | |
53 | // Start Time | 91 | var startTime = System.currentTimeMillis |
54 | var startTime = System.currentTimeMillis | 92 | |
55 | 93 | var VampireSolver reasoner | |
56 | var VampireSolver reasoner | 94 | // * |
57 | // * | 95 | reasoner = new VampireSolver |
58 | reasoner = new VampireSolver | 96 | |
59 | 97 | // ///////////////////////////////////////////////////// | |
60 | // ///////////////////////////////////////////////////// | 98 | // Minimum Scope |
61 | // Minimum Scope | 99 | // val classMapMin = new HashMap<Class, Integer> |
62 | val classMapMin = new HashMap<Class, Integer> | 100 | // classMapMin.put(Region, 1) |
63 | classMapMin.put(Region, 1) | 101 | // classMapMin.put(Transition, 2) |
64 | classMapMin.put(Transition, 2) | 102 | // classMapMin.put(CompositeElement, 3) |
65 | classMapMin.put(CompositeElement, 3) | 103 | // val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
66 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 104 | // Maximum Scope |
67 | 105 | // val classMapMax = new HashMap<Class, Integer> | |
68 | // Maximum Scope | 106 | // classMapMax.put(Region, 5) |
69 | val classMapMax = new HashMap<Class, Integer> | 107 | // classMapMax.put(Transition, 2) |
70 | classMapMax.put(Region, 5) | 108 | // classMapMax.put(Synchronization, 4) |
71 | classMapMax.put(Transition, 2) | 109 | // val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
72 | classMapMax.put(Synchronization, 4) | 110 | // Define Config File |
73 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | 111 | val size = i |
74 | 112 | val inc = INC | |
75 | // Define Config File | 113 | val vampireConfig = new VampireSolverConfiguration => [ |
76 | val vampireConfig = new VampireSolverConfiguration => [ | 114 | // add configuration things, in config file first |
77 | // add configuration things, in config file first | 115 | it.documentationLevel = DocumentationLevel::FULL |
78 | it.documentationLevel = DocumentationLevel::FULL | 116 | |
79 | 117 | it.typeScopes.minNewElements = size - inc | |
80 | it.typeScopes.minNewElements = 20 | 118 | it.typeScopes.maxNewElements = size |
81 | it.typeScopes.maxNewElements = 30 | 119 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
82 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 120 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
83 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 121 | it.contCycleLevel = 5 |
84 | it.contCycleLevel = 5 | 122 | it.uniquenessDuplicates = false |
85 | it.uniquenessDuplicates = false | 123 | ] |
86 | ] | 124 | |
87 | 125 | solution = reasoner.solve(problem, vampireConfig, workspace) | |
88 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "YAK") | 126 | // print((solution as ModelResult).representation.get(0)) |
89 | 127 | val soln = ((solution as ModelResult).representation.get(0) as VampireModel) | |
90 | /*/ | 128 | // println(soln.confirmations) |
91 | * | 129 | // println((solution as ModelResult).representation) |
92 | * reasoner = new AlloySolver | 130 | // modelFound = !soln.confirmations.filter [ |
93 | * val alloyConfig = new AlloySolverConfiguration => [ | 131 | // class == VLSFiniteModelImpl |
94 | * it.typeScopes.maxNewElements = 7 | 132 | // ].isEmpty |
95 | * it.typeScopes.minNewElements = 3 | 133 | // |
96 | * it.solutionScope.numberOfRequiredSolution = 1 | 134 | // if (modelFound) { |
97 | * it.typeScopes.maxNewIntegers = 0 | 135 | val time = solution.statistics.transformationTime / 1000.0 |
98 | * it.documentationLevel = DocumentationLevel::NORMAL | 136 | writer.append(time + ",") |
99 | * ] | 137 | print("(" + time + ")..") |
100 | * solution = reasoner.solve(problem, alloyConfig, workspace) | 138 | totalTime += time |
101 | //*/ | 139 | totFound += 1 |
102 | // ///////////////////////////////////////////////////// | 140 | // } else { |
103 | var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | 141 | // writer.append("MNF" + ",") |
104 | var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | 142 | //// print("MNF") |
105 | 143 | // } | |
106 | println("Problem solved") | 144 | // println("Problem solved") |
107 | println("Time was: " + totalTimeMin + ":" + totalTimeSec) | 145 | // visualisation, see |
146 | // var interpretations = reasoner.getInterpretations(solution as ModelResult) | ||
147 | /* interpretations.get(0) as VampireModelInterpretation | ||
148 | * println(ecore2Logic.IsAttributeValue(modelGenerationProblem.trace, ) | ||
149 | * Literal(modelGenerationProblem.trace, ecore2Logic.allLiteralsInScope(modelGenerationProblem.trace).get(0) ) | ||
150 | * ) | ||
151 | * println((ecore2Logic.allAttributesInScope(modelGenerationProblem.trace)).get(0).EAttributeType) | ||
152 | print(interpretations.class)*/ | ||
153 | // for (interpretation : interpretations) { | ||
154 | // val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) | ||
155 | // workspace.writeModel(model, "model.xmi") | ||
156 | /* val representation = im2pi.transform(modelGenerationProblem, model.eAllContents.toList, false)//solution.representation.get(0) // TODO: fix for multiple represenations | ||
157 | * if (representation instanceof PartialInterpretation) { | ||
158 | * val vis1 = new PartialInterpretation2Gml | ||
159 | * val gml = vis1.transform(representation) | ||
160 | * workspace.writeText("model.gml", gml) | ||
161 | |||
162 | * val vis2 = new GraphvizVisualiser | ||
163 | * val dot = vis2.visualiseConcretization(representation) | ||
164 | * dot.writeToFile(workspace, "model.png") | ||
165 | * } else { | ||
166 | * println("ERROR") | ||
167 | * } | ||
168 | look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor*/ | ||
169 | // } | ||
170 | /*/ | ||
171 | * | ||
172 | * reasoner = new AlloySolver | ||
173 | * val alloyConfig = new AlloySolverConfiguration => [ | ||
174 | * it.typeScopes.maxNewElements = 7 | ||
175 | * it.typeScopes.minNewElements = 3 | ||
176 | * it.solutionScope.numberOfRequiredSolution = 1 | ||
177 | * it.typeScopes.maxNewIntegers = 0 | ||
178 | * it.documentationLevel = DocumentationLevel::NORMAL | ||
179 | * ] | ||
180 | * solution = reasoner.solve(problem, alloyConfig, workspace) | ||
181 | //*/ | ||
182 | // ///////////////////////////////////////////////////// | ||
183 | // var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | ||
184 | // var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | ||
185 | // println("Problem solved") | ||
186 | // println("Time was: " + totalTimeMin + ":" + totalTimeSec) | ||
187 | } | ||
188 | println() | ||
189 | var avg = 0.0 | ||
190 | if (totFound == 0) { | ||
191 | avg = -1 | ||
192 | } else { | ||
193 | avg = totalTime / totFound | ||
194 | } | ||
195 | writer.append(avg.toString) | ||
196 | writer.append("\n") | ||
197 | } | ||
198 | writer.close | ||
199 | |||
108 | } | 200 | } |
109 | 201 | ||
110 | } | 202 | } |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index a30b7cfc..4880c751 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin index a818eb7e..8ad6dfed 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin index b913bd4b..164e6c2f 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index 4a9e17e1..46cad7ee 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin index 3dcefc79..eeb7c77a 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java index 01503783..7019f162 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.java | |||
@@ -1,9 +1,68 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
7 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | ||
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | ||
17 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | ||
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; | ||
19 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | ||
20 | import org.eclipse.emf.common.util.EList; | ||
21 | import org.eclipse.emf.ecore.EObject; | ||
22 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
23 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
24 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
25 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
26 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
27 | |||
3 | @SuppressWarnings("all") | 28 | @SuppressWarnings("all") |
4 | public class EcoreTest { | 29 | public class EcoreTest { |
5 | public static void main(final String[] args) { | 30 | public static void main(final String[] args) { |
6 | throw new Error("Unresolved compilation problems:" | 31 | try { |
7 | + "\nInvalid number of arguments. The method solve(LogicProblem, LogicSolverConfiguration, ReasonerWorkspace) is not applicable for the arguments (LogicProblem,VampireSolverConfiguration,FileSystemWorkspace,String)"); | 32 | StringConcatenation _builder = new StringConcatenation(); |
33 | _builder.append("initialModels/"); | ||
34 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); | ||
35 | StringConcatenation _builder_1 = new StringConcatenation(); | ||
36 | _builder_1.append("output/FEcoreTest/"); | ||
37 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); | ||
38 | workspace.initAndClear(); | ||
39 | InputOutput.<String>println("Input and output workspaces are created"); | ||
40 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(filesystemPackage.eINSTANCE); | ||
41 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "fs/filesystemInstance.xmi"); | ||
42 | final Object queries = null; | ||
43 | InputOutput.<String>println("DSL loaded"); | ||
44 | final Ecore2Logic ecore2Logic = new Ecore2Logic(); | ||
45 | final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); | ||
46 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); | ||
47 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | ||
48 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | ||
49 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | ||
50 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); | ||
51 | final LogicProblem logicProblem = modelGenerationProblem.getOutput(); | ||
52 | InputOutput.<String>println("Problem created"); | ||
53 | LogicResult solution = null; | ||
54 | LogicReasoner reasoner = null; | ||
55 | VampireSolver _vampireSolver = new VampireSolver(); | ||
56 | reasoner = _vampireSolver; | ||
57 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | ||
58 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | ||
59 | it.documentationLevel = DocumentationLevel.FULL; | ||
60 | }; | ||
61 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | ||
62 | solution = reasoner.solve(logicProblem, vampireConfig, workspace); | ||
63 | InputOutput.<String>println("Problem solved"); | ||
64 | } catch (Throwable _e) { | ||
65 | throw Exceptions.sneakyThrow(_e); | ||
66 | } | ||
8 | } | 67 | } |
9 | } | 68 | } |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java index 26252d6c..8cd08fd8 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java | |||
@@ -8,7 +8,6 @@ import functionalarchitecture.Function; | |||
8 | import functionalarchitecture.FunctionalArchitectureModel; | 8 | import functionalarchitecture.FunctionalArchitectureModel; |
9 | import functionalarchitecture.FunctionalOutput; | 9 | import functionalarchitecture.FunctionalOutput; |
10 | import functionalarchitecture.FunctionalarchitecturePackage; | 10 | import functionalarchitecture.FunctionalarchitecturePackage; |
11 | import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns; | ||
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; |
13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | 12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; |
14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | 13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; |
@@ -22,8 +21,6 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | |||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
23 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 22 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
24 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 23 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
25 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; | ||
26 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; | ||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; | 24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; |
28 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2PartialInterpretation; | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2PartialInterpretation; |
29 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | 26 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; |
@@ -63,14 +60,12 @@ public class FAMTest { | |||
63 | InputOutput.<String>println("Input and output workspaces are created"); | 60 | InputOutput.<String>println("Input and output workspaces are created"); |
64 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); | 61 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); |
65 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi"); | 62 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi"); |
66 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); | 63 | final Object queries = null; |
67 | InputOutput.<String>println("DSL loaded"); | 64 | InputOutput.<String>println("DSL loaded"); |
68 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | 65 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); |
69 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | 66 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); |
70 | LogicProblem problem = modelGenerationProblem.getOutput(); | 67 | LogicProblem problem = modelGenerationProblem.getOutput(); |
71 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); | 68 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); |
72 | Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); | ||
73 | problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, _viatra2LogicConfiguration).getOutput(); | ||
74 | workspace.writeModel(problem, "Fam.logicproblem"); | 69 | workspace.writeModel(problem, "Fam.logicproblem"); |
75 | InputOutput.<String>println("Problem created"); | 70 | InputOutput.<String>println("Problem created"); |
76 | long startTime = System.currentTimeMillis(); | 71 | long startTime = System.currentTimeMillis(); |
@@ -91,16 +86,12 @@ public class FAMTest { | |||
91 | it.documentationLevel = DocumentationLevel.FULL; | 86 | it.documentationLevel = DocumentationLevel.FULL; |
92 | it.typeScopes.minNewElements = 8; | 87 | it.typeScopes.minNewElements = 8; |
93 | it.typeScopes.maxNewElements = 10; | 88 | it.typeScopes.maxNewElements = 10; |
94 | int _size = typeMapMin.size(); | ||
95 | boolean _notEquals = (_size != 0); | ||
96 | if (_notEquals) { | ||
97 | it.typeScopes.minNewElementsByType = typeMapMin; | ||
98 | } | ||
99 | it.contCycleLevel = 5; | 89 | it.contCycleLevel = 5; |
100 | it.uniquenessDuplicates = false; | 90 | it.uniquenessDuplicates = false; |
101 | }; | 91 | }; |
102 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | 92 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); |
103 | LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); | 93 | LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); |
94 | InputOutput.<String>println("Problem solved"); | ||
104 | List<? extends LogicModelInterpretation> interpretations = reasoner.getInterpretations(((ModelResult) solution)); | 95 | List<? extends LogicModelInterpretation> interpretations = reasoner.getInterpretations(((ModelResult) solution)); |
105 | InputOutput.<Class<? extends List>>print(interpretations.getClass()); | 96 | InputOutput.<Class<? extends List>>print(interpretations.getClass()); |
106 | for (final LogicModelInterpretation interpretation : interpretations) { | 97 | for (final LogicModelInterpretation interpretation : interpretations) { |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java index f8502439..616868a6 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java | |||
@@ -1,10 +1,152 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | ||
8 | import functionalarchitecture.FunctionalarchitecturePackage; | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | ||
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | ||
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | ||
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.EcoreMetamodelDescriptor; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | ||
19 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | ||
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; | ||
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; | ||
22 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | ||
23 | import java.io.PrintWriter; | ||
24 | import java.util.Map; | ||
25 | import org.eclipse.emf.common.util.EList; | ||
26 | import org.eclipse.emf.common.util.URI; | ||
27 | import org.eclipse.emf.ecore.EObject; | ||
28 | import org.eclipse.emf.ecore.resource.Resource; | ||
29 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | ||
30 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
31 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
32 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
33 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
34 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
35 | |||
3 | @SuppressWarnings("all") | 36 | @SuppressWarnings("all") |
4 | public class YakinduTest { | 37 | public class YakinduTest { |
5 | public static void main(final String[] args) { | 38 | public static void main(final String[] args) { |
6 | throw new Error("Unresolved compilation problems:" | 39 | try { |
7 | + "\nThe method or field yakinduPackage is undefined" | 40 | final Ecore2Logic ecore2Logic = new Ecore2Logic(); |
8 | + "\neINSTANCE cannot be resolved"); | 41 | final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); |
42 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); | ||
43 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | ||
44 | StringConcatenation _builder = new StringConcatenation(); | ||
45 | _builder.append("initialModels/"); | ||
46 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); | ||
47 | StringConcatenation _builder_1 = new StringConcatenation(); | ||
48 | _builder_1.append("output/YakinduTest/"); | ||
49 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); | ||
50 | workspace.initAndClear(); | ||
51 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; | ||
52 | final Map<String, Object> map = reg.getExtensionToFactoryMap(); | ||
53 | XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); | ||
54 | map.put("logicproblem", _xMIResourceFactoryImpl); | ||
55 | InputOutput.<String>println("Input and output workspaces are created"); | ||
56 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); | ||
57 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi"); | ||
58 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); | ||
59 | InputOutput.<String>println("DSL loaded"); | ||
60 | int MAX = 150; | ||
61 | int START = 10; | ||
62 | int INC = 20; | ||
63 | int REPS = 1; | ||
64 | final int EXACT = (-1); | ||
65 | if ((EXACT != (-1))) { | ||
66 | MAX = EXACT; | ||
67 | START = EXACT; | ||
68 | INC = 1; | ||
69 | REPS = 5; | ||
70 | } | ||
71 | URI _workspaceURI = workspace.getWorkspaceURI(); | ||
72 | String _plus = (_workspaceURI + "//yakinduStats.csv"); | ||
73 | PrintWriter writer = new PrintWriter(_plus); | ||
74 | writer.append("size,"); | ||
75 | for (int x = 0; (x < REPS); x++) { | ||
76 | writer.append((("t" + Integer.valueOf(x)) + ",")); | ||
77 | } | ||
78 | writer.append("avg\n"); | ||
79 | double totalTime = 0.0; | ||
80 | double totFound = 0.0; | ||
81 | boolean modelFound = true; | ||
82 | LogicResult solution = null; | ||
83 | { | ||
84 | int i = START; | ||
85 | boolean _while = (i <= MAX); | ||
86 | while (_while) { | ||
87 | { | ||
88 | final int num = ((i - START) / INC); | ||
89 | InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); | ||
90 | String _plus_1 = (Integer.valueOf(i) + ","); | ||
91 | writer.append(_plus_1); | ||
92 | totalTime = 0.0; | ||
93 | totFound = 0.0; | ||
94 | modelFound = true; | ||
95 | for (int j = 0; (j < REPS); j++) { | ||
96 | { | ||
97 | InputOutput.<Integer>print(Integer.valueOf(j)); | ||
98 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | ||
99 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | ||
100 | LogicProblem problem = modelGenerationProblem.getOutput(); | ||
101 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); | ||
102 | workspace.writeModel(problem, "Yakindu.logicproblem"); | ||
103 | long startTime = System.currentTimeMillis(); | ||
104 | VampireSolver reasoner = null; | ||
105 | VampireSolver _vampireSolver = new VampireSolver(); | ||
106 | reasoner = _vampireSolver; | ||
107 | final int size = i; | ||
108 | final int inc = INC; | ||
109 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | ||
110 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | ||
111 | it.documentationLevel = DocumentationLevel.FULL; | ||
112 | it.typeScopes.minNewElements = (size - inc); | ||
113 | it.typeScopes.maxNewElements = size; | ||
114 | it.contCycleLevel = 5; | ||
115 | it.uniquenessDuplicates = false; | ||
116 | }; | ||
117 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | ||
118 | solution = reasoner.solve(problem, vampireConfig, workspace); | ||
119 | Object _get = ((ModelResult) solution).getRepresentation().get(0); | ||
120 | final VampireModel soln = ((VampireModel) _get); | ||
121 | int _transformationTime = solution.getStatistics().getTransformationTime(); | ||
122 | final double time = (_transformationTime / 1000.0); | ||
123 | String _plus_2 = (Double.valueOf(time) + ","); | ||
124 | writer.append(_plus_2); | ||
125 | InputOutput.<String>print((("(" + Double.valueOf(time)) + ")..")); | ||
126 | double _talTime = totalTime; | ||
127 | totalTime = (_talTime + time); | ||
128 | double _tFound = totFound; | ||
129 | totFound = (_tFound + 1); | ||
130 | } | ||
131 | } | ||
132 | InputOutput.println(); | ||
133 | double avg = 0.0; | ||
134 | if ((totFound == 0)) { | ||
135 | avg = (-1); | ||
136 | } else { | ||
137 | avg = (totalTime / totFound); | ||
138 | } | ||
139 | writer.append(Double.valueOf(avg).toString()); | ||
140 | writer.append("\n"); | ||
141 | } | ||
142 | int _i = i; | ||
143 | i = (_i + INC); | ||
144 | _while = (i <= MAX); | ||
145 | } | ||
146 | } | ||
147 | writer.close(); | ||
148 | } catch (Throwable _e) { | ||
149 | throw Exceptions.sneakyThrow(_e); | ||
150 | } | ||
9 | } | 151 | } |
10 | } | 152 | } |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index 4fb4dbc3..e9a1a8db 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin index 0eacff72..39d9c161 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index 2c32163b..effd204e 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin | |||
Binary files differ | |||