Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: deprecated: process-io

Topic: help with petrinets


view this post on Zulip zkao (Dec 05 2020 at 18:00):

Early disco partygoer here with limited knowledge of petrinets, wiring diagrams or category theory.

Say there is a transition g that just needs to know that place B is occupied in order to be enabled. But it does not need to "consume" B permanently.

What is the best way to represent this?

(1)

f: A -> B.
g: B -> C B.        ;; uses B and returns it back
h: B -> D.           ;; consumes B

Mostly works but in this caseg can be called many times, producing many C and hmay never called. If g could be called only once this would be good.

And this problem can be fixed by creating a new place Once and initializing it with 1 token:

f: A -> B.
g: B Once -> C B.        ;; uses B and returns it back
h: B -> D.                       ;; consumes B

This works good

(2)

f: A -> B.
copy: B -> B0 B1. ;; specialize types
g: B0 -> C.
h: B1 -> D.

always work but verbose -- make petrinets large, very quick

(3)

f: A -> B B.       ;; creates 2 tokens
g: B -> C.
h: B -> D.

weird because h (or g) can be called twice

view this post on Zulip Jelle Herold (Dec 08 2020 at 10:18):

You want to avoid case 1 because it makes the state space infinite as you noted.
Essentially you would need to copy, and 2 or 3 is therefor better.
There are subtleties, like which combination of g;h, h;g, h;h, g;g can you fire?

1 = h or g;h or g;g;h or g;h;g;g;g etc
1' = h or g;h (with Once)
2 = g;h or h;g

What do you want the behavior to be? Can you explain the use case here, to see if there is another way to deal with it?

view this post on Zulip Fabrizio Genovese (Dec 08 2020 at 11:51):

zkao said:

Early disco partygoer here with limited knowledge of petrinets, wiring diagrams or category theory.

Say there is a transition g that just needs to know that place B is occupied in order to be enabled. But it does not need to "consume" B permanently.

There's a way to represent this as a guarded net on a particularly "strange" semantics. We are writing a paper about it. Eventually this will be implemented in the software one day. For now I'd follow @Jelle Herold 's suggestion, he has great experience in modelling all sorts of stuff using nets :smile: