Skip to content
Snippets Groups Projects
Commit 90d26251 authored by Sebastian Krings's avatar Sebastian Krings
Browse files

integration commit between camille 2 and 3, merging the multiple lines of... 

integration commit between camille 2 and 3, merging the multiple lines of development (git + svn), includes rodin 3 port

Sadly, it was not possible to generate separate commits out of this as these did not exist in the former repositories
parent 60237533
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 72 additions and 815 deletions
org.eventb.texteditor.ui/.settings/org.eclipse.jdt.core.prefs deleted 100644 → 0
+ 0
− 7
View file @ 60237533
#Thu Mar 26 12:38:05 CET 2009
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5
org.eclipse.jdt.core.compiler.compliance=1.5
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.source=1.5
org.eventb.texteditor.ui/META-INF/MANIFEST.MF
+ 4
− 5
View file @ 90d26251
......@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: Camille Texteditor
Bundle-SymbolicName: org.eventb.texteditor.ui;singleton:=true
Bundle-Version: 3.0.0.qualifier
Bundle-Version: 3.0.1.qualifier
Bundle-Localization: plugin
Bundle-Activator: org.eventb.texteditor.ui.TextEditorPlugin$Implementation
Require-Bundle: org.eventb.texttools;bundle-version="[2.0.0,3.1.0)";visibility:=reexport,
......@@ -14,7 +14,8 @@ Require-Bundle: org.eventb.texttools;bundle-version="[2.0.0,3.1.0)";visibility:=
org.eventb.core.ast;bundle-version="[3.0.0,4.0.0)",
org.eclipse.ui.editors;bundle-version="[3.8.0,4.0.0)",
org.eclipse.ui.ide;bundle-version="[3.8.2,4.0.0)",
org.rodinp.keyboard.ui;bundle-version="[2.0.0,3.0.0)"
org.rodinp.keyboard.ui;bundle-version="[2.0.0,3.0.0)",
org.eclipse.ui.workbench.texteditor
Bundle-ActivationPolicy: lazy
Bundle-RequiredExecutionEnvironment: J2SE-1.5
Bundle-ClassPath: lib/commons-lang-2.4.jar,
......@@ -22,6 +23,4 @@ Bundle-ClassPath: lib/commons-lang-2.4.jar,
Bundle-Vendor: Heinrich-Heine University Dusseldorf
Export-Package: org.eventb.texteditor.ui,
org.eventb.texteditor.ui.editor
Import-Package: org.eclipse.emf.edit.ui.util,
org.eclipse.ui.texteditor.link,
org.eclipse.ui.texteditor.templates
Import-Package: org.eclipse.ui.texteditor.link
org.eventb.texteditor.ui/pom.xml 0 → 100644
+ 19
− 0
View file @ 90d26251
<?xml version="1.0" encoding="UTF-8"?>
<project
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd" xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<modelVersion>4.0.0</modelVersion>
<parent>
<groupId>org.eventb.texteditor</groupId>
<artifactId>org.eventb.texteditor.parent</artifactId>
<version>1.0.0.qualifier</version>
<relativePath>../org.eventb.texteditor.parent/pom.xml</relativePath>
</parent>
<groupId>org.eventb.texteditor</groupId>
<artifactId>org.eventb.texteditor.ui</artifactId>
<version>3.0.1.qualifier</version>
<packaging>eclipse-plugin</packaging>
</project>
\ No newline at end of file
org.eventb.texttools.test/.project deleted 100644 → 0
+ 0
− 28
View file @ 60237533
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.eventb.texttools.test</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.ManifestBuilder</name>
<arguments>
</arguments>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.SchemaBuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.pde.PluginNature</nature>
<nature>org.eclipse.jdt.core.javanature</nature>
</natures>
</projectDescription>
org.eventb.texttools.test/META-INF/MANIFEST.MF deleted 100644 → 0
+ 0
− 8
View file @ 60237533
Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: Test Fragment
Bundle-SymbolicName: org.eventb.texttools.test
Bundle-Version: 1.0.0
Fragment-Host: org.eventb.texttools;bundle-version="0.0.1"
Bundle-RequiredExecutionEnvironment: J2SE-1.5
Require-Bundle: org.junit
org.eventb.texttools.test/build.properties deleted 100644 → 0
+ 0
− 4
View file @ 60237533
source.. = src/
output.. = bin/
bin.includes = META-INF/,\
.
org.eventb.texttools.test/src/org/eventb/texttools/AllTestsSuite.java deleted 100644 → 0
+ 0
− 56
View file @ 60237533
package org.eventb.texttools;
import java.util.Enumeration;
import junit.framework.TestSuite;
import junit.runner.ClassPathTestCollector;
import junit.runner.TestCollector;
/**
* All tests on the classpath.
*/
public class AllTestsSuite extends TestSuite {
/**
* Returns a TestSuite containing all tests on the classpath.
*
* @return a TestSuite containing all tests on the classpath.
* @throws ClassNotFoundException
*/
@SuppressWarnings("unchecked")
public static TestSuite suite() throws ClassNotFoundException {
final TestSuite suite = new TestSuite();
final Enumeration enumer = collectTestClasses();
while (enumer.hasMoreElements()) {
final Class klass = Class.forName((String) enumer.nextElement());
if (klass != null) {
suite.addTestSuite(klass);
}
}
return suite;
}
/**
* Returns qualified class names of classes on the classpath, whos name ends
* with "Test".
*
* @return qualified class names of classes on the classpath, whos name ends
* with "Test".
*/
@SuppressWarnings("unchecked")
private static Enumeration collectTestClasses() {
final TestCollector collector = new ClassPathTestCollector() {
@Override
public boolean isTestClass(final String classFileName) {
if (classFileName.endsWith("Test.class")) {
return true;
} else {
return false;
}
}
};
return collector.collectTests();
}
}
org.eventb.texttools.test/src/org/eventb/texttools/formulas/ExpressionResolverTest.java deleted 100644 → 0
+ 0
− 22
View file @ 60237533
package org.eventb.texttools.formulas;
import junit.framework.TestCase;
import org.eventb.emf.core.machine.MachineFactory;
import org.eventb.emf.core.machine.Variant;
public class ExpressionResolverTest extends TestCase {
public void testParseError() {
final String input = "x y";
final Variant emfExpr = MachineFactory.eINSTANCE.createVariant();
emfExpr.setExpression(input);
try {
FormulaResolver.resolve(emfExpr);
fail("Expected Exception was not thrown");
} catch (final FormulaParseException e) {
assertEquals(emfExpr, e.getEmfObject());
assertEquals(1, e.getAstProblems().size());
}
}
}
org.eventb.texttools.test/src/org/eventb/texttools/formulas/ResolveVisitorTest.java deleted 100644 → 0
+ 0
− 368
View file @ 60237533
package org.eventb.texttools.formulas;
import junit.framework.TestCase;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.common.util.TreeIterator;
import org.eclipse.emf.ecore.EAnnotation;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eventb.core.ast.Formula;
import org.eventb.emf.core.AbstractExtension;
import org.eventb.emf.core.machine.Action;
import org.eventb.emf.core.machine.Invariant;
import org.eventb.emf.core.machine.MachineFactory;
import org.eventb.emf.core.machine.Variant;
import org.eventb.emf.formulas.AddExpression;
import org.eventb.emf.formulas.AndPredicate;
import org.eventb.emf.formulas.BExpressionResolved;
import org.eventb.emf.formulas.BFormula;
import org.eventb.emf.formulas.BecomesEqualToAssignment;
import org.eventb.emf.formulas.BecomesMemberOfAssignment;
import org.eventb.emf.formulas.BecomesSuchThatAssignment;
import org.eventb.emf.formulas.BoundIdentifierExpression;
import org.eventb.emf.formulas.EqualPredicate;
import org.eventb.emf.formulas.FALSITY;
import org.eventb.emf.formulas.ForallPredicate;
import org.eventb.emf.formulas.IdentifierExpression;
import org.eventb.emf.formulas.IdentityGenExpression;
import org.eventb.emf.formulas.IntegerLiteralExpression;
import org.eventb.emf.formulas.LessPredicate;
import org.eventb.emf.formulas.PartitionPredicate;
import org.eventb.emf.formulas.PredExpression;
import org.eventb.emf.formulas.Prj1GenExpression;
import org.eventb.emf.formulas.QuantifiedUnionExpression1;
import org.eventb.emf.formulas.SetExpression;
import org.eventb.emf.formulas.TRUE;
import org.eventb.emf.formulas.TRUTH;
import org.eventb.texttools.TextPositionUtil;
import org.eventb.texttools.model.texttools.TextRange;
import org.eventb.texttools.model.texttools.TexttoolsFactory;
public class ResolveVisitorTest extends TestCase {
/**
* Tests free_identifier, integer_literal, add_expression
*
* @throws FormulaParseException
*/
public void testAdd() throws FormulaParseException {
final String input = "x+5+y";
final Variant emfExpr = MachineFactory.eINSTANCE.createVariant();
emfExpr.setExpression(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof AddExpression);
final AddExpression addExpr = (AddExpression) extension;
assertEquals(3, addExpr.getChildren().size());
assertTrue(addExpr.getChildren().get(0) instanceof IdentifierExpression);
assertTrue(addExpr.getChildren().get(1) instanceof IntegerLiteralExpression);
}
/**
* Tests free_identifier, EQUAL, TRUE
*
* @throws FormulaParseException
*/
public void testEqual() throws FormulaParseException {
final String input = "x=TRUE";
final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant();
emfExpr.setPredicate(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof EqualPredicate);
final EqualPredicate addExpr = (EqualPredicate) extension;
assertTrue(addExpr.getLeft() instanceof IdentifierExpression);
assertEquals("x", ((IdentifierExpression) addExpr.getLeft()).getName());
assertTrue(addExpr.getRight() instanceof TRUE);
}
/**
* Tests TRUTH, FALSITY and AND
*
* @throws FormulaParseException
*/
public void testAnd() throws FormulaParseException {
final String input = "\u22a4 \u2227 \u22a4 \u2227 \u22a5";
final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant();
emfExpr.setPredicate(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof AndPredicate);
final AndPredicate andPred = (AndPredicate) extension;
assertEquals(3, andPred.getChildren().size());
assertTrue(andPred.getChildren().get(0) instanceof TRUTH);
assertTrue(andPred.getChildren().get(1) instanceof TRUTH);
assertTrue(andPred.getChildren().get(2) instanceof FALSITY);
}
/**
* Tests KPRED
*
* @throws FormulaParseException
*/
public void testPred() throws FormulaParseException {
final String input = "pred";
final Variant emfExpr = MachineFactory.eINSTANCE.createVariant();
emfExpr.setExpression(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof PredExpression);
}
/**
* Tests {@link Formula#KPRJ1_GEN}
*
* @throws FormulaParseException
*/
public void testPrj1Gen() throws FormulaParseException {
final String input = "prj1";
final Variant emfExpr = MachineFactory.eINSTANCE.createVariant();
emfExpr.setExpression(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof Prj1GenExpression);
}
/**
* Tests Tests {@link Formula#KID_GEN}
*
* @throws FormulaParseException
*/
public void testIdentityGen() throws FormulaParseException {
final String input = "id";
final Variant emfExpr = MachineFactory.eINSTANCE.createVariant();
emfExpr.setExpression(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof IdentityGenExpression);
}
/**
* Tests forall predicate with 2 local variables and an equal as predicate
*
* @throws FormulaParseException
*/
public void testForall() throws FormulaParseException {
final String input = "\u2200 x,y \u00b7 x=y";
final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant();
emfExpr.setPredicate(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof ForallPredicate);
final ForallPredicate predicate = (ForallPredicate) extension;
final EList<BoundIdentifierExpression> identifiers = predicate
.getIdentifiers();
assertEquals("x", identifiers.get(0).getName());
assertEquals("y", identifiers.get(1).getName());
assertTrue(predicate.getPredicate() instanceof EqualPredicate);
final EqualPredicate equalPred = (EqualPredicate) predicate
.getPredicate();
assertTrue(equalPred.getLeft() instanceof BoundIdentifierExpression);
assertTrue(equalPred.getRight() instanceof BoundIdentifierExpression);
}
public void testQuantifiedUnion() throws FormulaParseException {
final String input = "\u22c3 x,y \u00b7 \u22a5 \u2223 x";
final Variant emfExpr = MachineFactory.eINSTANCE.createVariant();
emfExpr.setExpression(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof QuantifiedUnionExpression1);
final QuantifiedUnionExpression1 expression = (QuantifiedUnionExpression1) extension;
assertEquals(2, expression.getIdentifiers().size());
assertTrue(expression.getPredicate() instanceof FALSITY);
assertTrue(expression.getExpression() instanceof IdentifierExpression);
}
public void testPartitionExpression() throws FormulaParseException {
final String input = "partition(S, {a}, {b})";
final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant();
emfExpr.setPredicate(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof PartitionPredicate);
final PartitionPredicate predicate = (PartitionPredicate) extension;
final EList<BFormula> children = predicate.getChildren();
assertEquals(3, children.size());
assertTrue(children.get(0) instanceof IdentifierExpression);
assertTrue(children.get(1) instanceof SetExpression);
assertTrue(children.get(2) instanceof SetExpression);
}
public void testBecomesEqual() throws FormulaParseException {
final String input = "x ≔ x + 1";
final Action emfExpr = MachineFactory.eINSTANCE.createAction();
emfExpr.setAction(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof BecomesEqualToAssignment);
final BecomesEqualToAssignment assignment = (BecomesEqualToAssignment) extension;
assertEquals(1, assignment.getIdentifiers().size());
final EList<IdentifierExpression> identifiers = assignment
.getIdentifiers();
assertEquals("x", identifiers.get(0).getName());
assertEquals(1, assignment.getExpressions().size());
final EList<BExpressionResolved> expressions = assignment
.getExpressions();
assertTrue(expressions.get(0) instanceof AddExpression);
}
public void testSuchThat() throws FormulaParseException {
final String input = "x :\u2223 x < x'";
final Action emfExpr = MachineFactory.eINSTANCE.createAction();
emfExpr.setAction(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof BecomesSuchThatAssignment);
final BecomesSuchThatAssignment assignment = (BecomesSuchThatAssignment) extension;
assertEquals(1, assignment.getIdentifiers().size());
final EList<IdentifierExpression> identifiers = assignment
.getIdentifiers();
assertEquals("x", identifiers.get(0).getName());
assertTrue(assignment.getPredicate() instanceof LessPredicate);
final LessPredicate lessPred = (LessPredicate) assignment
.getPredicate();
assertEquals("x", ((IdentifierExpression) lessPred.getLeft()).getName());
assertEquals("x'", ((BoundIdentifierExpression) lessPred.getRight())
.getName());
}
public void testElementOf() throws FormulaParseException {
final String input = "x :\u2208 S";
final Action emfExpr = MachineFactory.eINSTANCE.createAction();
emfExpr.setAction(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
assertTrue(extension instanceof BecomesMemberOfAssignment);
final BecomesMemberOfAssignment assignment = (BecomesMemberOfAssignment) extension;
assertEquals(1, assignment.getIdentifiers().size());
final EList<IdentifierExpression> identifiers = assignment
.getIdentifiers();
assertEquals("x", identifiers.get(0).getName());
assertTrue(assignment.getExpression() instanceof IdentifierExpression);
final IdentifierExpression identExpr = (IdentifierExpression) assignment
.getExpression();
assertEquals("S", identExpr.getName());
}
public void testSourceAnnotations() throws FormulaParseException {
final String input = "\u2200 x,y \u00b7 x=z+5+y";
final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant();
emfExpr.setPredicate(input);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
final TreeIterator<Object> iterator = EcoreUtil.getAllContents(
extension, false);
while (iterator.hasNext()) {
final Object next = iterator.next();
if (next instanceof BFormula) {
final BFormula formula = (BFormula) next;
final EAnnotation annotation = formula
.getEAnnotation(TextPositionUtil.ANNOTATION_TEXTRANGE);
assertNotNull(annotation);
} else if (next instanceof EAnnotation) {
final EAnnotation annotation = (EAnnotation) next;
assertNotNull(annotation.getEModelElement());
assertNotNull(TextPositionUtil.getTextRange(annotation
.getEModelElement()));
} else if (next instanceof TextRange) {
final TextRange range = (TextRange) next;
assertTrue(range.getOffset() + " >= " + 0,
range.getOffset() >= 0);
assertTrue(range.getOffset() + " < " + input.length(), range
.getOffset() < input.length());
assertTrue(range.getLength() + " <= " + input.length(), range
.getLength() <= input.length());
assertTrue(range.getLength() + " > " + input.length(), range
.getLength() > 0);
} else {
System.out.println("Found untested types: "
+ next.getClass().getSimpleName());
}
}
}
public void testSourceOffset() throws FormulaParseException {
final String input = "\u2200 x,y \u00b7 x=z+5+y";
final int offset = 50;
final Invariant emfExpr = MachineFactory.eINSTANCE.createInvariant();
emfExpr.setPredicate(input);
TextPositionUtil.annotatePosition(emfExpr, offset - 10,
input.length() + 10);
final TextRange subRange = TexttoolsFactory.eINSTANCE.createTextRange();
subRange.setOffset(offset);
subRange.setLength(input.length());
TextPositionUtil.addInternalPosition(emfExpr, input, subRange);
FormulaResolver.resolve(emfExpr);
assertEquals(1, emfExpr.getExtensions().size());
final AbstractExtension extension = emfExpr.getExtensions().get(0);
final TreeIterator<EObject> iterator = EcoreUtil.getAllContents(
extension, false);
while (iterator.hasNext()) {
final EObject next = iterator.next();
if (next instanceof BFormula) {
// test: every element has a position annotation
final BFormula formula = (BFormula) next;
final EAnnotation annotation = formula
.getEAnnotation(TextPositionUtil.ANNOTATION_TEXTRANGE);
assertNotNull(annotation);
} else if (next instanceof TextRange) {
// test: the position information is within the expected range
final TextRange range = (TextRange) next;
assertTrue(range.getOffset() + " >= " + offset, range
.getOffset() >= offset);
assertTrue(range.getOffset() + " < " + offset + input.length(),
range.getOffset() < offset + input.length());
assertTrue(range.getLength() + " > " + 0, range.getLength() > 0);
assertTrue(range.getLength() + " <= " + input.length(), range
.getLength() <= input.length());
} else if (!(next instanceof EAnnotation)) {
System.out.println("Found untested types: "
+ next.getClass().getSimpleName());
}
}
}
}
org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/CoreModelTest.java deleted 100644 → 0
+ 0
− 22
View file @ 60237533
package org.eventb.texttools.internal.parsing;
import junit.framework.TestCase;
import org.eclipse.emf.common.util.EList;
import org.eventb.emf.core.machine.Machine;
import org.eventb.emf.core.machine.MachineFactory;
public class CoreModelTest extends TestCase {
public void testRefinesNames() throws Exception {
Machine machine = MachineFactory.eINSTANCE.createMachine();
EList<String> list = machine.getRefinesNames();
list.add(0, "AbstractMac3");
list.add(0, "AbstractMac2");
list.add(0, "AbstractMac1");
assertEquals(3, machine.getRefinesNames().size());
assertEquals(3, machine.getRefines().size());
}
}
org.eventb.texttools.test/src/org/eventb/texttools/internal/parsing/TransformationVisitorTest.java deleted 100644 → 0
+ 0
− 246
View file @ 60237533
package org.eventb.texttools.internal.parsing;
import junit.framework.TestCase;
import org.eclipse.emf.common.util.EList;
import org.eclipse.jface.text.Document;
import org.eclipse.jface.text.IDocument;
import org.eventb.emf.core.machine.Action;
import org.eventb.emf.core.machine.Convergence;
import org.eventb.emf.core.machine.Event;
import org.eventb.emf.core.machine.Guard;
import org.eventb.emf.core.machine.Invariant;
import org.eventb.emf.core.machine.Machine;
import org.eventb.emf.core.machine.Parameter;
import org.eventb.emf.core.machine.Variable;
import org.eventb.texttools.TextPositionUtil;
import org.eventb.texttools.model.texttools.TextRange;
import de.be4.eventb.core.parser.BException;
import de.be4.eventb.core.parser.EventBParser;
import de.be4.eventb.core.parser.node.Start;
public class TransformationVisitorTest extends TestCase {
public void testMachineWithVariablesAndComments() throws BException {
final String input = "machine Test variables\n" + "varA varB\n"
+ "/*varC\n" + "comment*/" + "varC\n" + "end";
final Start rootNode = parseInput(input, false);
final TransformationVisitor visitor = new TransformationVisitor();
final IDocument document = new Document(input);
final Machine machine = visitor.transform(rootNode, document);
assertEquals("Test", machine.getName());
assertEquals(0, machine.getRefinesNames().size());
assertEquals(0, machine.getSees().size());
final EList<Variable> variables = machine.getVariables();
assertEquals(3, variables.size());
Variable variable = variables.get(0);
assertNull(variable.getComment());
assertEquals("varA", variable.getName());
variable = variables.get(1);
assertEquals("varC\n" + "comment", variable.getComment());
assertEquals("varB", variable.getName());
variable = variables.get(2);
assertNull(variable.getComment());
assertEquals("varC", variable.getName());
}
public void testMachineWithInvariantsAndComments() throws BException {
final String input = "machine Test invariants\n" + "@inv1 1=1\n"
+ "/*inv2\n" + "comment*/" + "@inv2 2=2\n" + "end";
final Start rootNode = parseInput(input, false);
final TransformationVisitor visitor = new TransformationVisitor();
final IDocument document = new Document(input);
final Machine machine = visitor.transform(rootNode, document);
assertEquals("Test", machine.getName());
assertEquals(0, machine.getRefinesNames().size());
assertEquals(0, machine.getSees().size());
assertEquals(0, machine.getVariables().size());
final EList<Invariant> invariants = machine.getInvariants();
assertEquals(2, invariants.size());
Invariant invariant = invariants.get(0);
assertEquals("inv2\n" + "comment", invariant.getComment());
assertEquals("inv1", invariant.getName());
assertEquals("1=1", invariant.getPredicate());
invariant = invariants.get(1);
assertNull(invariant.getComment());
assertEquals("inv2", invariant.getName());
assertEquals("2=2", invariant.getPredicate());
}
public void testTheorems() throws BException {
final String input = "machine Test invariants\n" + "@inv1 1=1\n"
+ "theorem @inv2 2=2\n" + "@inv3 3=3\n" + "end";
final Start rootNode = parseInput(input, false);
final TransformationVisitor visitor = new TransformationVisitor();
final IDocument document = new Document(input);
final Machine machine = visitor.transform(rootNode, document);
final EList<Invariant> invariants = machine.getInvariants();
assertEquals(3, invariants.size());
Invariant invariant = invariants.get(0);
assertNull(invariant.getComment());
assertEquals("inv1", invariant.getName());
assertEquals("1=1", invariant.getPredicate());
invariant = invariants.get(1);
assertNull(invariant.getComment());
assertEquals("inv2", invariant.getName());
assertEquals("2=2", invariant.getPredicate());
assertTrue(invariant.isTheorem());
invariant = invariants.get(2);
assertNull(invariant.getComment());
assertEquals("inv3", invariant.getName());
assertEquals("3=3", invariant.getPredicate());
}
public void testMachineWithEvents() throws BException {
final String input = "machine Test\n" + "refines MacA MacB\n"
+ "events\n" + "ordinary event evt1\n" + "any a\n"
+ "where @grd1 a=1\n" + "then\n" + "@act1 a≔1\n" + "end\n"
+ "\n" + "anticipated event evt2\n" + "refines evtAbstract\n"
+ "any b\n" + "with @x b=x\n" + "then\n" + "@act1 b≔1\n"
+ "end\n" + "end";
final Start rootNode = parseInput(input, false);
final TransformationVisitor visitor = new TransformationVisitor();
final IDocument document = new Document(input);
final Machine machine = visitor.transform(rootNode, document);
assertEquals("Test", machine.getName());
assertEquals(2, machine.getRefinesNames().size());
assertEquals("MacA", machine.getRefinesNames().get(0));
assertEquals("MacB", machine.getRefinesNames().get(1));
assertEquals(0, machine.getSees().size());
assertEquals(0, machine.getVariables().size());
final EList<Event> events = machine.getEvents();
assertEquals(2, events.size());
Event event = events.get(0);
assertNull(event.getComment());
assertEquals("evt1", event.getName());
assertEquals(Convergence.ORDINARY, event.getConvergence());
final EList<Parameter> parameters = event.getParameters();
assertEquals(1, parameters.size());
assertNull(parameters.get(0).getComment());
assertEquals("a", parameters.get(0).getName());
final EList<Guard> guards = event.getGuards();
assertEquals(1, guards.size());
assertNull(guards.get(0).getComment());
assertEquals("grd1", guards.get(0).getName());
assertEquals("a=1", guards.get(0).getPredicate());
final EList<Action> actions = event.getActions();
assertEquals(1, actions.size());
assertNull(actions.get(0).getComment());
assertEquals("act1", actions.get(0).getName());
assertEquals("a≔1", actions.get(0).getAction());
event = events.get(1);
assertEquals("evt2", event.getName());
}
public void testEventRefinement() throws BException {
final String input = "machine Test\n" + "events\n" + "event evt1\n"
+ "end\n" + "\n" + "event evt2\n" + "refines evtX evtY\n"
+ "end\n" + "event evt3\n" + "extends evtZ\n" + "end\n" + "end";
final Start rootNode = parseInput(input, false);
final TransformationVisitor visitor = new TransformationVisitor();
final IDocument document = new Document(input);
final Machine machine = visitor.transform(rootNode, document);
final EList<Event> events = machine.getEvents();
assertEquals(3, events.size());
Event event = events.get(0);
assertEquals("evt1", event.getName());
assertEquals(Convergence.ORDINARY, event.getConvergence());
assertEquals(0, event.getRefinesNames().size());
assertFalse(event.isExtended());
event = events.get(1);
assertEquals("evt2", event.getName());
assertEquals(Convergence.ORDINARY, event.getConvergence());
assertEquals(2, event.getRefinesNames().size());
assertFalse(event.isExtended());
event = events.get(2);
assertEquals("evt3", event.getName());
assertEquals(Convergence.ORDINARY, event.getConvergence());
assertEquals(1, event.getRefinesNames().size());
assertTrue(event.isExtended());
}
public void testPositions() throws BException {
final String input = "machine Test\n" + "events\n" + "event X\n"
+ "any Y\n" + "end\n" + "\n" + "event Y\n" + "refines X\n"
+ "end\n" + "end";
final Start rootNode = parseInput(input, false);
final TransformationVisitor visitor = new TransformationVisitor();
final IDocument document = new Document(input);
final Machine machine = visitor.transform(rootNode, document);
final EList<Event> events = machine.getEvents();
assertEquals(2, events.size());
Event event = events.get(0);
final TextRange eventRange1 = TextPositionUtil.getTextRange(event);
assertNotNull(eventRange1);
final EList<Parameter> parameters = event.getParameters();
assertEquals(1, parameters.size());
final Parameter parameter = event.getParameters().get(0);
final TextRange paramRange = TextPositionUtil.getTextRange(parameter);
final TextRange stringRange1 = TextPositionUtil.getInternalPosition(
parameter, parameter.getName());
assertNotNull(paramRange);
assertNotNull(stringRange1);
assertNotSame(eventRange1, paramRange);
assertNotSame(paramRange, stringRange1);
assertSame(stringRange1, TextPositionUtil.getInternalPosition(
parameter, parameter.getName()));
assertEquals(paramRange.getOffset(), stringRange1.getOffset());
assertEquals(paramRange.getLength(), stringRange1.getLength());
event = events.get(1);
final TextRange eventRange2 = TextPositionUtil.getTextRange(event);
assertNotNull(eventRange2);
final EList<String> refinesNames = event.getRefinesNames();
assertEquals(1, refinesNames.size());
final TextRange refinesRange = TextPositionUtil.getInternalPosition(
event, refinesNames.get(0));
assertNotNull(refinesRange);
assertNotSame(eventRange2, refinesRange);
assertSame(refinesRange, TextPositionUtil.getInternalPosition(event,
refinesNames.get(0)));
assertTrue(refinesRange.getOffset() > eventRange2.getOffset());
}
private Start parseInput(final String input, final boolean debugOutput)
throws BException {
final EventBParser parser = new EventBParser();
final Start rootNode = parser.parse(input, debugOutput);
return rootNode;
}
}
org.eventb.texttools/.classpath
+ 2
− 3
View file @ 90d26251
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="src"/>
<classpathentry exported="true" kind="lib" path="lib/aspectjrt.jar"/>
<classpathentry exported="true" kind="lib" path="lib/EventBParser.jar" sourcepath="/de.be4.eventb.parser"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="src" path="src_generated"/>
<classpathentry kind="lib" path="lib/EventBParser.jar"/>
<classpathentry kind="output" path="bin"/>
</classpath>
org.eventb.texttools/.project
+ 12
− 16
View file @ 90d26251
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>org.eventb.texttools</name>
<comment></comment>
<projects>
</projects>
<comment/>
<projects/>
<natures>
<nature>org.eclipse.pde.PluginNature</nature>
<nature>org.eclipse.jdt.core.javanature</nature>
<nature>org.eclipse.pde.api.tools.apiAnalysisNature</nature>
</natures>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
<arguments/>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.ManifestBuilder</name>
<arguments>
</arguments>
<arguments/>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.SchemaBuilder</name>
<arguments>
</arguments>
<arguments/>
</buildCommand>
<buildCommand>
<name>org.eclipse.pde.api.tools.apiAnalysisBuilder</name>
<arguments>
</arguments>
<arguments/>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.pde.PluginNature</nature>
<nature>org.eclipse.jdt.core.javanature</nature>
<nature>org.eclipse.pde.api.tools.apiAnalysisNature</nature>
</natures>
<linkedResources/>
</projectDescription>
org.eventb.texttools/.settings/org.eclipse.jdt.core.prefs deleted 100644 → 0
+ 0
− 12
View file @ 60237533
#Sun May 10 11:23:16 CEST 2009
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=1.5
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.5
org.eventb.texttools/META-INF/MANIFEST.MF
+ 4
− 4
View file @ 90d26251
......@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: Event-B EMF Texttools
Bundle-SymbolicName: org.eventb.texttools;singleton:=true
Bundle-Version: 3.0.0.qualifier
Bundle-Version: 3.0.1.qualifier
Bundle-Activator: org.eventb.texttools.TextToolsPlugin
Require-Bundle: org.eclipse.jface.text;bundle-version="[3.6.0,4.0.0)",
org.eventb.emf.formulas;bundle-version="[1.3.2,2.0.0)",
......@@ -11,7 +11,8 @@ Require-Bundle: org.eclipse.jface.text;bundle-version="[3.6.0,4.0.0)",
org.eclipse.emf.compare;bundle-version="[1.2.2,2.0.0)",
org.eclipse.emf.compare.diff;bundle-version="[1.2.2,2.0.0)",
org.eclipse.emf.compare.match;bundle-version="[1.2.2,2.0.0)",
org.eclipse.core.resources;bundle-version="[3.8.1,4.0.0)";visibility:=reexport
org.eclipse.core.resources;bundle-version="[3.8.1,4.0.0)";visibility:=reexport,
org.eclipse.emf.ecore
Bundle-ActivationPolicy: lazy
Bundle-RequiredExecutionEnvironment: J2SE-1.5
Export-Package: de.be4.eventb.core.parser.node,
......@@ -21,7 +22,6 @@ Export-Package: de.be4.eventb.core.parser.node,
org.eventb.texttools.model.texttools,
org.eventb.texttools.prettyprint,
org.eventb.texttools.syntaxExtension
Bundle-ClassPath: lib/aspectjrt.jar,
lib/EventBParser.jar,
Bundle-ClassPath: lib/EventBParser.jar,
.
Bundle-Vendor: Heinrich-Heine University Dusseldorf
org.eventb.texttools/build.properties
+ 2
− 4
View file @ 90d26251
......@@ -4,7 +4,5 @@ output.. = bin/
bin.includes = META-INF/,\
.,\
plugin.xml,\
lib/EventBParser.jar,\
lib/aspectjrt.jar
src.includes = lib/EventBParser.jar,\
lib/aspectjrt.jar
lib/EventBParser.jar
src.includes = lib/EventBParser.jar
org.eventb.texttools/pom.xml 0 → 100644
+ 19
− 0
View file @ 90d26251
<?xml version="1.0" encoding="UTF-8"?>
<project
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd" xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<modelVersion>4.0.0</modelVersion>
<parent>
<groupId>org.eventb.texteditor</groupId>
<artifactId>org.eventb.texteditor.parent</artifactId>
<version>1.0.0.qualifier</version>
<relativePath>../org.eventb.texteditor.parent/pom.xml</relativePath>
</parent>
<groupId>org.eventb.texteditor</groupId>
<artifactId>org.eventb.texttools</artifactId>
<version>3.0.1.qualifier</version>
<packaging>eclipse-plugin</packaging>
</project>
\ No newline at end of file
org.eventb.texttools/src/org/eventb/texttools/diff/EventBAttributesCheck.java
+ 0
− 7
View file @ 90d26251
......@@ -48,20 +48,13 @@ public class EventBAttributesCheck extends AttributesCheck {
//ignore contents of string 2 string map entries (e.g. in RodinInternalDetails)
// FIXME: make this more specific to RodinInternalDetails
ignore = ignore || (container instanceof ENamedElement && "StringToStringMapEntry".equals(((ENamedElement) container).getName()));
//ignore contents of Annotations
// FIXME: make this more specific to RodinInternalDetails
ignore = ignore || container.equals(CorePackage.eINSTANCE.getAnnotation());
//ignore reference (instead, the derived attribute 'name' will be shown)
ignore = ignore || attribute.equals(CorePackage.eINSTANCE.getEventBElement_Reference());
//ignore generated and local generated attributes as these must be preserved
ignore = ignore || attribute.equals(CorePackage.eINSTANCE.getEventBElement_Generated()); //ADDED
ignore = ignore || attribute.equals(CorePackage.eINSTANCE.getEventBElement_LocalGenerated()); //ADDED
//ignore attributes of Abstract Extension
ignore = ignore || container.equals(CorePackage.eINSTANCE.getAbstractExtension());
//ignore attributes of Extension
ignore = ignore || container.equals(CorePackage.eINSTANCE.getExtension()); //ADDED
return ignore;
......
org.eventb.texttools/src/org/eventb/texttools/diff/EventBReferencesCheck.java
+ 1
− 3
View file @ 90d26251
......@@ -28,7 +28,6 @@ import org.eclipse.emf.ecore.EReference;
import org.eclipse.emf.ecore.EcorePackage;
import org.eclipse.emf.ecore.util.EcoreUtil.CrossReferencer;
import org.eventb.emf.core.CorePackage;
import org.eventb.emf.core.machine.MachinePackage;
public class EventBReferencesCheck extends ReferencesCheck {
......@@ -87,7 +86,6 @@ public class EventBReferencesCheck extends ReferencesCheck {
ignore = ignore || reference.isContainer();
ignore = ignore || reference.eContainer().equals(EcorePackage.eINSTANCE.getEGenericType());
String name = reference.getName();
// ignore = ignore || MachinePackage.eINSTANCE.getMachine_Refines() == reference; //Would this be a better way to check references rather than comparing names?
ignore = ignore || "refines".equals(name);
ignore = ignore || "sees".equals(name);
ignore = ignore || "extends".equals(name);
......
org.eventb.texttools/src/org/eventb/texttools/internal/parsing/TransformationVisitor.java
+ 9
− 0
View file @ 90d26251
......@@ -25,6 +25,7 @@ import org.eventb.emf.core.context.ContextFactory;
import org.eventb.emf.core.machine.Action;
import org.eventb.emf.core.machine.Convergence;
import org.eventb.emf.core.machine.Event;
import org.eventb.emf.core.machine.Guard;
import org.eventb.emf.core.machine.Invariant;
import org.eventb.emf.core.machine.Machine;
import org.eventb.emf.core.machine.MachineFactory;
......@@ -42,6 +43,7 @@ import de.be4.eventb.core.parser.node.AConstant;
import de.be4.eventb.core.parser.node.AContextParseUnit;
import de.be4.eventb.core.parser.node.AConvergentConvergence;
import de.be4.eventb.core.parser.node.ADerivedAxiom;
import de.be4.eventb.core.parser.node.ADerivedGuard;
import de.be4.eventb.core.parser.node.ADerivedInvariant;
import de.be4.eventb.core.parser.node.AEvent;
import de.be4.eventb.core.parser.node.AExtendedEventRefinement;
......@@ -262,6 +264,13 @@ public class TransformationVisitor extends DepthFirstAdapter {
node.getPredicate(), node.getName(), node.getComments(), true);
}
@Override
public void outADerivedGuard(final ADerivedGuard node) {
Guard guard = MachineFactory.eINSTANCE.createGuard();
guard.setTheorem(true);
handleLabeledPredicate(guard, node, node.getPredicate(), node.getName(), node.getComments(), true);
}
@Override
public void outAParameter(final AParameter node) {
handleNamedAndCommented(MachineFactory.eINSTANCE.createParameter(),
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment