Looking for contradictions

Help
Andrés
2010-07-16
2013-04-29
  • Andrés
    Andrés
    2010-07-16

    Hello,

    I am trying to use this system in order to check system consistency. The way to do is to look for a instance of the model that fulfills all the invariants.
    When there are any contradictions, it works well, and I have a correct instance of my model. But, if there is a contradiction, USE works for a lot of time (I let it work more than 6 hours), but I don't have the answer from USE that I should have: "No results", or "Any instance that fulfills all the constraints".
    Any idea about how can I do to have this "error" message?

    Thanks, regards

     
  • mkuhlmann
    mkuhlmann
    2010-07-20

    Hi,

    if there is no valid instance the USE-Generator has to consider each system state in the search space which is defined by the user-defined procedure. The search spaces can be very large (e.g., because all possible link constellations are tried). Thus, the USE-Generator may not return a result in the expected time. Currently there is no way to improve the search time for a specific (large) search space. But we are working on a SAT based solution to drastically increase the search time.

    I have a question concerning your statement: "When there are any contradictions, it works well, and I have a correct instance of my model." I do not understand, because there should be no solution if there are contradictions. Did you mean "When there are no contradictions…"?

    Best regards,
    Mirco

     
  • Hi,

    I am interested on automatically generating instances that satisfy UML model and its OCL constraints. Is there is a way to do that?

    Also, the USE document does not have info about USE-Generator. How can I obtain such information?

    Moreover, any information on how to use ASSL with USE tool other than the already published paper will be appreciated.

    Thanks,
    Mustafa 

     
  • Lars Hamann
    Lars Hamann
    2011-04-26

    Hi Mustafa,

    you already mentioned one way to generate system states in a more or less automatic way namely ASSL or the generator.
    ASSL is the name for the language used by the generator.

    The main benefit of the generator is the backtracking feature to search for a system state ins opposite to other ways that can be used in USE.

    I guess you are looking for this, because you asked for information about ASSL. You can find a small documentation and samples for using the generator in the directory "examples/generator".

    We are working on a more detailed documentation.

    Regards!
    Lars

     
  • Hi Lars,

    Thanks for the response. Have you completed the documentation of the generator?

    Also, does USE produce a counterexample in case that a validation case fails?

    I have read the paper of "Validating UML and OCL MOdels in USE by Automatic Snapshot Generation". However, it does not have a VC that fails and the paper does not say anything about counterexamples?

    Is there a way by which USE creates counterexamples showing a particular VC is failing?

    If we treat the VC as a TC, then it would work.

    Thanks,
    Mustafa

     
  • mkuhlmann
    mkuhlmann
    2011-07-13

    Hi Mustafa,
    let us take "A implies B" as a VC, where A may be a set of formulas (e.g., the/some model invariants) and B may be a further property (it may also be a model invariant).

    You can then start the generator while activating all formulas in A and negating B. If generator now finds a valid solution/snapshot/system state, it is a counter example for your assumption that A implies B.

    Please tell me, if I did not understand your problem/aim correctly.

    Best regards,
    Mirco

     
  • Hi Mirco,

    You understood me correctly, explained it elegantly, and gave an awesome example. This is what I want, thanks very much.

    Also, I am interested on the new UML generator that is based on Kodkod and SAT. How to optain it and use it? Is it already in the new release of USE?

    Regards,
    Mustafa

     
  • mkuhlmann
    mkuhlmann
    2011-07-13

    Hi,
    the Model Validator using Kodkod/SAT ist currently in a prototype stage in which we add new features in order to support a specific set of UML and OCL concepts.

    As soon as we have a quality assured version of the Model Validator, we will make it available in SourceForge.

    Best regards,
    Mirco

    P.S. Thank you for pointing out that my example is awesome. So, I will make it the core example in my phd thesis! :P

     
  • Hi Marco,

    I am interested in getting a copy of your thesis, if you have already done with it. I went to your website and could not find a link to it.

    God luck and regards,
    Mustafa

     
  • mkuhlmann
    mkuhlmann
    2012-02-20

    Hi Mustafa,

    it's not done yet. ;)

    Best regards,
    Mirco