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

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.