Package org.bigraphs.framework.simulation.modelchecking

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

  • Method Details

    • exportOpts

      public static ModelCheckingOptions.ExportOptions.Builder exportOpts()

    • transitionOpts

      public static ModelCheckingOptions.TransitionOptions.Builder transitionOpts()

    • create

      public static ModelCheckingOptions create()

    • and

      public ModelCheckingOptions and(ModelCheckingOptions.Opts opts)

    • setMeasureTime

      public void setMeasureTime(boolean measureTime)

    • isMeasureTime

      public boolean isMeasureTime()

    • doMeasureTime

      public ModelCheckingOptions doMeasureTime(boolean measureTime)
      Instruct the simulation to measure the time for individual steps of the current used simulation algorithm. Defaults to false. 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

      public ModelCheckingOptions withParallelRuleMatching(boolean flag)
      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. If false, 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

      public ModelCheckingOptions setReactionGraphWithCycles(boolean reactionGraphWithCycles)
      Configure whether the reaction graph should permit the depiction of cycles. If the parameter is set to false, 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 to false the reaction graph will visually represent a Directed Acyclic Graph (DAG) even if the BRS simulation produces cycles.

    • get

      public <T extends ModelCheckingOptions.Opts> T get(ModelCheckingOptions.Options kind)