org.processmining.plugins.petrinet.behavioralanalysis.woflan
Class WoflanDiagnosis

java.lang.Object
  extended by org.processmining.plugins.petrinet.behavioralanalysis.woflan.WoflanDiagnosis
All Implemented Interfaces:
org.processmining.framework.util.HTMLToString

public class WoflanDiagnosis
extends java.lang.Object
implements org.processmining.framework.util.HTMLToString

Author:
hverbeek

Nested Class Summary
 
Nested classes/interfaces inherited from interface org.processmining.framework.util.HTMLToString
org.processmining.framework.util.HTMLToString.HTMLCellRenderer
 
Field Summary
protected  org.processmining.models.graphbased.directed.petrinet.Petrinet net
          Diagnostic information.
protected  org.processmining.models.semantics.Semantics<org.processmining.models.semantics.petrinet.Marking,org.processmining.models.graphbased.directed.petrinet.elements.Transition> semantics
           
protected  org.processmining.models.graphbased.directed.petrinet.Petrinet shortCNet
           
 
Constructor Summary
WoflanDiagnosis(org.processmining.models.graphbased.directed.petrinet.Petrinet net)
          Public constructor.
 
Method Summary
 java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Transition> getDeadTransitions()
           
 java.util.Collection<org.processmining.framework.util.Pair<org.processmining.models.semantics.petrinet.Marking,org.processmining.models.graphbased.directed.petrinet.elements.Transition>> getNonLiveSequences()
          Precondition: net is bounded.
 java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Transition> getNonLiveTransitions()
           
 java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Place> getSinkPlaces()
           
 java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Place> getUnboundedPlaces()
           
 java.util.Collection<org.processmining.framework.util.Pair<org.processmining.models.semantics.petrinet.Marking,org.processmining.models.graphbased.directed.petrinet.elements.Transition>> getUnboundedSequences()
           
 java.lang.Boolean isBounded()
           
 java.lang.Boolean isLive()
           
 java.lang.Boolean isNotDead()
           
protected  void setDeadTransitions(org.processmining.models.graphbased.directed.petrinet.analysis.DeadTransitionsSet transitions)
          Sets the set of dead transitions and the final verdict to DEAD.
protected  void setNotFreeChoice(org.processmining.models.graphbased.directed.petrinet.analysis.NonExtendedFreeChoiceClustersSet clusters)
          Sets the set of non-extended-free-choice clusters.
protected  void setNotLiveTransitions(org.processmining.models.graphbased.directed.petrinet.analysis.NonLiveTransitionsSet transitions, org.processmining.models.graphbased.directed.petrinet.analysis.NonLiveSequences sequences)
          Sets the set of non-live transitions and the set of non-live sequences, and sets the final verdict to NOTLIVE.
protected  void setNotPCoveredNodes(org.processmining.models.graphbased.directed.petrinet.analysis.NotPCoveredNodesSet nodesSet)
          Sets the set of places that are not covered by any positive place invariant.
protected  void setNotSCoveredNodes(org.processmining.models.graphbased.directed.petrinet.analysis.NotSCoveredNodesSet nodesSet)
          Sets the set of nodes that are not covered by any S-component.
protected  void setPTHandles(org.processmining.models.graphbased.directed.petrinet.analysis.PTHandles handles)
          Sets the set of PT-handles.
protected  void setSinkPlaces(org.processmining.framework.plugin.PluginContext context, java.util.SortedSet<org.processmining.models.graphbased.directed.petrinet.elements.Place> places)
          Sets the set of sink places, and the final verdict to NOWFNET.
protected  void setSound()
          Sets the final verdict to SOUND.
protected  void setSourcePlaces(org.processmining.framework.plugin.PluginContext context, java.util.SortedSet<org.processmining.models.graphbased.directed.petrinet.elements.Place> places)
          Sets the set of source places, and the final verdict to NOWFNET.
protected  void setTPHandles(org.processmining.models.graphbased.directed.petrinet.analysis.TPHandles handles)
          Sets the set of TP-handles.
protected  void setUnboundedPlaces(org.processmining.models.graphbased.directed.petrinet.analysis.UnboundedPlacesSet places, org.processmining.models.graphbased.directed.petrinet.analysis.UnboundedSequences sequences)
          Sets the set of unbounded places and the set of unbounded sequences, and sets the final verdict to UNBOUNDED.
protected  void setUnconnectedNodes(org.processmining.framework.plugin.PluginContext context, java.util.SortedSet<org.processmining.models.graphbased.directed.petrinet.PetrinetNode> nodes)
          Sets the set of unconnected nodes, and the final verdict to NOWFNET.
 java.lang.String toHTMLString(boolean includeHTMLTags)
          Generates the HTML Woflan diagnosis report.
 java.lang.String toString()
          Returns a condense report in some format.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

net

protected org.processmining.models.graphbased.directed.petrinet.Petrinet net
Diagnostic information.


shortCNet

protected org.processmining.models.graphbased.directed.petrinet.Petrinet shortCNet

semantics

protected org.processmining.models.semantics.Semantics<org.processmining.models.semantics.petrinet.Marking,org.processmining.models.graphbased.directed.petrinet.elements.Transition> semantics
Constructor Detail

WoflanDiagnosis

public WoflanDiagnosis(org.processmining.models.graphbased.directed.petrinet.Petrinet net)
Public constructor. Initialize the diagnostic information.

Parameters:
context - The plug-in context.
net - The Petri net under diagnosis.
Method Detail

setSourcePlaces

protected void setSourcePlaces(org.processmining.framework.plugin.PluginContext context,
                               java.util.SortedSet<org.processmining.models.graphbased.directed.petrinet.elements.Place> places)
Sets the set of source places, and the final verdict to NOWFNET.

Parameters:
places - The set of source places.

setSinkPlaces

protected void setSinkPlaces(org.processmining.framework.plugin.PluginContext context,
                             java.util.SortedSet<org.processmining.models.graphbased.directed.petrinet.elements.Place> places)
Sets the set of sink places, and the final verdict to NOWFNET.

Parameters:
places - The set of sink places.

setUnconnectedNodes

protected void setUnconnectedNodes(org.processmining.framework.plugin.PluginContext context,
                                   java.util.SortedSet<org.processmining.models.graphbased.directed.petrinet.PetrinetNode> nodes)
Sets the set of unconnected nodes, and the final verdict to NOWFNET.

Parameters:
nodes - The set of unconnected nodes.

setNotSCoveredNodes

protected void setNotSCoveredNodes(org.processmining.models.graphbased.directed.petrinet.analysis.NotSCoveredNodesSet nodesSet)
Sets the set of nodes that are not covered by any S-component.

Parameters:
nodesSet - A set of set of nodes, containing the set of nodes that are not covered by any S-component as its only member.

setNotPCoveredNodes

protected void setNotPCoveredNodes(org.processmining.models.graphbased.directed.petrinet.analysis.NotPCoveredNodesSet nodesSet)
Sets the set of places that are not covered by any positive place invariant.

Parameters:
nodes - A set of set of places, containing the set of places that are not covered by any positive place invariant as its only member.

setUnboundedPlaces

protected void setUnboundedPlaces(org.processmining.models.graphbased.directed.petrinet.analysis.UnboundedPlacesSet places,
                                  org.processmining.models.graphbased.directed.petrinet.analysis.UnboundedSequences sequences)
Sets the set of unbounded places and the set of unbounded sequences, and sets the final verdict to UNBOUNDED.

Parameters:
places - A set of set of places, containing the set of unbounded places as its only member.
sequences - The set of unbounded sequences. Each member of this set contains either: - only transitions, in which case unboundedness is inevitable, or - one transition and a multiset of places, in which case the given transition should be disabled at the marking given by the multiset of places.

setNotLiveTransitions

protected void setNotLiveTransitions(org.processmining.models.graphbased.directed.petrinet.analysis.NonLiveTransitionsSet transitions,
                                     org.processmining.models.graphbased.directed.petrinet.analysis.NonLiveSequences sequences)
Sets the set of non-live transitions and the set of non-live sequences, and sets the final verdict to NOTLIVE.

Parameters:
transitions - A set of set of transitions, containing the set of non-live transitions as its only member.
sequences - The set of non-live sequences. Each member of this set contains either: - only transitions, in which case the final state is not reachable, or - one transition and a multiset of places, in which case the given transition should be disabled at the marking given by the multiset of places.

setDeadTransitions

protected void setDeadTransitions(org.processmining.models.graphbased.directed.petrinet.analysis.DeadTransitionsSet transitions)
Sets the set of dead transitions and the final verdict to DEAD.

Parameters:
transitions - A set of set of transition, containing the set of dead transitions as its only member.

setSound

protected void setSound()
Sets the final verdict to SOUND.


setNotFreeChoice

protected void setNotFreeChoice(org.processmining.models.graphbased.directed.petrinet.analysis.NonExtendedFreeChoiceClustersSet clusters)
Sets the set of non-extended-free-choice clusters.

Parameters:
clusters - The set of non-free-choice clusters.

setPTHandles

protected void setPTHandles(org.processmining.models.graphbased.directed.petrinet.analysis.PTHandles handles)
Sets the set of PT-handles.

Parameters:
handles - The set of PT-handles.

setTPHandles

protected void setTPHandles(org.processmining.models.graphbased.directed.petrinet.analysis.TPHandles handles)
Sets the set of TP-handles.

Parameters:
handles - The set of TP-handles.

toHTMLString

public java.lang.String toHTMLString(boolean includeHTMLTags)
Generates the HTML Woflan diagnosis report.

Specified by:
toHTMLString in interface org.processmining.framework.util.HTMLToString
Returns:
The Woflan diagnosis report in HTML format.

toString

public java.lang.String toString()
Returns a condense report in some format. Used for testing Woflan.

Overrides:
toString in class java.lang.Object

getSinkPlaces

public java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Place> getSinkPlaces()

isBounded

public java.lang.Boolean isBounded()
Returns:
Whether the net is bounded (null = unknown, true = bounded, false = unbounded).

isNotDead

public java.lang.Boolean isNotDead()
Returns:
Whether the net contains no dead transitions (null = unknown, true = no dead transitions, false = dead transitions).

isLive

public java.lang.Boolean isLive()
Returns:
Whether the net is live (null = unknown, true = live, false = not live).

getUnboundedPlaces

public java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Place> getUnboundedPlaces()
Returns:
The collection of unbounded places. Empty if boundedness is unknown or true.

getDeadTransitions

public java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Transition> getDeadTransitions()
Returns:
The collection of dead transitions. Empty if existence of dead transition is unknown or false.

getNonLiveTransitions

public java.util.Collection<org.processmining.models.graphbased.directed.petrinet.elements.Transition> getNonLiveTransitions()
Returns:
The collection of non-live transitions. Empty if liveness is unknown or true.

getUnboundedSequences

public java.util.Collection<org.processmining.framework.util.Pair<org.processmining.models.semantics.petrinet.Marking,org.processmining.models.graphbased.directed.petrinet.elements.Transition>> getUnboundedSequences()
Returns:
The unbounded sequences. Every sequence consists of a marking and a transition (enabled in this marking). From the marking, unbounded behavior can still be avoided. After having fired the transition in this marking, unbounded behavior has become unavoidable.

getNonLiveSequences

public java.util.Collection<org.processmining.framework.util.Pair<org.processmining.models.semantics.petrinet.Marking,org.processmining.models.graphbased.directed.petrinet.elements.Transition>> getNonLiveSequences()
Precondition: net is bounded.

Returns:
The non-live sequences. Every sequence consists of a marking and a transition (enabled in this marking). From the marking, the final marking can still be reached. After having fired the transition in this marking, the final marking has become unreachable.