som-research / emftocsp Goto Github PK

View Code? Open in Web Editor NEW

14.0 14.0 2.0 3.07 MB

Bounded verification of UML/OCL (or EMF/OCL) models

License: Eclipse Public License 1.0

HTML 7.72% Prolog 21.55% Java 69.27% CSS 0.13% XSLT 1.33%

emftocsp's People

Contributors

Stargazers

Watchers

Forkers

ferhaterata daylyt247

emftocsp's Issues

No support for OCL closure

have an OCL constraint using the OCL closure expression but it is not supported by EMFtoCSP: the generated ECL file contains a call to ocl_col_closure but this operation is not to be found in the ECL libraries.

Validate command is only available in java perspective

[enhancement]

The "Validate model" command only appears if the java perspective is enabled. This is not very intuitive (and undocumented).

Version: emftocsp head from git as of today

'Aborting execution' on large metamodel

Hello,

I have been experimenting EMFtoCSP on a relatively large metamodel and have been running into problems.

I ran into a first problem related to the cardinalities of metaclasses which got me to learn how to use the Tracer tool in ECLiPSe and figure out that the cardinalities were too low to achieve strong satisfiability (one abstract metaclass had many implementing metaclasses and needed a higher cardinality). A priori now the cardinalities should be consistent and the execution goes beyond the first error.

However I am running into another problem that I am unable to understand.

I loaded the ECL generated file in ECLiPSe (strong satisfiability) followed by the uml and ocl libraries as is done by your plugin. I am getting the following error in ECLiPSe:

no_value(_23692{1 .. 14})
Aborting execution ...

Following the execution with the Tracer shows the problem occurs on a call to ic_global_gac:gcc at uml_basic.ecl:278 with the following call stack:

+(0) 0 .... trace_body(..., ...)
(1) 1 .... findSolutions(...)
(79944) 2 .... cardinalityLinkscodemodel_modules(...)
(79945) 3 .... linksConstraintMultiplicities(..., ..., ..., ...)
(80059) 4 .... linksConstraintMultiplicities3(..., ..., ..., ...)
(80069) 5 LEAVE gcc(..., ...)

(you can stop the execution at the problem by selecting the port type 'leave' in the Tracer and clicking 'To Port')

It seems to me that the problem is not that the set of constraints are unsatisfiable because I do not get the regular 'No' answer. This seems like an exceptional behavior but I do not know how to further investigate it.

Has anybody encountered this issue before and hopefully has a solution?
Otherwise does anybody have a suggestion on how I could further investigate the problem?

Attached are the metamodel and the corresponding ECL file.

Best regards,
Elie

Choosing weak Satisfiability correctness property results in instance that violates invariants

Consider the simple ecore model in attachment.

Try to validate the model with the domains and cardinalities as set in the screenshot (attach). When selecting
the correctness property:

strong satisfiability: A correct model instance is generated (ie. in this model instance the size of the yourClass Set is equal to 1 and the model instance contains one instance of YourClass. This is as expected.
weak satisfiability: In this case the solver generates a model instance (see graphviz output attach) in which the invariant is not respected: the resulting model contains no instance of YourClass! I Assume that weak satisfiability means that not all classes need to be instantiated, however all invariants need to satisfied.

What version of the product are you using? On what operating system?

emftocsp from git
eclipseclp 6.1.194 on mac os x x86_64

impliesTest.ecore : https://copy.com/p4mLFUaEaZ2y

"null" when validating model on Eclipse 2019-03

Hi, first thanks for the interesting work which I am looking forward to try out.

I have installed EMFtoCSP according to https://github.com/SOM-Research/EMFtoCSP/wiki/Installing-EMFtoCSP on Eclipse 2019-03 with JDK8, including:

ECLiPSe Constraint Programming System 6.1
Graphviz 2.38
EMF - Eclipse Modeling Framework SDK 2.17.0.v20190301-1325 org.eclipse.emf.sdk.feature.group Eclipse Modeling Project
OCL Classic SDK: Ecore/UML Parsers,Evaluator,Edit 5.8.0.v20190311-1843 org.eclipse.ocl.all.sdk.feature.group Eclipse OCL
and configured the corresponding paths according to https://github.com/SOM-Research/EMFtoCSP/wiki/Using-EMFtoCSP

Unfortunately, I get a "Impossible to Validate the model: null" error message, hinting to make sure that the paths set are correct (which they should be IMO). There's no information in the error log view hinting to an issue s.th. I am stuck here.

The .ecore.log contains this info:

EMFtoCSP LOGS

2019/06/06 10:45:15 class fr.inria.atlanmod.emftocsp.ui.main.commands.WizardHandler: INFO: Starting EMFtoCSP GUI
2019/06/06 10:45:50 class fr.inria.atlanmod.emftocsp.ui.wizards.impl.ModelSelectedWizard: INFO: Closing EMFtoCSP

Does anyone have a hint on what I could try out to make EMFtoCSP work? Or has someone already been successful in getting EMFtoCSP to work with the software stack above?

CastException using sets of Attributes

What steps will reproduce the problem?

(Try to) Validate the simple ecore model in attachment.

The following exception occurs:

Processing constraint: SetSize
Body: myAttribute->size() = 1
java.lang.ClassCastException: org.eclipse.emf.ecore.impl.EAttributeImpl cannot be cast to org.eclipse.emf.ecore.EReference
    at fr.inria.atlanmod.emftocsp.emf.impl.EmfOclParser.updateConcernedRanges(EmfOclParser.java:237)
    at fr.inria.atlanmod.emftocsp.emf.impl.EmfOclParser.setupNumericalRange(EmfOclParser.java:225)
    at fr.inria.atlanmod.emftocsp.emf.impl.EmfOclParser.parseModelConstraints(EmfOclParser.java:200)
    at fr.inria.atlanmod.emftocsp.emf.impl.EmfOclParser.getModelInvariantNames(EmfOclParser.java:372)
    at fr.inria.atlanmod.emftocsp.emf.impl.EmfOclParser.getModelInvariantNames(EmfOclParser.java:1)
    at fr.inria.atlanmod.emftocsp.ui.wizards.impl.PropertiesSelectionPage.fillConstraintsCombos(PropertiesSelectionPage.java:124)
    at fr.inria.atlanmod.emftocsp.ui.wizards.impl.PropertiesSelectionPage.setVisible(PropertiesSelectionPage.java:95)
    at org.eclipse.jface.wizard.WizardDialog.updateForPage(WizardDialog.java:1259)
    at org.eclipse.jface.wizard.WizardDialog.access$4(WizardDialog.java:1238)
    at org.eclipse.jface.wizard.WizardDialog$8.run(WizardDialog.java:1227)
    at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
    at org.eclipse.jface.wizard.WizardDialog.showPage(WizardDialog.java:1225)
    at org.eclipse.jface.wizard.WizardDialog.nextPressed(WizardDialog.java:915)
    at org.eclipse.jface.wizard.WizardDialog.buttonPressed(WizardDialog.java:428)
    at org.eclipse.jface.dialogs.Dialog$2.widgetSelected(Dialog.java:628)
    at org.eclipse.swt.widgets.TypedListener.handleEvent(TypedListener.java:248)
    at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
    at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4166)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1466)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1489)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1474)
    at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1279)
    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4012)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3651)
    at org.eclipse.jface.window.Window.runEventLoop(Window.java:826)
    at org.eclipse.jface.window.Window.open(Window.java:802)
    at fr.inria.atlanmod.emftocsp.ui.commands.AbstractWizardHandler.launchWizard(AbstractWizardHandler.java:108)
    at fr.inria.atlanmod.emftocsp.ui.commands.AbstractWizardHandler.execute(AbstractWizardHandler.java:84)
    at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:290)
    at org.eclipse.ui.internal.handlers.E4HandlerProxy.execute(E4HandlerProxy.java:90)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at org.eclipse.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:56)
    at org.eclipse.e4.core.internal.di.InjectorImpl.invokeUsingClass(InjectorImpl.java:243)
    at org.eclipse.e4.core.internal.di.InjectorImpl.invoke(InjectorImpl.java:224)
    at org.eclipse.e4.core.contexts.ContextInjectionFactory.invoke(ContextInjectionFactory.java:132)
    at org.eclipse.e4.core.commands.internal.HandlerServiceHandler.execute(HandlerServiceHandler.java:167)
    at org.eclipse.core.commands.Command.executeWithChecks(Command.java:499)
    at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:508)
    at org.eclipse.e4.core.commands.internal.HandlerServiceImpl.executeHandler(HandlerServiceImpl.java:213)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.executeItem(HandledContributionItem.java:850)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.handleWidgetSelection(HandledContributionItem.java:743)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.access$7(HandledContributionItem.java:727)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem$4.handleEvent(HandledContributionItem.java:662)
    at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
    at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4166)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1466)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1489)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1474)
    at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1279)
    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4012)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3651)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$9.run(PartRenderingEngine.java:1113)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:997)
    at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:138)
    at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:610)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:567)
    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
    at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:124)
    at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:354)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:181)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:636)
    at org.eclipse.equinox.launcher.Main.basicRun(Main.java:591)
    at org.eclipse.equinox.launcher.Main.run(Main.java:1450)
    at org.eclipse.equinox.launcher.Main.main(Main.java:1426)

Version: emftocsp from git + eclipseclp 6.1
attributeSetTest.ecore : https://copy.com/syrvhLXuWiRo

Invalid let generation

The following domain model produces erroneous ecl code:

package samplemodel : samplemodel = 'http://samplemodel/1.0'
{
    class Person
    {
        invariant testLet:
        let test : Real = 2
        in true;
    }
}

The invariant generates the following piece of ECL code which is invalid:

% OCL constraint let test : Real = 2 in true
nConstant1testLet(_, _, Result):-
    Result=2.
nConstant2testLet(_, _, Result):-
    Result=1.
testLet(Instances):-
    null(Instances, [], Result),
    Result #=1.

SampleModel.ecore : https://copy.com/tunQlbn2oOrb

Operations body not supported

If I try to validate the following domain model, an exception is generated by ECLiPSe:

package samplemodel : samplemodel = 'http://samplemodel/1.0'
{
    class Person
    {
        operation alwaysTrue() : Boolean
        {
            body: true;
        }
        property pets : Animal[3..3] { ordered composes };
        invariant checkAlwaysTrue: alwaysTrue();
    }

    class Animal;
}

The generated ECL file is invalid for the invariant evaluation.
Furthermore, the operation alwaysTrue seems not to be taken into account (nothing gets generated in the ECL file).
SampleModel.ecore : https://copy.com/tunQlbn2oOrb

Graphviz output: represent aggregationkind:Composition by a subgraph

[enhancement]

It would be nice/more intuitive if the owners of composite associations are replaced by graphviz (cluster) subgraphs instead of ordinary nodes.

oclIsTypeOf() not working properly

(related issue, but the solution to that does not seem to have fixed the problem entirely:
https://code.google.com/a/eclipselabs.org/p/emftocsp/issues/detail?id=10)

Consider the following ecore model (expressed below using oclinecore syntax)

package OCLTypeOfTest : oclTypeOfTest = 'http:///oclTypeOfTest.ecore'
{
    annotation _'http://www.eclipse.org/uml2/2.0.0/UML'
    (
        originalName = 'OCLTypeOfTest'
    );
    class Block1
    {
        property block2 : Block2 { composes };
    }
    class Block2;
    class Block2S extends Block2;

    /*
     * self.block2.oclIsTypeOf(Block2S)
     */
    class Block1S extends Block1
    {
        invariant Constraint1: self.block2.oclIsTypeOf(Block2S);
    }
}

then EMFtoCSP comes up with the following solution

Clearly invariant Constraint1 is not satisfied for this instance since Block 1S1 is connected to a Block of type Block2 (for which oclIsTypeOf(Block2S) should fail).

oclAsType not implemented

It seems that the ECL code generator supports the oclAsType since a call to the ocl_oclAsType procedure is generated, but this procedure doesn't exist, causing an exception to be thrown.

Here is a domain model that displays the problem (again, this is not a really useful case but only to display the problem):

package samplemodel : samplemodel = 'http://samplemodel/1.0'
{
    class Person
    {
        property pets#owner : Animal[*] { ordered composes };
        invariant testOclAsType: self.oclAsType(Person).pets->size() = 2;
    }
    class Animal
    {
        property owner#pets : Person;
    }
}

SampleModel.ecore : https://copy.com/H8Zyi8OsOTLF

som-research / emftocsp Goto Github PK

emftocsp's People

Contributors

Stargazers

Watchers

Forkers

emftocsp's Issues

EMFtoCSP LOGS

Recommend Projects

Recommend Topics

Recommend Org