org.processmining.plugins.petrinet.behavioralanalysis.woflan

Class WoflanDiagnosis

java.lang.Object

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

Fields

Modifier and Type	Field and Description
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

Constructors

Constructor and Description
WoflanDiagnosis(org.processmining.models.graphbased.directed.petrinet.Petrinet net) Public constructor.

Method Summary

Modifier and Type	Method and Description
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()
java.lang.Boolean	isSound()
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).

isSound

public java.lang.Boolean isSound()

Returns:

Whether the net is a sound WF-net (false = not a WF net or not sound)

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.