Module dev.civl.gmc

Package dev.civl.gmc.concurrent

package dev.civl.gmc.concurrent

This package provides concurrent generic model checking functionality. It is intended to be used as a set of utilities for constructing concurrent model checking applications.

Some of the services provided include:

  • Concurrent depth first searcher of an arbitrary state-transition system
  • Class
    Description
    ConcurrentDfsSearcher<STATE,TRANSITION>
    This ConcurrentDfsSearcher is implemented based on Alfons Laarman's algorithm in paper "Partial-Order Reduction for Multi-Core LTL Model Checking", but there are improvements being made.
    ConcurrentNode<STATE>
     
    ConcurrentNodeFactory<STATE,TRANSITION>
     
    ConcurrentStateManagerIF<STATE,TRANSITION>
    A ConcurrentStateManager is used by a ConcurrentDfsSearcher which encapsulates all methods that are needed by ConcurrentDfsSearcher on STATE.
    MyThreadPool
    The threadPool That is used to manage the threads used in the algorithm.
    ProvisoValue
    This enumeration stores the result of checking "stack proviso" of a STATE in the STATE-TRANSITION system.
    StackEntry<STATE,TRANSITION>
    The stack entry that is going to be pushed onto the stack during the search.