Re: [henshin-dev] loop transitions in state space example

[Christian Krause <henshin.ck@xxxxxxxxx>]

Hi Daniel,

the rule uses so-called amalgamation to match *all* unshared secrets. This is indicated by the star-operators. If there are no unshared secrets, the for-all condition is still fulfilled (there are no unshared secrets, so all of them are matched ;) ). Therefore, if there are no unshared secrets, the rule is still applicable but it won't change the graph. This is the reason why you get a self-loop transition. You can also compare it with matching a regular _expression_ like x*  --> the empty string matches this _expression_. 

I hope this helps.

Cheers,

Christian

2014-10-01 22:06 GMT+02:00 Daniel Jungblut <jungblut.d@xxxxxxxxx>:

Dear Christian,

I am just exploring the different henshin features and have a question concerning the GossipingGirls State Space example:

Why can there be loop transitions, meaning that secrets will be shared between girls that have already shared their secrets, if the NAC (already existing transitions between a girl and the secret of another are marked "forbid") should prevent the rule "exchangeSecrets (g1, g2)" from beeing applied?

Thanks in advance!

Cheers,

Daniel
_______________________________________________
henshin-dev mailing list
henshin-dev@xxxxxxxxxxx
To change your delivery options, retrieve your password, or unsubscribe from this list, visit
https://dev.eclipse.org/mailman/listinfo/henshin-dev