Differences

This shows you the differences between two versions of the page.

faq [2009/05/12 11:55]
hverbeek created
faq [2009/05/12 13:54] (current)
hverbeek
Line 5: Line 5:
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: 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 start init 1;
place middle;   place middle;
Line 10: Line 11:
trans t1 in start out middle, middle;   trans t1 in start out middle, middle;
trans t2 in middle, middle out end;   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. 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.
Line 15: Line 18:
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: 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 start init 1;
place middle;   place middle;
Line 21: Line 25:
trans t2 in middle, middle out end;   trans t2 in middle, middle out end;
trans t3 in middle out middle;   trans t3 in middle out middle;
+
+------
As a result, Woflan will not use the abovementioned fact, and will report no errors. As a result, Woflan will not use the abovementioned fact, and will report no errors.