Counting the number of transitions in DrinkVendingMachine-COL-N
2 posters
Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission
Page 1 of 1
Counting the number of transitions in DrinkVendingMachine-COL-N
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
Re: Counting the number of transitions in DrinkVendingMachine-COL-N
That is a good question. I forward it to the author of the unfolding tool we used.
Forum for the Model Checking Contest :: MCC'2017 (archives) :: Questions about models and model submission
Page 1 of 1
Permissions in this forum:
You cannot reply to topics in this forum