Top of this page
Skip navigation, go straight to the content

This is an old revision of the document!


FAQ

Can Woflan handle arc weights (aka multiple arcs)?

Yes, Woflan can handle arc weights, but there is a catch. Note that Woflan uses the fact that a free-choice net (or a net that contains no handles) can only be sound if it is S-coverable. This fact holds for nets that do not contain arc weights, but examples with arc weights exist for which this does not hold. Take, for example, the following net:

place start init 1;
place middle;
place end;
trans t1 in start out middle, middle;
trans t2 in middle, middle out end;

Woflan will report that this net is not sound due to non-live transitions, but it also reports no non-live transitions. For the former conclusion, it used the fact mentioned above (the net is free-choice, contains no handles, is not S-coverable, is bounded, contains no dead transitions, and is not sound, hence there have to be non-live transitions), for the latter it computed the actual non-live transitions.

A workaround is to make the net not feee-chocie and add handles, by adding a self-loop transition to some place that may contain multiple tokens:

place start init 1;
place middle;
place end;
trans t1 in start out middle, middle;
trans t2 in middle, middle out end;
trans t3 in middle out middle;

As a result, Woflan will not use the abovementioned fact, and will report no errors.