Package edu.udel.cis.vsl.gmc

package edu.udel.cis.vsl.gmc

The root package of generic model checking is used to construct model checking applications, either sequential or concurrent.

Some of the services provided include:

  • Command line parser to parse GMC configurations.
  • Error Log to for recording errors and corresponding traces encountered during a model checking run.
  • TransitionChooser to replay the trace file or conduct a simulation run.
  • Trace
    • represents a trace of an execution of a given model.
  • Class
    Description
    CommandLineException
    An exception that is thrown if the command line arguments are not formatted correctly.
    CommandLineParser
    A tool for parsing a command line and generating a GMCConfiguration.
    ErrorLog
    A log for recording errors and corresponding traces encountered during a model checking run.
    ExcessiveErrorException
    An exception thrown when the number of errors encountered in the course of a search of a state-transition system exceeds some specified bound.
    FalsePredicate<S>
    The state predicate which simply returns "false" at every state.
    GMCConfiguration
    A GMCConfiguration is composed of a number of GMCSection's, each of which encapsulates a set of key-value pairs, where the keys correspond to commandline parameters and the value is the value assigned to that parameter.
    GMCSection
    A GMCSection has a unique name and it encapsulates a set of key-value pairs, where the keys correspond to commandline parameters and the value is the value assigned to that parameter.
    GuidedTransitionChooser<STATE,TRANSITION>
    Transition Chooser which makes its choice using an explicit "guide".
    LogEntry
    An entry in an error log.
    MisguidedExecutionException
     
    Option
    An instance of this class represents a command-line parameter for a model checker.
    Option.OptionType
    The types of option.
    RandomTransitionChooser<STATE,TRANSITION>
    An implementation of TransitionChooser in which a transition is chosen randomly from the full set of the enabled transitions enabled at a state.
    Simulator<STATE,TRANSITION>
    A Simulator is used to execute a transition system using a TransitionChooser to determine which transition to execute from each state.
    StatePredicateIF<S>
    A state predicate is basically a function which returns either true or false at any state in the transition system.
    StateSpaceCycleException
    This is the Exception that will be thrown by the DfsSearcher if and only if 1) a cycle in state space detected; and 2) cycle violation is set to be reported.
    Trace<TRANSITION,STATE>
    This represents a trace of an execution of a given model.
    TraceStepIF<STATE>
    A TraceStepIF represents the execution result of nextState of StateManagerIF.
    TransitionChooser<STATE,TRANSITION>
    General interface for an object which can select one enabled transition from the set of enabled transitions at any state.