Frank

The "trivially" variants of the outcomes are introduced by Kodkod, the underlying library used to solve for model instances. Kodkod is a very powerful tool that performs a lot of transformations and optimizations before handing the instance to a SAT solver. In some cases this preparation work makes it apparent that the model contains a contradiction or that there exists an instance. In these cases the SAT solver is not even started and Kodkod conveys this information with the trivially variants of...

You can put in the desired Strings in the 'Preferred Values' section on the basic types tab. The role is important for the navigations in OCL. Please refer to a lecture for basic UML/OCL usage like this. Associations are bidirectional. There is not really a start or end, but participants and the connected classes are assigned properties to navigate to based on the roles of the connected association.

What I meant was that USE supports the UML semantics as defined in the UML standard from the OMG. The same features are also supported by Eclipse, but the file formats to define models are vastly different and not automatically interchangable. You will have to create a new UML model in the .use file format by hand, but the semantics will be the same as the one you have already.

1st. In order for specific strings to work, you have to define the set of strings adequately. In this case using the String 'hi', your configuration would need to look like: String_max = 10 String = Set{'hi'} Without the explicit list of strings they are automatically generated following the pattern 'stringN', where N is a number denoting this being the N-th String. So for example: 'string1', 'string2', etc. 2nd. The navigation over association works with the roles of the association. This is not...

Hi, if there are no invariants shown in the configuration GUI then they are either not part of the model or could not be translated to Kodkod/Alloy. In the latter case, there would be an output on the shell. Did you put in the invariant after you loaded the model maybe? When you change the model definition file (.use file) you have to reload/reopen it in USE for the changes to take effect. You can check the current invariants in the USE main window with the view from the lightning icon. Other than...

First of all: Always pay close attention to the output of the model validator on the shell. If an invariant cannot be used it will tell you there and will report on eventual problems during the validation. For the given model, if the plugin outputs Satisfiable then there could be a system state found that satisfies all invariants (explicit in OCL and implicit from thne UML structure etc.) and that system state is then loaded in USE. If the output is Unsatisfiable, there exists no system state that...

Hi, the USE tool does support UML. The class containing the execution of the model generation process from the GUI and shell is: org.tzi.use.kodkod.plugin.KodkodValidateCmd . You can find the program sources in the files section. It should give you pointers to the configuration process of the model and the start of the model validation.

There is currently no plugin to convert between the formats automatically. However, USE supports most class diagram features and there should not be a problem representing the EMF model in USE. isDefined() is a USE specific OCL construct similar to oclIsUndefined(). There are a few of those present in USE that are usually from a time when the OCL standard did not have official support for such features, but the majority of them are supported by the MV plugin. Keep and eye on the console when using...