Class ModelCheckingOptions
java.lang.Object
org.bigraphs.framework.simulation.modelchecking.ModelCheckingOptions
@Configuration
@ConfigurationProperties(prefix="model-checking",
ignoreInvalidFields=true)
public class ModelCheckingOptions
extends Object
This class represents the available options for the model checker
BigraphModelChecker.
It can also be configured via an external configuration file.- Author:
- Dominik Grzelak
-
Nested Class Summary
Nested ClassesModifier and TypeClassDescriptionstatic final classThis class represents export-specific options regarding the generated artifacts when synthesizing the transition system.static enumstatic interfacestatic final classClass that represents simulation-specific options. -
Method Summary
Modifier and TypeMethodDescriptionand(ModelCheckingOptions.Opts opts) static ModelCheckingOptionscreate()doMeasureTime(boolean measureTime) Instruct the simulation to measure the time for individual steps of the current used simulation algorithm.<T extends ModelCheckingOptions.Opts>
TbooleanbooleanbooleanIndicates, whether the reaction graph should permit the depiction of cycles.voidsetMeasureTime(boolean measureTime) voidsetParallelRuleMatching(boolean flag) Instruct the simulation either to perform rule matching in parallel or sequentially (default).setReactionGraphWithCycles(boolean reactionGraphWithCycles) Configure whether the reaction graph should permit the depiction of cycles.withParallelRuleMatching(boolean flag) Instruct the simulation either to perform rule matching in parallel or sequentially (default).
-
Method Details
-
exportOpts
-
transitionOpts
-
create
-
and
-
setMeasureTime
public void setMeasureTime(boolean measureTime) -
isMeasureTime
public boolean isMeasureTime() -
doMeasureTime
Instruct the simulation to measure the time for individual steps of the current used simulation algorithm. Defaults tofalse. Useful for debugging purposes.- Parameters:
measureTime- flag to enable or disable time measurement- Returns:
- the current options instance
-
setParallelRuleMatching
public void setParallelRuleMatching(boolean flag) Instruct the simulation either to perform rule matching in parallel or sequentially (default).- Parameters:
flag- flag to enable or disable parallel rule matching
-
withParallelRuleMatching
Instruct the simulation either to perform rule matching in parallel or sequentially (default).- Parameters:
flag- flag to enable or disable parallel rule matchings- Returns:
- the current options instance
-
isParallelRuleMatching
public boolean isParallelRuleMatching() -
isReactionGraphWithCycles
public boolean isReactionGraphWithCycles()Indicates, whether the reaction graph should permit the depiction of cycles. Iffalse, the reaction graph will visually represent a Directed Acyclic Graph (DAG). Otherwise, they are drawn if the BRS simulation produces cycles.Note: This configuration does not imply that cycles are absent during simulation. Rather, cycles are simply not displayed in the reaction graph.
-
setReactionGraphWithCycles
Configure whether the reaction graph should permit the depiction of cycles. If the parameter is set tofalse, the reaction graph will be a Directed Acyclic Graph (DAG).Note: This configuration does not imply that cycles are absent during simulation. Rather, cycles are simply not displayed in the reaction graph.
- Parameters:
reactionGraphWithCycles- if set tofalsethe reaction graph will visually represent a Directed Acyclic Graph (DAG) even if the BRS simulation produces cycles.
-
get
-