diff --git a/de.prob.units.tests/src/de/prob/units/tests/PragmaAttributesTest.java b/de.prob.units.tests/src/de/prob/units/tests/PragmaAttributesTest.java new file mode 100644 index 0000000000000000000000000000000000000000..f51e9a11f287207248ae54eeca7e4f9d57a0b8db --- /dev/null +++ b/de.prob.units.tests/src/de/prob/units/tests/PragmaAttributesTest.java @@ -0,0 +1,81 @@ +package de.prob.units.tests; + +import org.eclipse.core.resources.IncrementalProjectBuilder; +import org.eclipse.core.runtime.CoreException; +import org.eclipse.core.runtime.NullProgressMonitor; +import org.eventb.core.IConstant; +import org.eventb.core.IContextRoot; +import org.eventb.core.IEventBProject; +import org.eventb.core.IMachineRoot; +import org.eventb.core.IVariable; +import org.junit.Test; +import org.rodinp.core.IAttributeType; +import org.rodinp.core.RodinCore; + +import de.prob.core.translator.TranslationFailedException; + +public class PragmaAttributesTest extends AbstractEventBTests { + final IAttributeType.String UNITATTRIBUTE = RodinCore + .getStringAttrType("de.prob.units.unitPragmaAttribute"); + + @Test + public void testMachineWithUnitPragmaOnVariable() throws CoreException, + TranslationFailedException { + IEventBProject project = createEventBProject("TestProject"); + IMachineRoot machine = createMachine(project, "TestMachine"); + + IVariable v1 = createVariable(machine, "v1"); + createInvariant(machine, "inv1", "v1=5", false); + + // add unit pragma to variable + v1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor()); + + // save file and build workspace - this triggers static check, and + // generates missing files + machine.getRodinFile().save(monitor, false); + workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor); + + // there should be one variable and one SC variable + assertEquals(1, machine.getVariables().length); + assertEquals(1, machine.getSCMachineRoot().getSCVariables().length); + + // and both should hold our attribute + assertEquals("test", + machine.getVariables()[0].getAttributeValue(UNITATTRIBUTE)); + assertEquals("test", + machine.getSCMachineRoot().getSCVariables()[0] + .getAttributeValue(UNITATTRIBUTE)); + } + + @Test + public void testContextWithUnitPragmaOnConstant() throws CoreException, + TranslationFailedException { + IEventBProject project = createEventBProject("TestProject"); + IContextRoot context = createContext(project, "TestContext"); + + IConstant c1 = createConstant(context, "cst1"); + createAxiom(context, "axm1", "cst1=5", false); + + // add unit pragma to constant + c1.setAttributeValue(UNITATTRIBUTE, "test", new NullProgressMonitor()); + + // save file and build workspace - this triggers static check, and + // generates missing files + context.getRodinFile().save(monitor, false); + project.getRodinProject().save(monitor, false); + workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor); + + // there should be one constant and one SC constant + // both holding the attribute + assertEquals(1, context.getConstants().length); + assertEquals(1, context.getSCContextRoot().getSCConstants().length); + + // and both should hold our attribute + assertEquals("test", + context.getConstants()[0].getAttributeValue(UNITATTRIBUTE)); + assertEquals("test", + context.getSCContextRoot().getSCConstants()[0] + .getAttributeValue(UNITATTRIBUTE)); + + } +} diff --git a/de.prob.units.tests/src/de/prob/units/tests/PragmaTranslatorTest.java b/de.prob.units.tests/src/de/prob/units/tests/PragmaTranslatorTest.java index eef489a38f338266853c7da5e8fca80e1cc236d8..f2b199e665188d58e992068aa05f44c0012b61c1 100644 --- a/de.prob.units.tests/src/de/prob/units/tests/PragmaTranslatorTest.java +++ b/de.prob.units.tests/src/de/prob/units/tests/PragmaTranslatorTest.java @@ -81,11 +81,7 @@ public class PragmaTranslatorTest extends AbstractEventBTests { workspace.build(IncrementalProjectBuilder.FULL_BUILD, monitor); // there should be one constant and one SC constant - // the constant holds the attribute assertEquals(1, context.getConstants().length); - assertEquals("test", - context.getConstants()[0].getAttributeValue(UNITATTRIBUTE)); - assertEquals(1, context.getSCContextRoot().getSCConstants().length); TranslatorFactory.translate(context, writer);