Package jline.api.wfn
Class SoundnessReport
java.lang.Object
jline.api.wfn.SoundnessReport
Result of
WorkflowNet.checkSoundness(int, double).
Markings are arrays over the places of the net, in place order. The
fields mirror the report struct of the MATLAB twin
(matlab/src/api/wfn/WorkflowNet.m, checkSoundness).
-
Field Summary
FieldsModifier and TypeFieldDescriptionList<int[]>Reachable markings, other than the final one, that enable no transitionNames of the transitions that fire in no reachable markingList<int[]>Reachable markings with k tokens in the sink together with other tokensintNumber of tokens put in the source placeList<int[]>Reachable markings from which the final marking is unreachablestatic final StringVerdict of a net whose reachability graph is complete and soundintNumber of reachable markings exploredbooleanTrue if a reachable marking strictly covers one of its ancestorsbooleanTrue if the state cap stopped the explorationint[]The covering marking proving unboundedness, or nullstatic final StringVerdict when the state cap was reached firststatic final StringVerdict of a net with at least one defectReadable one-line descriptions of each defect -
Constructor Summary
Constructors -
Method Summary
-
Field Details
-
SOUND
Verdict of a net whose reachability graph is complete and sound- See Also:
-
UNSOUND
Verdict of a net with at least one defect- See Also:
-
UNKNOWN
Verdict when the state cap was reached first- See Also:
-
k
public int kNumber of tokens put in the source place -
verdict
-
stateSpaceSize
public int stateSpaceSizeNumber of reachable markings explored -
deadlocks
Reachable markings, other than the final one, that enable no transition -
noOptionToComplete
Reachable markings from which the final marking is unreachable -
improperCompletion
Reachable markings with k tokens in the sink together with other tokens -
deadTransitions
Names of the transitions that fire in no reachable marking -
unbounded
public boolean unboundedTrue if a reachable marking strictly covers one of its ancestors -
unboundedWitness
public int[] unboundedWitnessThe covering marking proving unboundedness, or null -
unboundedOrTooLarge
public boolean unboundedOrTooLargeTrue if the state cap stopped the exploration -
witnesses
Readable one-line descriptions of each defect
-
-
Constructor Details
-
SoundnessReport
public SoundnessReport()
-
-
Method Details