[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index] [List Home]
Re: [henshin-user] Nested application conditions in Henshin diagrams?

Thanks, Stefan. Sounds sensible, but also somehow not ideal. I know I've had a similar discussion with Daniel in the past about the need / possibility of having a + operator similar to the current * operator, which basically means you're not considering something a match unless you can find at least one match for the multi-rule. I appreciate, this wouldn't solve my current problem, but it shows another issue with the current definition of multi-rules.

Are there any strong formal reasons for doing things in this way or is this simply something that was never considered so far? I really would like to do a semantics without units if I can help it. I could go down the OCL route, of course, but if this could be done using matching alone that would be better. 

Of course, your explanation doesn't address the issue with the new formulation of the rule, where we're using nested NACs, which better describe the fire condition anyway. My "require*" approach I was never happy with. I was thinking that it would be nice to have a "distinct" annotation for multi-rules, which would randomly pick a subset of all matches for the multi-rule ensuring that there were no overlaps between these matches (apart from those parts of the match that were inherited from the parent rule, of course). That would solve my problem, as I could simply ask for the "LHS multi-rule" (i.e., the one with the delete bit in it) to be "distinct" so that I don't get matches for all tokens for all pre-places, but only for one token for each pre-place.



Dr. rer. nat. Steffen Zschaler AHEA
Senior Lecturer

King's College London
Department of Informatics

Email szschaler@xxxxxxx
Phone +44 (020) 7848 1513
WWW   http://www.steffen-zschaler.de/

-----Original Message-----
From: henshin-user-bounces@xxxxxxxxxxx [mailto:henshin-user-bounces@xxxxxxxxxxx] On Behalf Of S. John
Sent: 02 November 2018 22:32
To: henshin-user@xxxxxxxxxxx
Subject: Re: [henshin-user] Nested application conditions in Henshin diagrams?


sorry for joining this a bit late. I feel I need to comment on the example rule you added in the first place. You said it never matched, which did not really make sense to me. So I rebuilt your example (hopefully identically) and for me the rule works as expected.

- The rule always finds a match as long as there is a transition. The applicability of a rule is not dependent on whether there is a match of the multi-rule.

- Three incoming and one outgoing place are connected to a transition; only on incoming place got tokens:
The multi-rule does not find a match as the require-part and the source-part can not be matched at the same time.

- Three incoming and one outgoing place are connected to a transition; two incoming places got tokens:
All tokens are transferred as the places with tokens are alternately matched for the require-part and the source-part.

You need to consider that the multi-rule creates a match with ONE mapping for each element of the multi-rule and finds. So the require-part can not ensure that all places have a token before you even start to match the rest of the rule. Instead it only ensures that ONE of the other incoming places needs a token, when you found a fitting source place. This is trivially fulfilled if you have at least two incoming places with a token in it.

The descriptions of multi-rules often talk about them being a forAll operator. But that does not mean something can be done for all elements at once. Unfortunately, you can only iterate over the elements and handle them independently.

I'll add the metamodel and rule for reference.

Best wishes,

@Steffen: I think the above problem is actually the reason for the OCL condition in our use case.

On 20.10.2018 09:29, Zschaler, Steffen wrote:
> Hi all,
> I'm trying to figure out how to do nested application conditions in the 
> Henshin diagram editor. I was hoping that this could be done the same 
> way that I can nest multi-rules, using paths in the labels. However, 
> that doesn't seem to do anything useful. Is there a different way of 
> doing this?
> Specifically, I'm trying to write a standard Petri Net firing rule. For 
> this, I would like to add a NAC that there are no source places with no 
> tokens. So, roughly,
> ¬\exists({Transition-Place} à ¬\exists{Transition-Place-Token})
> I've tried using a require* instead, as below, but that rule never 
> matches, even when all source places have a token.
> Any suggestions?
> Many thanks,
> Steffen
> Dr. rer. nat. Steffen Zschaler AHEA
> Senior Lecturer
> King's College London
> Department of Informatics
> Email szschaler@xxxxxxx
> Phone +44 (020) 7848 1513
> WWW   https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.steffen-zschaler.de%2F&data=01%7C01%7Csteffen.zschaler%40kcl.ac.uk%7Cdc13a9a076ed43a85ab208d6411310fd%7C8370cf1416f34c16b83c724071654356%7C0&sdata=OZBd43STSxucrGfkqrsfbv1jaDsHtp3k934y2Y0AxUg%3D&reserved=0
> _______________________________________________
> henshin-user mailing list
> henshin-user@xxxxxxxxxxx
> To change your delivery options, retrieve your password, or unsubscribe from this list, visit
> https://emea01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdev.eclipse.org%2Fmailman%2Flistinfo%2Fhenshin-user&data=01%7C01%7Csteffen.zschaler%40kcl.ac.uk%7Cdc13a9a076ed43a85ab208d6411310fd%7C8370cf1416f34c16b83c724071654356%7C0&sdata=ik4Gz2Yr6SS%2FyG%2FxqxY80CKcJaMZG%2BBmkdKDV79vIG4%3D&reserved=0