Feedback wanted: invariant constraints in AlphaSimple/TextUML

I am working on support for invariant constraints in AlphaSimple/TextUML.

Some of the basic support has already made into the live site. For instance, the AlphaSimple project has a rule that says:

A user may not have more than 3 private projects.”

This in TextUML looks like this:


class User 

    attribute projects : Project[*] 
        invariant Maximum 3 private projects { 
            return self.privateProjects.size() <= 3
        };
        
    derived attribute privateProjects : Project[*] := () : Project[*] {
        return self.projects.select((p : Project) : Boolean {
            return not p.shared
        });
    };

end;

(Note the constraint relies on a derived property for more easily expressing the concept of private projects, and that backslashes are used to escape characters that otherwise would not be allowed in identifiers, such as whitespaces.)

What do you think? Does it make sense? I know the syntax for higher order functions could benefit from some sugar, but that can be easily fixed later. I am much more interested in feedback on the idea of modeling with executable constraints than in syntax.

Wading in unknown waters

I am in the process of modeling a real world application in AlphaSimple and for most cases, the level of support for constraints that we are building seems to be sufficient and straightforward to apply.

I have though found one kind of constraint that is hard to model (remember, AlphaSimple is a tool for modeling business domains, not a programming language): in general terms, you cannot modify or delete an object if the object (or a related object) is in some state. For example:

"One cannot delete a project's files if the project is currently shared".

Can you think of a feature in UML that could be used to address a rule like that? I can't think of anything obvious (ChangeEvent looks relevant at a first glance, but there is no support for events in TextUML yet).

Any ideas are really appreciated.

EmailFacebookLinkedInGoogle+Twitter

6 thoughts on “Feedback wanted: invariant constraints in AlphaSimple/TextUML

  1. del65

    March 1, 2012 at 5:37am

    Activity diagrams can help here : according to the places/transitions semantics introduced in UML 2 the rule “One cannot delete a project’s files if the project is currently shared” can be nicely defined, executed and even mathematically proven.

    places : unshared, shared
    transitions : (un)share project, delete file

    Unshared
    ->(x)| delete file
    | |
    | v
    ====== (un)share project
    | |
    | v
    –( ) Shared

    Applet with some exemples of perti net charts :
    http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/java/Vargiu/

  2. rafael.chaves

    March 1, 2012 at 8:24am

    Hi, thanks for the comment.

    I couldn’t quite get what you are referring to. Would you be referring to state charts instead of activity diagram (the link you posted has examples of state machines)? The UML spec only talks about transitions in the context of state machines? Unfortunately I didn’t manage to understand the diagram you posted, ascii art does not like automatic left justification…

  3. Jordi Cabot

    March 2, 2012 at 5:35am

    I’d say all depends on how you represent the object “state”. If knowing the state is so important you can always add a new attribute that identifies the state the object is in (this attribute could be modified by the operations that are used to transition the object from one state to the other).

    If the state is “materialized” then invariants or preconditions can be used as you already do now

    • rafael.chaves

      March 2, 2012 at 9:20am

      @Jordi

      I am not sure it is that simple. If all the changes are controlled by operations, sure. But my original intent was to allow direct writes to the objects attributes (or destroying the object) and then control when that is allowed via a constraint, but an invariant can’t really determine *when* a change is allowed as it does not know in what situations it will be evaluated (unless the invariant only evaluated when that attribute was changing, which I don’t think it is how they work, instead they are always in effect) – all they know is the object and property they related to, but what they see is final state of the object. Or am I missing something?

      Btw, I started a similar discussion on LinkedIn. There I got a solution for the delete case (can the object be deleted?). But I think direct modification to properties cannot be dealt with the same way, as I don’t think one can’t hook a property change to a state transition.

  4. del65

    March 2, 2012 at 5:39am

    Since UML 2.x Activity Diagrams uses Petri net like semantics.

    Petri net semantics goes further than state machines : the main difference from state diagrams is that a Petri net diagram uses a set of tokens (the dots in circles depicting a Place) switching from a place to another accros transitions activation (horizontal or vertical “barriers”).

    I digged a little bit further to adapt my previous ascii art diagram to textUML “Action language” notation (see http://sourceforge.net/apps/mediawiki/textuml/index.php?title=TextUML_Action_Language) :

    “share” “unshare” and “deleteFile” operations are transitions.
    “unshared” and “shared” are Place class instances wich acts as places (= token container)

    A token is a Place attribute wich moves along the graph according to transition activation.

    This sample goes beyond the need for a single project “shared” state, but can be improved to more complex situations without compromising the workflow.

    // places initialisation:
    var unshared : Place := new Place(1, 1);
    var shared : Place := new Place(1, 0);

    operation deleteProjectFile();
    precondition (unshared.tokenCount >= 1) raises TokenException
    begin
    // TODO do project file deletion
    end;

    operation share()
    precondition (unshared.tokenCount >= 1 and shared.tokenCount > 0) raises TokenException
    begin
    // move the project token from the “unshared” to the “shared” place
    shared.moveTokenFrom(unshared);
    end;

    operation unshare()
    precondition (shared.tokenCount >= 1 and unshared.tokenCount > 0) raises TokenException
    begin
    // move the project token from the “shared” to the “unshared” place
    shared.moveTokenFrom(unshared);
    end;

    —————————————
    Petri net “Place” semantic declaration
    —————————————
    // Place class declaration
    class Place
    attribute maxTokenCount : Integer;
    attribute tokenCount : Integer;
    [Factory]
    static operation newPlace(theMaxTokenCount : Integer, initialTokenCount : Integer) : Place
    begin
    maxTokenCount := theMaxTokenCount ;
    tokenCount := initialTokenCount;
    end;

    operation moveTokenFrom(Place place)
    predicate (place.tokenCount > 0 and self.tokenCount < self.maxTokenCount) raises TokenException
    begin
    place.tokenCount–;
    self.tokenCount++;
    end;

  5. rafael.chaves

    March 2, 2012 at 9:27am

    @del65

    Thanks for the elaborate answer. Bonus points for using TextUML! So you are talking about petri nets. I vaguely remember designing vending machines in petri nets during a formal methods course back in my undergrad.

    I think your solution ends up relying on an operation (deleteProject), instead of just relying on the object being deleted (or modified) – which I wanted to avoid, but may really be unavoidable, see my comment to Jordi.

Comments are closed.