Forum for the Model Checking Contest
Would you like to react to this message? Create an account in a few clicks or log in to continue.

Counting the number of transitions in DrinkVendingMachine-COL-N

2 posters

Go down

Counting the number of transitions in DrinkVendingMachine-COL-N Empty Counting the number of transitions in DrinkVendingMachine-COL-N

Post by dalzilio Wed 12 Apr - 15:00


Hello again,

I understand that participants to the previous competitions have a strong opinion about how transitions should be counted. (And this whole topic certainly needs more discussion!) My post has a less general scope and deals only with the DrinkVendingMachine (colored version). I do not have the intention to start a heated discussion. I simply believe that the following problem is worth mentioning.

The model has transitions labeled "elaborate2" that takes any pairs of options in place theOptions and generates tokens in optionSlots. This is done using a (colored) arc with pattern <o1>+<o2>.

You may see now that there are two possible semantics depending on whether + (multiset addition) is considered commutative or not.

The tools performing unfolding and the PT equivalent versions take the stand that + is not commutative. For any pair of colored pattern in theOptions, we find a pair of duplicate transitions in the resulting ordinary net.

Is this behavior mandated by "the standard" ? If yes, how is it defined ?

Silvano



dalzilio

Posts : 31
Join date : 2017-03-29

Back to top Go down

Counting the number of transitions in DrinkVendingMachine-COL-N Empty Re: Counting the number of transitions in DrinkVendingMachine-COL-N

Post by Admin Wed 12 Apr - 17:25

That is a good question. I forward it to the author of the unfolding tool we used.

Admin
Admin

Posts : 25
Join date : 2016-11-26

https://mc-contest.forumactif.com

Back to top Go down

Back to top


 
Permissions in this forum:
You cannot reply to topics in this forum