A resource workflow net (RWF-net) is a workflow net, supplied with an additional set of initially marked resource places. Resources can be consumed and/or produced by transitions. Neither the intermediate nor final resource markings are constrained, hence a net can have an infinite number of different reachable states. An RWF-net with k tokens in the initial place and a certain number of resource tokens in resource places is called k-sound if it properly terminates with k tokens in the final place and, moreover, adding any extra initial resource does not violate its proper termination. An unmarked RWF-net is k-sound if it is k-sound for some initial resource. In this paper we prove the decidability of both marked and unmarked k-soundness for a restricted class of RWF-nets with a single unbounded resource place (1-dim RWF-nets). We present an algorithm for computing the minimal k-sound resource for a given sound 1-dim RWF-net.
Grading dozens of Petri net models manually is a tedious and error-prone task. In this paper, we present Grade/CPN, a tool supporting the grading of Colored Petri nets modeled in CPN Tools. The tool is extensible, configurable, and can check static and dynamic properties. It automatically handles tedious tasks like checking that good modeling practise is adhered to, and supports tasks that are difficult to automate, such as checking model legibility. We propose and support the Britney Temporal Logic which can be used to guide the simulator and to check temporal properties. We provide our experiences with using the tool in a course with 100 participants.