semantics of place-bound

by **Admin** Sat 10 Feb - 9:56

Junaid wrote:
We have a question about the following definition in the Formula Manual for MCC 2018:

"Bound formulas are formed only by atoms place-bound(·), whose semantics is defined as follows:
• The atom place-bound(p1 , . . . , pn ) evaluates to some natural number c so that c is the maximum number of tokens that any reachable marking can put in all n places p1, p2, . . . , pn at the same time."

We are not sure of the semantics of place-bound(p1 , . . . , pn ). Is it one of the following?

A:
place-bound(pi) = maximum number of tokens that any reachable marking can put in place pi
place-bound(p1 , . . . , pn) = max(place-bound(p1) , . . . , place-bound(pn))

B:
place-bound(p1 , . . . , pn) = max(token-count(p1 , . . . , pn) for all reachable markings)

Could you please clarify if A is correct or B, or if it is something else?

Thank you,
Best Regards,
Junaid

Thank you very much for your question. After discussion with the Formula experts, their answer is B.