Top of this page
Skip navigation, go straight to the content
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.