Package jline.api.wfn

Class SoundnessReport

java.lang.Object
jline.api.wfn.SoundnessReport

public class SoundnessReport extends Object
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 Details

    • SOUND

      public static final String SOUND
      Verdict of a net whose reachability graph is complete and sound
      See Also:
    • UNSOUND

      public static final String UNSOUND
      Verdict of a net with at least one defect
      See Also:
    • UNKNOWN

      public static final String UNKNOWN
      Verdict when the state cap was reached first
      See Also:
    • k

      public int k
      Number of tokens put in the source place
    • verdict

      public String verdict
    • stateSpaceSize

      public int stateSpaceSize
      Number of reachable markings explored
    • deadlocks

      public List<int[]> deadlocks
      Reachable markings, other than the final one, that enable no transition
    • noOptionToComplete

      public List<int[]> noOptionToComplete
      Reachable markings from which the final marking is unreachable
    • improperCompletion

      public List<int[]> improperCompletion
      Reachable markings with k tokens in the sink together with other tokens
    • deadTransitions

      public List<String> deadTransitions
      Names of the transitions that fire in no reachable marking
    • unbounded

      public boolean unbounded
      True if a reachable marking strictly covers one of its ancestors
    • unboundedWitness

      public int[] unboundedWitness
      The covering marking proving unboundedness, or null
    • unboundedOrTooLarge

      public boolean unboundedOrTooLarge
      True if the state cap stopped the exploration
    • witnesses

      public List<String> witnesses
      Readable one-line descriptions of each defect
  • Constructor Details

    • SoundnessReport

      public SoundnessReport()
  • Method Details

    • isSound

      public boolean isSound()
      Returns:
      true if the verdict is SOUND
    • toString

      public String toString()
      Overrides:
      toString in class Object