Skip to main content


Eclipse Community Forums
Forum Search:

Search      Help    Register    Login    Home
Home » Modeling » OCL » Valuation of forAll in combination with @pre and check of vanished items
Valuation of forAll in combination with @pre and check of vanished items [message #1507079] Thu, 11 December 2014 09:53 Go to next message
Nils Przigoda is currently offline Nils PrzigodaFriend
Messages: 14
Registered: September 2013
Location: Bremen, Germany
Junior Member
Hi,

I've question about the valuation of a concrete postcondition in one of my models. To keep it as simple as possible, I tried to minize the model without losing important any information.

The model is the following:
class Board {
  op void magic_move();
  !ordered ref Field[+] fields;
  !ordered ref Item#board items;
}

class Field {
  !ordered ref Board[1] board;
  !ordered ref Field[*] neighbours;
  !ordered ref Field[*] moveableNeighbours;
  !ordered ref Item#field item;
}

class Item {
  !ordered attr int[1] ~id;
  !ordered attr int[1] partition;
  !ordered ref Field[1]#item field;
  !ordered ref Boardp[1]#items board;
}

The operation Board::magic_move(): should simulate the movement of items on the board. For this purpose, I differ between the moveableNeighbours and neighbours. A moveableNeighbours is directly connected field, to which an item could move. The reference neighbours is a superset of moveableNeighbours, where items only can "see" each other, ensured by the invariant
context Field inv: (self.neighbours->includesAll(self.moveableNeighbours))

Items of different partitions should not be in neighbouring fields at any system state:
Context Item
    inv blockNeighbours:
        self.field.neighbours->forAll( f |
            if f.item->isEmpty()
            then true
            else f.item.partition = self.partition
            endif
        )


Back to the operation Board::magic_move():, I do not only want to ensure that items of different partitions are not in neighbouring field, but also over the pre- and post-state, i.e. it the following example should be illegal:
pre-state:        post-state:

F6---F7---F8      F6---F7---F8
|    |    |       |I0  |    |
|    |    |       |    |    |
F3---F4---F5      F3---F4---F5
|I0  |    |       |    |    |
|    |    |       |    |    |
F0---F1---F2      F0---F1---F2
           I1           I1    

Note that only moveableNeighbours are marked with | or -, and that all fields in a small square are in neighbours. For example, the field F0 has the moveableNeighbours F1 and F3 and the neighbours F1, F3, and F4. The item I0 and I1 should have different partitions are connected the field left above.

To avoid such an illegal operation, I wrote the following post conditions:
context Board::magic_move():
    post blockNeighboursOfPreState:
        Item.allInstances()->forAll( i |
            (   i.field@pre.neighbours@pre->forAll( f |
                    if f.item@pre->isEmpty()
                    then true
                    else f.item.partition@pre = i.partition
                    endif
                )
            )
        )

But I'm not completely convinced the postconditions above because I'm not really shure over which Set of field f will be evaluted. That's why I added randomly @pre in the inner ite-expression. After carefully reading the OMG OCL Spec (v2.4, p. 235f.), I think that f will be something like pointers to Field in the post state and just removing the @pre in the ite is want I'm looking for.
Is this correct?
And if not, does somebody know how I have to adjust the postcondition such that it will be evaluated as desired?

My second question if about the creation and deletion of items in the same model. I've found the operation oclIsNew() to check whether an object is created. But I want to make sure that each time when the operation magic_move is called at least one item moves, will be created or vanishes. My try to model this looks like:
    post oneItemMustMoveOrVanish:
        self.items->exists( i |
               (   i.field
                <> i.field@pre)
            or (    i.oclIsUndefined()
                 <> i@pre.oclIsUndefined()
               )
            or ( i.oclIsNew() )
        )

Which is parsed as invalid OCL code:
org.eclipse.ocl.SemanticException: @pre may only be applied to feature calls (<-- refering to i@pre)
	at org.eclipse.ocl.util.OCLUtil.checkForErrors(OCLUtil.java:358)
	at org.eclipse.ocl.OCL.parse(OCL.java:323)
...


Does somebody know/see what I'm doing wrong here?
Honestly, I would prefer a solution using Item.allInstances() instead one with a relation between Board and Items, because it is not used anywhere else and I'd like to remove it.

Details about the used Eclipse version:
Eclipse Modeling Tools Version: Kepler Service Release 2 Build id: 20140224-0627
or.eclipse.ocl OCL (Object Constraint Language) Version: 3.3.0.v20140120-1508

If I forget any further information, let me know.

Regards,
Nils
Re: Valuation of forAll in combination with @pre and check of vanished items [message #1512030 is a reply to message #1507079] Mon, 15 December 2014 11:36 Go to previous message
Nils Przigoda is currently offline Nils PrzigodaFriend
Messages: 14
Registered: September 2013
Location: Bremen, Germany
Junior Member
I've found a solution for my second problem:

    post oneItemMustMoveOrVanish:
           ((Drop.allInstances@pre()) <> (Drop.allInstances()))
        or (Drop.allInstances()->exists( d |
                d.field <> d.field@pre
            ))
Previous Topic:OCLinEcore Problem
Next Topic:problem in evaluating the UML model with OCL API
Goto Forum:
  


Current Time: Tue Mar 19 09:53:16 GMT 2024

Powered by FUDForum. Page generated in 0.04052 seconds
.:: Contact :: Home ::.

Powered by: FUDforum 3.0.2.
Copyright ©2001-2010 FUDforum Bulletin Board Software

Back to the top