public class PetriNetMetricManager
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
static PetriNetMetricManager |
getInstance() |
PetriNetMetric |
getMetric(java.lang.String name) |
java.util.List<PetriNetMetric> |
getMetrics() |
boolean |
isDefault(PetriNetMetric miner) |
void |
register(PetriNetMetric metric,
boolean isDefault) |
public static PetriNetMetricManager getInstance()
public void register(PetriNetMetric metric, boolean isDefault)
public java.util.List<PetriNetMetric> getMetrics()
public boolean isDefault(PetriNetMetric miner)
public PetriNetMetric getMetric(java.lang.String name)