New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Duplicate guarded transition allowed in Umple #760

Open
opeyemiAdesina opened this Issue Feb 26, 2016 · 15 comments

Comments

Projects
None yet
4 participants
@opeyemiAdesina
Contributor

opeyemiAdesina commented Feb 26, 2016

class CarTransmission {

Boolean driveSelected;
state {
neutral {
selectReverse -> reverse;
selectDrive -> drive;
selectFirst -> first;
selectSecond -> second;
}

reverse {
  selectNeutral -> neutral;
}

drive {
  selectNeutral -> neutral;
  selectFirst -> first;
  selectSecond -> second;

  first {
    reachSecondSpeed [driveSelected]  -> second;      
    reachSecondSpeed [driveSelected]  -> second;  //duplicate guarded transition 
  }
  second {  }
}

}
}

@vahdat-ab

This comment has been minimized.

Member

vahdat-ab commented Feb 26, 2016

I think we need to build a truth table for conditions and make sure they are not the same. This concept can be more complicated when we have fix values participated in the boolean expression or one of the conditions are reduced.
I believe this algorithm is really important for Umple in order to guarantee non-deterministic state machines. I have done a small search (as part of my own work) but couldn't find a concrete algorithm for this purpose.

@TimLethbridge

This comment has been minimized.

Member

TimLethbridge commented Feb 26, 2016

Right. So duplicate guarded transitions are OK as long as there are no situations where two of the guards can be true at the same time. If two guards are identical, as in the example at the start of this issue then there should be a warning. Then there should be a different warning if they are not the same but are not mutually exclusive. There should be no warning if they are mutually exclusive.

@opeyemiAdesina

This comment has been minimized.

Contributor

opeyemiAdesina commented Feb 26, 2016

A warning is sufficient for the case presented in the issue. However, I have implemented a temporary solution to prevent such duplicates in the list returned by "*.getAllTransitions()" as it guarantees correct output for nuXmv pending the time the issue is resolved.

@vahdat-ab

This comment has been minimized.

Member

vahdat-ab commented Feb 26, 2016

Consider the following simple example:

class A{
    Boolean x;
    Boolean y;
    status{
        on{
            turnOff[x<y] ->off; //n1
            turnOff[y>x] ->off; //n2
            turnOff[x<y] -> on; //n3
        }
        off{
            turnOn[x>y] -> on; //f1
            turnOn[y<=x] -> on; //f2
            turnOn[y==x] -> off;//f3
        }
    }
}

There is no conflict between n1 and n2 because they go to the same state. Therefore, there is no worry. We may consider to just warn the designer about his/her design.

There is conflict obviously between (n1 and n3) and (n2 and n3). I think we should generate an error because it makes Umple state machines non-deterministic, except if would like to support non-deterministic state machines. In that case, we must provide a mechanism to deal those cases, such as prioritization.

There is another non-deterministic case between f2 and f3 .

@tlaport4 tlaport4 self-assigned this Oct 11, 2016

@tlaport4

This comment has been minimized.

Contributor

tlaport4 commented Dec 13, 2016

Is there a final verdict on whether we should be generating an error or just a warning in the cases outlined in Vahdat's last post?

@TimLethbridge

This comment has been minimized.

Member

TimLethbridge commented Dec 13, 2016

If there is no guard, it is a warning if there are two identical events. We get:
45 Warning on line 10 : Transition xxxxx will be ignored due to a unguarded duplicate event.
If there are guards and both event and guards are identical, then logically it should also be a warning. The duplicate is ignored. It should work like error 45 does now. Message would be
Transition xxxxx will be ignored to to duplicate events with identical guards.

@tlaport4

This comment has been minimized.

Contributor

tlaport4 commented Dec 20, 2016

In PR #938, I added logic to ignore transitions that have the same event and equivalent guard as another transition. The warning message displayed is "Guarded Transition xxxxx will be ignored due to a duplicate event with an equivalent guard".

Also works for auto transitions that have equivalent guards.

The logic for determining whether two guards are equivalent will do most basic comparison between the guards. For example, two guards like [(x + y) < z] and [z >= (y+x)] would be confirmed as equivalent. Also, works for more complicated guards that use negation and constraintBody's (parenthesis -- OPEN_ROUND_BRACKET [[constraint]] CLOSE_ROUND_BRACKET). See PR

@vahdat-ab

This comment has been minimized.

Member

vahdat-ab commented Dec 22, 2016

Another example

class A{
  sm{
    on{
      [x>y]-> off;
      [y<x]-> on;
    }
    off{  } 
  }

This should not be allowed.

@tlaport4

This comment has been minimized.

Contributor

tlaport4 commented Dec 22, 2016

Hmmm yeah that's right.

When I wrote I for some reason I thought the equivalent of > would be <=, but that's the opposite. I'll quickly update it.

@tlaport4

This comment has been minimized.

Contributor

tlaport4 commented Dec 22, 2016

I updated the CR and all the tests just passed.

@vahdat-ab

This comment has been minimized.

Member

vahdat-ab commented Dec 22, 2016

You algorithm cannot detect the issue related to f2 and f3 in the above example

@tlaport4

This comment has been minimized.

Contributor

tlaport4 commented Dec 22, 2016

Those aren't necessarily equivalent though. They're only equivalent when x = y. What should it do? Should either one be ignored?

@vahdat-ab

This comment has been minimized.

Member

vahdat-ab commented Dec 23, 2016

This is a dynamic behavior and from my perspective, it must be notified to the modeler. However, maybe @TimLethbridge and @opeyemiAdesina want to comment more about this case.
This clearly shows that the state machine has this potential to be in two states. However, it might never happen because of a restriction on the values of x and y (e.g. OCL constraint). For example, someone might define a constraint in which it is said x and y must not be equal.

@TimLethbridge

This comment has been minimized.

Member

TimLethbridge commented Dec 24, 2016

This is a case where one guard is a sub-case of another. We can't easily compute all these cases logically (i.e. analyse all truth tables). In this case one could compute easily that one is a sub-case, but cases get complex very quickly. I say we leave this unless we are going to go 'whole-hog' and try to compute all the cases that are computable statically (this is a static case).

I don't call this non-determinism by the way. In Umple, order of declaration determines which case applies. It is only nondeterministic if it can change. But it is under-specified what happens in the presence of traits, and with mixins the order can be hard to be sure about.

@TimLethbridge

This comment has been minimized.

Member

TimLethbridge commented Nov 21, 2017

Maybe this issue can be closed, as it is partly solved. But more testing would be useful

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment