Uses of Class
dev.civl.gmc.GMCConfiguration
Packages that use GMCConfiguration
Package
Description
The root package of generic model checking is used to construct model
checking applications, either sequential or concurrent.
This package provides sequential generic model checking functionality.
A simple implementation of General Model Checker (GMC) is used by a set of
code coverage test cases.
-
Uses of GMCConfiguration in dev.civl.gmc
Methods in dev.civl.gmc that return GMCConfigurationModifier and TypeMethodDescriptionGMCConfiguration.clone()Returns a deep copy of this configuration.LogEntry.getConfiguration()Returns the configuration which will be used to replay the trace.CommandLineParser.newConfig()Returns new, empty configuration with option set equal to the set of options associated to this parser.CommandLineParser.parse(Collection<String> args) Given a collection of strings, parses them in the order of their iterator to produce a new configuration.Methods in dev.civl.gmc with parameters of type GMCConfigurationModifier and TypeMethodDescriptionvoidCommandLineParser.parse(GMCConfiguration config, BufferedReader reader) Parses the reader, interpreting lines as command line args, modifying given configuration accordingly.voidCommandLineParser.parse(GMCConfiguration config, File file) Parses a file containing a configuration section, using the command line arguments from that section to modify the given configuration.voidCommandLineParser.parse(GMCConfiguration config, Collection<String> args) Given a collection of strings and a configuration compatible with this parser, parses the strings and uses the resulting information to modify the configuration.voidGMCConfiguration.read(GMCConfiguration that) Modifies this configuration by reading in the values of the given configuration and using those to set values of this one.voidGMCSection.setConfiguration(GMCConfiguration config) Updates the configuration associates with this section.Constructors in dev.civl.gmc with parameters of type GMCConfigurationModifierConstructorDescriptionGMCSection(GMCConfiguration config, String name) Constructs a new instance of GMCSection with the given GMCConfiguration and name.LogEntry(GMCConfiguration configuration) Default construtor: does nothing. -
Uses of GMCConfiguration in dev.civl.gmc.dpor
Constructors in dev.civl.gmc.dpor with parameters of type GMCConfigurationModifierConstructorDescriptionDporDfsSearcher(DependencyAnalyzer<STATE, TRANSITION> analyzer, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig) DporDfsSearcher(DependencyAnalyzer<STATE, TRANSITION> analyzer, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig, PrintStream debugOut) Constructs a new depth first search searcher. -
Uses of GMCConfiguration in dev.civl.gmc.seq
Constructors in dev.civl.gmc.seq with parameters of type GMCConfigurationModifierConstructorDescriptionDfsSearcher(EnablerIF<STATE, TRANSITION> enabler, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig) DfsSearcher(EnablerIF<STATE, TRANSITION> enabler, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig, PrintStream debugOut) Constructs a new depth first search searcher. -
Uses of GMCConfiguration in dev.civl.gmc.smc
Methods in dev.civl.gmc.smc with parameters of type GMCConfigurationModifier and TypeMethodDescriptionbooleanSMC.run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate, GMCConfiguration config) For a givenMatrixDirectedGraphgraphand apredicateimplementingStatePredicateIF,
If thepredicateis hold,truewill be returned, elsefalse.
Note that the default starting state is the state with id of0booleanSMC.run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate, Integer initialState, GMCConfiguration config) For a givenMatrixDirectedGraphgraph, apredicateimplementingStatePredicateIFand a starting stateinitialState,
If thepredicateis hold,truewill be returned, elsefalse.Constructors in dev.civl.gmc.smc with parameters of type GMCConfiguration